Model generation with Boolean Constraints

Research output: Contribution to journalArticle

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 TPTP problem library.

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

Fingerprint

Logic programming

All Science Journal Classification (ASJC) codes

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

Cite this

Model generation with Boolean Constraints. / Koshimura, Miyuki; Fujita, Hiroshi; Hasegawa, R.

In: Research Reports on Information Science and Electrical Engineering of Kyushu University, Vol. 6, No. 2, 09.2001, p. 157-160.

Research output: Contribution to journalArticle

@article{510138c28a244744911e2b34d0242440,
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 TPTP problem library.",
author = "Miyuki Koshimura and Hiroshi Fujita and R. Hasegawa",
year = "2001",
month = "9",
language = "English",
volume = "6",
pages = "157--160",
journal = "Research Reports on Information Science and Electrical Engineering of Kyushu University",
issn = "1342-3819",
publisher = "Kyushu University, Faculty of Science",
number = "2",

}

TY - JOUR

T1 - Model generation with Boolean Constraints

AU - Koshimura, Miyuki

AU - Fujita, Hiroshi

AU - Hasegawa, R.

PY - 2001/9

Y1 - 2001/9

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

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

UR - http://www.scopus.com/inward/record.url?scp=0035454678&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0035454678&partnerID=8YFLogxK

M3 - Article

VL - 6

SP - 157

EP - 160

JO - Research Reports on Information Science and Electrical Engineering of Kyushu University

JF - Research Reports on Information Science and Electrical Engineering of Kyushu University

SN - 1342-3819

IS - 2

ER -