Model generation with Boolean Constraints

Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

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 CASC-JS system competition.

Original languageEnglish
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning - 8th International Conference, LPAR 2001, Proceedings
EditorsRobert Nieuwenhuis, Andrei Voronkov
PublisherSpringer Verlag
Pages299-308
Number of pages10
ISBN (Electronic)9783540429579
DOIs
Publication statusPublished - 2001
Event8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2001 - Havana, Cuba
Duration: Dec 3 2001Dec 7 2001

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2250
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2001
CountryCuba
CityHavana
Period12/3/0112/7/01

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

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

Cite this