Free variable tableaux for a logic with term declarations

DOI10.1007/3-540-69778-0_23MaRDI QIDQ3838814zbMATH OpenFDO

Authors P. J. Martin, A. Gavilanes, J. Leach

Publication date 8 October 1998

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-69778-0_23

zbMATH Keywords

free variable tableau methods with term declarationorder-sorted logicsorted unification calculus

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Review text

The reported research is focused on free variable tableau methods with term declaration. Most of the developments are performed for an order-sorted logic (LTD) which extends classical first-order logic by introducing a new formula constructor and allowing the dynamic sort declarations of terms. The main syntactic and semantic features of the Logic with Term Declarations are exhibited in the introductory part. A ground tableau method is presented in the fourth section of the paper and the proof of its soundness with respect to the new concept of well-sorted substitutions is supplied. An improved version of the method resulted by restricting the application of the substitution rule to close branches is shown and the extension of the ground tableau method to a free variable version is derived. Aiming to obtain suitable well-sorted unifiers in a free variable tableau whenever its related ground version is closed, a sorted unification calculus is developed in the sixth section of the paper. Finally, a tableau system where the application of the substitution rule is restricted to close branches is defined based on the previously introduced sorted unification calculus. It is proved that the calculus is sound and complete. For the entire collection see [Zbl 0888.00018].

Recommendations

• Free variable tableaux for propositional modal logics
• Free-variable tableaux for propositional modal logics
• Free variable tableaux for a many sorted logic with preorders
• Tableaux for free logics with descriptions
• A Free Variable Version of the First-Order Predicate Calculus
• Free-variable tableaux for constant-domain quantified modal logics with rigid and non-rigid designation
• Ground and free-variable tableaux for variants of quantified modal logics
• Full first-order free variable sequents and tableaux in implicit induction
• The liberalized -rule in free variable semantic tableaux
• Free variables and subexpressions in higher-order meta logic

Cited in

(5)

• A variable-free logic for mass terms
• Free-variable semantic tableaux for the logic of fuzzy inequalities
• Logics in Artificial Intelligence
• Tableau methods for a logic with term declarations
• Variable declarations in natural deduction

This page was built for publication: Free variable tableaux for a logic with term declarations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3838814)