| Title: | A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses |
| Authors: | Sophie Tourret, Mnacho Echenim and Nicolas Peltier |
| Proceedings: | PAAR 2014 Proceedings |
| Editors: | Stephan Schulz, Leonardo De Moura and Boris Konev |
| Keywords: | prime impliquates, equational logic, constraints |
| Abstract: | We describe an algorithm that generates prime implicates of equational clause sets without variables and function symbols. The procedure is based on constrained superposition rules, where constraints are used to store literals that are asserted as additional axioms (or hypotheses) during the proof search. This approach is sound and deductive-complete, and it is more ecient than previous algorithms based on conditional paramodulation. It is also more exible in the sense that it allows one to restrict the search space by imposing additional properties that the generated
implicates should satisfy (e.g., to ensure relevance). |
| Pages: | 11 |
| Talk: | Jul 23 08:45 |
| Paper: |  |