### 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 |

Externally published | Yes |

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 |

### All Science Journal Classification (ASJC) codes

- Engineering(all)

## Fingerprint Dive into the research topics of 'Model generation theorem prover in KL1 using a ramified-stack algorithm'. Together they form a unique fingerprint.

## 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, .