Effcient minimal model generation using branching lemmas

Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura

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

14 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
DOIs
Publication statusPublished - 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

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Effcient minimal model generation using branching lemmas'. Together they form a unique fingerprint.

Cite this