Hyper Tableaux with Equality

DOI10.1007/978-3-540-73595-3_36zbMath1213.03019OpenAlexW1813202136MaRDI QIDQ3608795

Björn Pelzer, Peter Baumgartner, Ulrich Furbach

Publication date: 6 March 2009

Published in: Automated Deduction – CADE-21 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-73595-3_36

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Automated Reasoning in the Wild, Theorem Proving with Bounded Rigid E-Unification, Representing and building models for decidable subclasses of equational clausal logic, LogAnswer - A Deduction-Based Question Answering System (System Description), First-Order Tableaux in Applications (Extended Abstract), Deontic Logic for Human Reasoning, SCL(EQ): SCL for first-order logic with equality, Blocking and other enhancements for bottom-up model generation methods, Possible models computation and revision -- a practical approach, SCL(EQ): SCL for first-order logic with equality