Skip navigation
Skip navigation

The model evolution calculus as a first-order DPLL method

Baumgartner, Peter; Tinelli, Cesare

Description

The DPLL procedure is the basis of some of the most successful propositional satisfiability solvers to date. Although originally devised as a proof-procedure for first-order logic, it has been used almost exclusively for propositional logic so far because of its highly inefficient treatment of quantifiers, based on instantiation into ground formulas. The FDPLL calculus by Baumgartner was the first successful attempt to lift the procedure to the first-order level without resorting to ground...[Show more]

dc.contributor.authorBaumgartner, Peter
dc.contributor.authorTinelli, Cesare
dc.date.accessioned2015-12-10T22:14:11Z
dc.identifier.issn0004-3702
dc.identifier.urihttp://hdl.handle.net/1885/50162
dc.description.abstractThe DPLL procedure is the basis of some of the most successful propositional satisfiability solvers to date. Although originally devised as a proof-procedure for first-order logic, it has been used almost exclusively for propositional logic so far because of its highly inefficient treatment of quantifiers, based on instantiation into ground formulas. The FDPLL calculus by Baumgartner was the first successful attempt to lift the procedure to the first-order level without resorting to ground instantiations. FDPLL lifts to the first-order case the core of the DPLL procedure, the splitting rule, but ignores other aspects of the procedure that, although not necessary for completeness, are crucial for its effectiveness in practice. In this paper, we present a new calculus loosely based on FDPLL that lifts these aspects as well. In addition to being a more faithful lifting of the DPLL procedure, the new calculus contains a more systematic treatment of universal literals, which are crucial to achieve efficiency in practice. The new calculus has been implemented successfully in the Darwin system, described elsewhere. The main results of this paper are theoretical, showing the soundness and completeness of the new calculus. In addition, the paper provides a high-level description of a proof procedure for the calculus, as well as a comparison with other calculi.
dc.publisherElsevier
dc.sourceArtificial Intelligence
dc.subjectKeywords: Algorithms; Calculations; Darwin system; Model generation; Logic programming DPLL procedure; First-order logic; Model generation; Sequent calculi
dc.titleThe model evolution calculus as a first-order DPLL method
dc.typeJournal article
local.description.notesImported from ARIES
local.identifier.citationvolume172
dc.date.issued2008
local.identifier.absfor080199 - Artificial Intelligence and Image Processing not elsewhere classified
local.identifier.ariespublicationu8803936xPUB198
local.type.statusPublished Version
local.contributor.affiliationBaumgartner, Peter, College of Engineering and Computer Science, ANU
local.contributor.affiliationTinelli, Cesare, University of Iowa
local.description.embargo2037-12-31
local.bibliographicCitation.issue4-5
local.bibliographicCitation.startpage591
local.bibliographicCitation.lastpage632
local.identifier.doi10.1016/j.artint.2007.09.005
dc.date.updated2015-12-09T08:04:51Z
local.identifier.scopusID2-s2.0-38149014645
local.identifier.thomsonID000253329500009
CollectionsANU Research Publications

Download

File Description SizeFormat Image
01_Baumgartner_The_model_evolution_calculus_2008.pdf769.59 kBAdobe PDF    Request a copy


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator