@inproceedings{7598181f038846d39f138e6a2b05ddac,
title = "Model generation with Boolean Constraints",
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.",
author = "Miyuki Koshimura and Hiroshi Fujita and Ryuzo Hasegawa",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2001. Copyright: Copyright 2020 Elsevier B.V., All rights reserved.; 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2001 ; Conference date: 03-12-2001 Through 07-12-2001",
year = "2001",
doi = "10.1007/3-540-45653-8_20",
language = "English",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "299--308",
editor = "Robert Nieuwenhuis and Andrei Voronkov",
booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning - 8th International Conference, LPAR 2001, Proceedings",
address = "Germany",
}