Studia Logica 72 (1):31-59 (2002)
|Abstract||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||No keywords specified (fix it)|
|Categories||categorize this paper)|
|Through your library||Configure|
Similar books and articles
Noriko H. Arai, Toniann Pitassi & Alasdair Urquhart (2006). The Complexity of Analytic Tableaux. Journal of Symbolic Logic 71 (3):777 - 790.
Marta Cialdea Mayer & Serenella Cerrito (2001). Ground and Free-Variable Tableaux for Variants of Quantified Modal Logics. Studia Logica 69 (1):97-131.
Riccardo Rosati (2001). A Sound and Complete Tableau Calculus for Reasoning About Only Knowing and Knowing at Most. Studia Logica 69 (1):171-191.
André Vellino (1993). The Relative Complexity of Analytic Tableaux and SL-Resolution. Studia Logica 52 (2):323 - 337.
Sorry, there are not enough data points to plot this chart.
Added to index2009-01-28
Recent downloads (6 months)0
How can I increase my downloads?