Name
Abstract | ||
|---|---|---|
We survey some basic issues in first-order theorem proving and their implications for conditional term-rewriting systems. In particular, we discuss the propositional efficiency of theorem proving strategies, goal-sensitivity, and the use of semantics. We give several recommendations for theorem proving strategies to enable them to properly treat these issues. Although few current theorem provers implement these recommendations, we discuss the clause linking theorem proving method and its extension to equality and semantics as examples of methods that satisfy most or all of our recommendations. Implicit induction theorem provers meet our recommendations, to some extent. We also discuss correctness and efficiency issues involved in the use of semantics in first-order theorem proving. Finally, we discuss issues of efficiency and semantics in conditional term-rewriting. |
Year | DOI | Venue |
|---|---|---|
1992 | 10.1007/3-540-56393-8_19 | CTRS |
Keywords | Field | DocType |
first-order theorem proving,conditional term rewriting,first order,satisfiability,theorem proving,theorem prover | Discrete mathematics,Automated theorem proving,Correctness,Rewriting,Confluence,Fundamental theorem,Knuth–Bendix completion algorithm,Mathematics,Semantics,Calculus,Compactness theorem | Conference |
ISBN | Citations | PageRank |
3-540-56393-8 | 6 | 0.50 |
References | Authors | |
17 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| David A. Plaisted | 1 | 1680 | 255.36 |
| Geoffrey D. Alexander | 2 | 11 | 2.28 |
| Heng Chu | 3 | 58 | 4.78 |
| Shie-Jue Lee | 4 | 770 | 66.08 |