Model generation with Boolean Constraints

M. Koshimura, Hiroshi Fujita, R. Hasegawa

Research output: Contribution to journalArticlepeer-review


We present a simple method for eliminating redundant searches in model generation. The method employs Boolean Constraints which are conjunctions of ground instances of clauses having participated in proofs. Boolean Constraints work as sets of lemmas with which duplicate subproofs and irrelevant model extensions can be eliminated. The method has been tentatively implemented on a constraint logic programming system. We evaluated effects of the method by proving some typical problems taken from the TPTP problem library.

Original languageEnglish
Pages (from-to)157-160
Number of pages4
JournalResearch Reports on Information Science and Electrical Engineering of Kyushu University
Issue number2
Publication statusPublished - Sept 2001

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Engineering (miscellaneous)
  • Electrical and Electronic Engineering


Dive into the research topics of 'Model generation with Boolean Constraints'. Together they form a unique fingerprint.

Cite this