zbMATH — the first resource for mathematics

Quantifier-free equational logic and prime implicate generation. (English) Zbl 06515515
Felty, Amy P. (ed.) et al., Automated deduction – CADE-25. 25th international conference on automated deduction, Berlin, Germany, August 1–7, 2015. Proceedings. Cham: Springer (ISBN 978-3-319-21400-9/pbk; 978-3-319-21401-6/ebook). Lecture Notes in Computer Science 9195. Lecture Notes in Artificial Intelligence, 311-325 (2015).
Summary: An algorithm for generating prime implicates of sets of equational ground clauses is presented. It consists in extending the standard Superposition Calculus with rules that allow attaching hypotheses to clauses to perform additional inferences. The hypotheses that lead to a refutation represent implicates of the original set of clauses. The set of prime implicates of a clausal set can thus be obtained by saturation of this set. Data structures and algorithms are also devised to represent sets of constrained clauses in an efficient and concise way.
Our method is proven to be correct and complete. Practical experimentations show the relevance of our method in comparison to existing approaches for propositional or first-order logic.
For the entire collection see [Zbl 1316.68011].

03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI