### Abstract

This paper presents a model-generation based parallel theorem prover for first-order logic implemented in KL1. The prover, called MGTP, is efficient in solving range-restricted non-Horn problems. The range-restrictedness condition allows us to represent object-level variables with KL1 variables, and to use only matching rather than full unification, thereby obtaining an interpreter that is very simple yet efficient. The implementation techniques developed are also useful for other related areas, such as truth maintenance systems and intelligent database systems. To improve the efficiency of MGTP, we also developed a ramified-stack (RAMS) algorithm for removing redundant computation during the conjunctive matching phase of a proving process. Experimental results show that an MGTP prover with RAMS can attain orders of magnitude of speedup over the naive one without RAMS, and can achieve good performance for non-Horn problems on a non-shared memory multiprocessor, Multi-PSI.

Original language | English |
---|---|

Pages | 535-548 |

Number of pages | 14 |

Publication status | Published - Dec 1 1991 |

Event | Logic Programming - Proceedings of the 8th International Conference - Paris, Fr Duration: Jun 24 1991 → Jun 28 1991 |

### Other

Other | Logic Programming - Proceedings of the 8th International Conference |
---|---|

City | Paris, Fr |

Period | 6/24/91 → 6/28/91 |

### Fingerprint

### All Science Journal Classification (ASJC) codes

- Engineering(all)

### Cite this

*Model generation theorem prover in KL1 using a ramified-stack algorithm*. 535-548. Paper presented at Logic Programming - Proceedings of the 8th International Conference, Paris, Fr, .

**Model generation theorem prover in KL1 using a ramified-stack algorithm.** / Fujita, Hiroshi; Hasegawa, Ryuzo.

Research output: Contribution to conference › Paper

}

TY - CONF

T1 - Model generation theorem prover in KL1 using a ramified-stack algorithm

AU - Fujita, Hiroshi

AU - Hasegawa, Ryuzo

PY - 1991/12/1

Y1 - 1991/12/1

N2 - This paper presents a model-generation based parallel theorem prover for first-order logic implemented in KL1. The prover, called MGTP, is efficient in solving range-restricted non-Horn problems. The range-restrictedness condition allows us to represent object-level variables with KL1 variables, and to use only matching rather than full unification, thereby obtaining an interpreter that is very simple yet efficient. The implementation techniques developed are also useful for other related areas, such as truth maintenance systems and intelligent database systems. To improve the efficiency of MGTP, we also developed a ramified-stack (RAMS) algorithm for removing redundant computation during the conjunctive matching phase of a proving process. Experimental results show that an MGTP prover with RAMS can attain orders of magnitude of speedup over the naive one without RAMS, and can achieve good performance for non-Horn problems on a non-shared memory multiprocessor, Multi-PSI.

AB - This paper presents a model-generation based parallel theorem prover for first-order logic implemented in KL1. The prover, called MGTP, is efficient in solving range-restricted non-Horn problems. The range-restrictedness condition allows us to represent object-level variables with KL1 variables, and to use only matching rather than full unification, thereby obtaining an interpreter that is very simple yet efficient. The implementation techniques developed are also useful for other related areas, such as truth maintenance systems and intelligent database systems. To improve the efficiency of MGTP, we also developed a ramified-stack (RAMS) algorithm for removing redundant computation during the conjunctive matching phase of a proving process. Experimental results show that an MGTP prover with RAMS can attain orders of magnitude of speedup over the naive one without RAMS, and can achieve good performance for non-Horn problems on a non-shared memory multiprocessor, Multi-PSI.

UR - http://www.scopus.com/inward/record.url?scp=0026271995&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0026271995&partnerID=8YFLogxK

M3 - Paper

AN - SCOPUS:0026271995

SP - 535

EP - 548

ER -