Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/978-3-319-21401-6_21 | Lecture Notes in Artificial Intelligence |
Field | DocType | Volume |
Prime (order theory),Data structure,Discrete mathematics,Uninterpreted function,Computer science,Propositional calculus,Algorithm,Superposition calculus,Equational logic | Conference | 9195 |
ISSN | Citations | PageRank |
0302-9743 | 2 | 0.37 |
References | Authors | |
20 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mnacho Echenim | 1 | 95 | 15.75 |
| Nicolas Peltier | 2 | 50 | 11.84 |
| Sophie Tourret | 3 | 8 | 5.20 |