Name
Abstract | ||
|---|---|---|
In this paper, we study two lemma methods for accelerating Loveland's model elimination calculus: One is lemma generalization and another is non-unit lemma matching. The derivation of lemmas in this paper is a dynamic one, i.e., lemma generation is repeatedly performed during an entire refutation search process. A derived lemma is immediately generalized by investigating the obtained subproof of the lemma. The lemma generalization increases the possibility of successful applications of the lemma matching rule. The non-unit lemma matching is an extension of the previously proposed unit lemma matching, and has the ability for stably speeding up model elimination calculus by monotonically reducing the refutation search space. We have implemented a PTTP-based theorem prover, named I-THOP, which performs unit lemma generalization and 2-literal non-unit lemma matching. We report good experimental results obtained with I-THOP. |
Year | DOI | Venue |
|---|---|---|
1999 | 10.1007/3-540-46674-6_15 | ASIAN |
Keywords | Field | DocType |
model elimination calculus,lemma generation,2-literal non-unit lemma matching,non-unit lemma matching,unit lemma generalization,entire refutation search process,lemma method,lemma generalization,lemma matching rule,unit lemma matching,model elimination,search space,theorem prover | Aubin–Lions lemma,Discrete mathematics,Borel–Cantelli lemma,Teichmüller–Tukey lemma,Zorn's lemma,Céa's lemma,Fatou's lemma,Pumping lemma for context-free languages,Lemma (mathematics),Mathematics | Conference |
ISBN | Citations | PageRank |
3-540-66856-X | 0 | 0.34 |
References | Authors | |
20 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Koji Iwanuma | 1 | 138 | 17.65 |
| Kenichi Kishino | 2 | 0 | 0.34 |