Studia Logica 72 (1):31-59 (2002)
In this paper we integrate a sorted unification calculus into free variable tableau methods for logics with term declarations. The calculus we define is used to close a tableau at once, unifying a set of equations derived from pairs of potentially complementary literals occurring in its branches. Apart from making the deduction system sound and complete, the calculus is terminating and so, it can be used as a decision procedure. In this sense we have separated the complexity of sorts from the undecidability of first order logic.
|Keywords||Philosophy Logic Mathematical Logic and Foundations Computational Linguistics|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
The Complexity of Analytic Tableaux.Noriko H. Arai, Toniann Pitassi & Alasdair Urquhart - 2006 - Journal of Symbolic Logic 71 (3):777 - 790.
The Relative Complexity of Analytic Tableaux and SL-Resolution.André Vellino - 1993 - Studia Logica 52 (2):323 - 337.
A Sound and Complete Tableau Calculus for Reasoning About Only Knowing and Knowing at Most.Riccardo Rosati - 2001 - Studia Logica 69 (1):171-191.
Ground and Free-Variable Tableaux for Variants of Quantified Modal Logics.Marta Cialdea Mayer & Serenella Cerrito - 2001 - Studia Logica 69 (1):97-131.
A Tableau Calculus with Automaton-Labelled Formulae for Regular Grammar Logics.Rajeev Gore - unknown
Added to index2009-01-28
Total downloads8 ( #484,301 of 2,153,826 )
Recent downloads (6 months)1 ( #398,274 of 2,153,826 )
How can I increase my downloads?