Studia Logica 85 (3):283 - 302 (2007)
|Abstract||We present two proof systems for first-order logic with identity and without function symbols. The first one is an extension of the Rasiowa-Sikorski system with the rules for identity. This system is a validity checker. The rules of this system preserve and reflect validity of disjunctions of their premises and conclusions. The other is a Tableau system, which is an unsatisfiability checker. Its rules preserve and reflect unsatisfiability of conjunctions of their premises and conclusions. We show that the two systems are dual to each other. The duality is expressed in a formal way which enables us to define a transformation of proofs in one of the systems into the proofs of the other.|
|Keywords||No keywords specified (fix it)|
|Through your library||Configure|
Similar books and articles
Marcello D'Agostino (1992). Are Tableaux an Improvement on Truth-Tables? Journal of Logic, Language and Information 1 (3):235-252.
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.
Bernhard Beckert & Rajeev GorÉ (2001). Free-Variable Tableaux for Propositional Modal Logics. Studia Logica 69 (1):59-96.
Joke Meheus & Dagmar Provijn (2007). Abduction Through Semantic Tableaux Versus Abduction Through Goal-Directed Proofs. Theoria 22 (3):295-304.
Carlo Cellucci (2000). Analytic Cut Trees. Logic Journal of the IGPL 8:733-750.
Francis Jeffry Pelletier (1998). Automated Natural Deduction in Thinker. Studia Logica 60 (1):3-43.
Noriko H. Arai, Toniann Pitassi & Alasdair Urquhart (2006). The Complexity of Analytic Tableaux. Journal of Symbolic Logic 71 (3):777 - 790.
Added to index2009-01-28
Total downloads10 ( #106,438 of 549,198 )
Recent downloads (6 months)1 ( #63,397 of 549,198 )
How can I increase my downloads?