TITLE: A First-Order DPLL Procedure and an Application to Knowledge Representation

PRESENTER: Peter Baumgartner, Email: baumgart@mpi-sb.mpg.de

AFFILIATION: Max-Planck-Institut fuer Informatik Stuhlsatzenhausweg

DATE: Monday 8th November 2004

TIME: 2pm to 3pm

PLACE: CSE K17 1st Floor Seminar Room

ABSTRACT:

The Davis-Putnam-Logemann-Loveland procedure (DPLL) was brought forward in the early 60s as a method for first-order theorem proving. To this end, ground instances of first-order clauses are enumerated and fed into the propositional part of the procedure (which is the basis of many contemporary SAT solvers). Thus, variables do not play an active role during the proof search in the propositional part, and the problem of intelligently enumerating ground instances emerges.

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

The first part of the talk focuses on the Model Evolution Calculus: 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).

The Model Evolution Calculus and related so-called instance based methods share a distinguishing feature: unlike more traditional calculi like tableaux or resolution they are a natural decision procedure for the Bernays-Schoenfinkel (BS) fragment of first-order logic (which corresponds to clause logic without function symbols except constants). In the second part of the talk I will report on current work aiming at exploiting this feature for knowledge representation purposes. More specifically, I will sketch how to compute stable expansions for formulas of the Bernays-Schoenfinkelfragment of first-order autoepistemic logic by reduction to satisfiability of classical BS formulas. This logic seems interesting e.g. because it allows to embed a fragment of description logics extended by nonmonotonic language constructs in combination with logic programming style rules.

BIOGRAPHY OF SPEAKER:

Peter Baumgartner is a researcher at the Programming Logics Group at the Max-Planck Institute for Informatics in Saarbruecken. Previously he was at the University Koblenz-Landau where he worked with Prof. Uli Furbach.

HOST

Toby Walsh, Research Fellow, National ICT Australia and Professor at the Department of Computer Science and Engineering, UNSW, Sydney.

SEMINART CONVENER:

Bernhard Hengst
National ICT Australia, Symbolic Machine Learning & Knowledge Acquisition
Tel: +61-2-9385-6940