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

Hiroshi Fujita, Ryuzo Hasegawa

Research output: Contribution to conferencePaper

34 Citations (Scopus)

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 languageEnglish
Pages535-548
Number of pages14
Publication statusPublished - Dec 1 1991
Externally publishedYes
EventLogic Programming - Proceedings of the 8th International Conference - Paris, Fr
Duration: Jun 24 1991Jun 28 1991

Other

OtherLogic Programming - Proceedings of the 8th International Conference
CityParis, Fr
Period6/24/916/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

    Fujita, H., & Hasegawa, R. (1991). 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, .