New implementation technique for model generation theorem provers to solve constraint satisfaction problems

Ryuzo Hasegawa, Hiroshi Fujita

Research output: Contribution to journalArticle

4 Citations (Scopus)

Abstract

A new implementation technique for model-generation theorem provers (MGTP) is presented, which is particularly efficient in solving constraint satisfaction problems. We solved the so-called multi-environment problem by using restoration lists for destructively modified data structures. Furthermore, we introduced a new mechanism called Activation-cell which dramatically reduces the complexity of conjunctive matching, subsumption tests, and conflict tests in the proving process of MGTP. Combined with other implementation techniques including term-indexing and clause-indexing, the new MGTP written in Java shows remarkable performance compared to the previous implementations.

Original languageEnglish
Pages (from-to)57-62
Number of pages6
JournalResearch Reports on Information Science and Electrical Engineering of Kyushu University
Volume4
Issue number1
Publication statusPublished - Mar 1 1999

All Science Journal Classification (ASJC) codes

  • Computer Science(all)
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'New implementation technique for model generation theorem provers to solve constraint satisfaction problems'. Together they form a unique fingerprint.

  • Cite this