The Model Evolution Calculus - A First-Order DPLL Procedure
Prof. Peter Baumgartner (Max Planck Institute)
CSL SEMINAR SERIESDATE: 2004-11-15
TIME: 16:00:00 - 17:00:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
The Davis-Putnam-Logemann-Loveland procedure (DPLL) was brought forward in the early 60s as a method for first-order theorem proving. It works by enumerating ground instances of first-order clauses and feeding them into the propositional part of the procedure (which is the well-known basis of many contemporary SAT solvers). Because of this decoupled processing, variables do not play an active role during the proof search in the propositional part, and the problem of intelligently enumerating ground instances arises.
Starting from this observation I developed a "proper" first-order DPLL method (FDPLL). It is motivated by lifting some of these very effective techniques developed for the propositional part of DPLL to the first-order level in conjunction with exploiting successful first-order theorem proving techniques like unification and subsumption.
The FDPLL calculus has been refined and improved by, e.g., incorporating DPLL style simplification rules. The resulting method we call the Model Evolution Calculus (it is joint work with Prof. Cesare Tinelli from the University of Iowa, USA).
In the talk I will give an overview of the calculus and mention performance results obtained with its implementation, the Darwin system ( http://www.mpi-sb.mpg.de/~baumgart/DARWIN/ ). I will also report on recent work on extending the calculus with an interface for theory reasoning, which allows to couple specialized reasoners for specific theories (e.g. the Waldmeister prover for equality reasoning). Finally, I will briefly discuss an application of the calculus as the core component of a decision procedure for a fragment of first-order Autoepistemic Logic.
