| Creator |
|
|
|
|
|
|
|
| Language |
|
| Publisher |
|
|
|
| Date |
|
| Source Title |
|
| Vol |
|
| Issue |
|
| First Page |
|
| Last Page |
|
| Publication Type |
|
| Access Rights |
|
| JaLC DOI |
|
| Related DOI |
|
| Related URI |
|
| Relation |
|
| Abstract |
Factorization used in resolution provers can be effectively applied to model generation provers in order to eliminate the redundancies in case splittings. We propose a new factorization-based techniqu...e called a static/dynamic lemma generation, and present its efficient implementation on MGTP(Model Generation Theorem Prover). Experimental results obtained by running MGTP with the technique for several problems from the TPTP library demonstrate the effectiveness of the proposed technique and implementation.show more
|
Export Mendeley
p081