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

Fingerprint

Phase matching
Data storage equipment
Intelligent databases

All Science Journal Classification (ASJC) codes

  • Engineering(all)

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

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

1991. 535-548 Paper presented at Logic Programming - Proceedings of the 8th International Conference, Paris, Fr, .

Research output: Contribution to conferencePaper

Fujita, H & Hasegawa, R 1991, 'Model generation theorem prover in KL1 using a ramified-stack algorithm' Paper presented at Logic Programming - Proceedings of the 8th International Conference, Paris, Fr, 6/24/91 - 6/28/91, pp. 535-548.
Fujita H, Hasegawa R. Model generation theorem prover in KL1 using a ramified-stack algorithm. 1991. Paper presented at Logic Programming - Proceedings of the 8th International Conference, Paris, Fr, .
Fujita, Hiroshi ; Hasegawa, Ryuzo. / Model generation theorem prover in KL1 using a ramified-stack algorithm. Paper presented at Logic Programming - Proceedings of the 8th International Conference, Paris, Fr, .14 p.
@conference{8dea1674d3044439afa60ae5dcdd1949,
title = "Model generation theorem prover in KL1 using a ramified-stack algorithm",
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.",
author = "Hiroshi Fujita and Ryuzo Hasegawa",
year = "1991",
month = "12",
day = "1",
language = "English",
pages = "535--548",
note = "Logic Programming - Proceedings of the 8th International Conference ; Conference date: 24-06-1991 Through 28-06-1991",

}

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 -