Semantic tableaux with equality

DOI10.1093/LOGCOM/7.1.39MaRDI QIDQ2785839zbMATH OpenOpenAlexFDO

Authors Bernhard Beckert

Publication date 21 April 1997

Published in Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/logcom/7.1.39

zbMATH Keywords

\(E\)-unificationautomated deductionequality reasoningsemantic tableauxsurvey

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Grammars and rewriting systems (68Q42)

Review text

This article is a very good survey of deduction methods based on semantic tableaux, and the approaches to enrich semantic tableaux with equality reasoning. It covers ground semantic tableaux, semantic tableaux with free variables, and semantic tableaux with universal variables. For equality reasoning in the context of semantic tableaux it considers methods based on adding expansion rules for equality and methods based on \(E\)-unification. Depending on the type of tableaux, the latter can be universal \(E\)-unification, rigid \(E\)-unification, or mixed universal and rigid \(E\)-unification. The paper can be recommended as introductory reading for starting research in equality reasoning in the context of semantic tableaux. On the other hand, somebody interested in equality reasoning should also consult other sources, e.g.:NEWLINENEWLINENEWLINE\textit{N. Dershowitz} and \textit{J.-P. Jouannaud}, ``Rewrite systems [in: J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, Vol. B, 243-320 (1990; Zbl 0714.68001)],NEWLINENEWLINENEWLINE\textit{D. A. Plaisted}, ``Equational reasoning and term rewriting systems [in: D. M. Gabbay et al. (eds.), Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 1, 273-364 (1993; Zbl 0808.68027)],NEWLINENEWLINENEWLINE\textit{M. P. Bonacina} and \textit{J. Hsiang}, ``Towards a foundation of completion procedures as semidecision procedures [Theor. Comput. Sci. 146, 199-242 (1995; Zbl 0873.68102)].

Recommendations

• Adding equality to semantic tableaux
• Equality reasoning in sequent-based calculi
• Superposition-based equality handling for analytic tableaux
• A Tableaux Method for Systematic Simultaneous Search for Refutations and Models using Equational Problems
• Incremental theory reasoning methods for semantic tableaux

Cited in

(6)

• Adding equality to semantic tableaux
• Ordered semantic hyper tableaux
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Equality reasoning in sequent-based calculi
• Modal tableau systems with blocking and congruence closure
• Incremental theory reasoning methods for semantic tableaux

This page was built for publication: Semantic tableaux with equality

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