Effcient minimal model generation using branching lemmas

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

12 Citations (Scopus)

Abstract

An effcient method for minimal model generation is presented. The method employs branching assumptions and lemmas so as to prune branches that lead to nonminimal models, and to reduce minimality tests on obtained models. This method is applicable to other approaches such as Bry's complement splitting and constrained search or Niemelä's groundedness test, and greatly improves their effciency.We implemented MM-MGTP based on the method. Experimental results with MM-MGTP show a remarkable speedup compared to MM-SATCHMO.

Original languageEnglish
Title of host publicationAutomated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings
EditorsDavid McAllester
PublisherSpringer Verlag
Pages184-199
Number of pages16
ISBN (Electronic)3540676643, 9783540676645
Publication statusPublished - Jan 1 2000
Event17th International Conference on Automated Deduction, CADE 2000 - Pittsburgh, United States
Duration: Jun 17 2000Jun 20 2000

Publication series

NameLecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)
Volume1831
ISSN (Print)0302-9743

Other

Other17th International Conference on Automated Deduction, CADE 2000
CountryUnited States
CityPittsburgh
Period6/17/006/20/00

Fingerprint

Minimal Model
Branching
Lemma
Minimality
Speedup
Branch
Complement
Experimental Results
Model

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Hasegawa, R., Fujita, H., & Koshimura, M. (2000). Effcient minimal model generation using branching lemmas. In D. McAllester (Ed.), Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings (pp. 184-199). (Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science); Vol. 1831). Springer Verlag.

Effcient minimal model generation using branching lemmas. / Hasegawa, Ryuzo; Fujita, Hiroshi; Koshimura, Miyuki.

Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings. ed. / David McAllester. Springer Verlag, 2000. p. 184-199 (Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science); Vol. 1831).

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

Hasegawa, R, Fujita, H & Koshimura, M 2000, Effcient minimal model generation using branching lemmas. in D McAllester (ed.), Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings. Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science), vol. 1831, Springer Verlag, pp. 184-199, 17th International Conference on Automated Deduction, CADE 2000, Pittsburgh, United States, 6/17/00.
Hasegawa R, Fujita H, Koshimura M. Effcient minimal model generation using branching lemmas. In McAllester D, editor, Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings. Springer Verlag. 2000. p. 184-199. (Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)).
Hasegawa, Ryuzo ; Fujita, Hiroshi ; Koshimura, Miyuki. / Effcient minimal model generation using branching lemmas. Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings. editor / David McAllester. Springer Verlag, 2000. pp. 184-199 (Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)).
@inproceedings{677773b9aba14c6596acf9a0b20fc3a2,
title = "Effcient minimal model generation using branching lemmas",
abstract = "An effcient method for minimal model generation is presented. The method employs branching assumptions and lemmas so as to prune branches that lead to nonminimal models, and to reduce minimality tests on obtained models. This method is applicable to other approaches such as Bry's complement splitting and constrained search or Niemel{\"a}'s groundedness test, and greatly improves their effciency.We implemented MM-MGTP based on the method. Experimental results with MM-MGTP show a remarkable speedup compared to MM-SATCHMO.",
author = "Ryuzo Hasegawa and Hiroshi Fujita and Miyuki Koshimura",
year = "2000",
month = "1",
day = "1",
language = "English",
series = "Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)",
publisher = "Springer Verlag",
pages = "184--199",
editor = "David McAllester",
booktitle = "Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings",
address = "Germany",

}

TY - GEN

T1 - Effcient minimal model generation using branching lemmas

AU - Hasegawa, Ryuzo

AU - Fujita, Hiroshi

AU - Koshimura, Miyuki

PY - 2000/1/1

Y1 - 2000/1/1

N2 - An effcient method for minimal model generation is presented. The method employs branching assumptions and lemmas so as to prune branches that lead to nonminimal models, and to reduce minimality tests on obtained models. This method is applicable to other approaches such as Bry's complement splitting and constrained search or Niemelä's groundedness test, and greatly improves their effciency.We implemented MM-MGTP based on the method. Experimental results with MM-MGTP show a remarkable speedup compared to MM-SATCHMO.

AB - An effcient method for minimal model generation is presented. The method employs branching assumptions and lemmas so as to prune branches that lead to nonminimal models, and to reduce minimality tests on obtained models. This method is applicable to other approaches such as Bry's complement splitting and constrained search or Niemelä's groundedness test, and greatly improves their effciency.We implemented MM-MGTP based on the method. Experimental results with MM-MGTP show a remarkable speedup compared to MM-SATCHMO.

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

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

M3 - Conference contribution

AN - SCOPUS:84937391182

T3 - Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)

SP - 184

EP - 199

BT - Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings

A2 - McAllester, David

PB - Springer Verlag

ER -