Semantic tableaux with equality

DOI10.1093/logcom/7.1.39zbMath0876.03008OpenAlexW2110641123MaRDI QIDQ2785839

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

surveyautomated deductionsemantic tableauxequality reasoning\(E\)-unification

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)

Related Items

Modal Tableau Systems with Blocking and Congruence Closure, First-order automated reasoning with theories: when deduction modulo theory meets practice