Constrained Hyper Tableaux
| Abstract | Hyper tableau reasoning is a version of clausal form tableau reasoning where all negative literals in a clause are resolved away in a single inference step. Constrained hyper tableaux are a generalization of hyper tableaux, where branch closing substitutions, from the point of view of model generation, give rise to constraints on satisfying assignments for the branch. These variable constraints eliminate the need for the awkward ‘purifying substitutions’ of hyper tableaux. The paper presents a non-destructive and proof confluent calculus for constrained hyper tableaux, together with a soundness and completeness proof, with completeness based on a new way to generate models from open tableaux. It is pointed out that the variable constraint approach applies to free variable tableau reasoning in general | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,672 |
| External links |
  Try with proxy. |
| Through your library | Only published papers are available at libraries |
Similar books and articlesNoriko H. Arai, Toniann Pitassi & Alasdair Urquhart (2006). The Complexity of Analytic Tableaux. Journal of Symbolic Logic 71 (3):777 - 790.
Bernhard Beckert & Rajeev GorÉ (2001). Free-Variable Tableaux for Propositional Modal Logics. Studia Logica 69 (1):59-96.
Luis Fariñas del Cerro & Olivier Gasquet (2006). Modal Tableaux for Reasoning About Diagrams. Poznan Studies in the Philosophy of the Sciences and the Humanities 91 (1):169-184.
Carlo Cellucci (2000). Analytic Cut Trees. Logic Journal of the IGPL 8:733-750.
P. J. Martín & A. Gavilanes (2002). Simultaneous Rigid Sorted Unification for Tableaux. Studia Logica 72 (1):31-59.
Marcello D'Agostino (1992). Are Tableaux an Improvement on Truth-Tables? Journal of Logic, Language and Information 1 (3):235-252.
Joanna Golinska-Pilarek & Ewa Orlowska (2006). Relational Logics and Their Applications. In Harrie de Swart, Ewa Orlowska, Gunther Smith & Marc Roubens (eds.), Theory and Applications of Relational Structures as Knowledge Instruments II. Springer.
Dan E. Willard (2002). How to Extend the Semantic Tableaux and Cut-Free Versions of the Second Incompleteness Theorem Almost to Robinson's Arithmetic Q. Journal of Symbolic Logic 67 (1):465-496.
Walter A. Carnielli (1987). Systematization of Finite Many-Valued Logics Through the Method of Tableaux. Journal of Symbolic Logic 52 (2):473-493.
Analytics
Monthly downloads |
Added to index2010-11-21Total downloads8 ( #123,036 of 549,068 )Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
