Philipp Rümmer:
A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
Abstract: Abstract:
One of the main challenges in automated theorem proving is to combine reasoning about full first-order logic (including quantifiers) with reasoning about theories like the integers. At the time, there are efficient provers for handling formulae in first-order logic, as well as SMT-solvers that can efficiently handle ground problems modulo many theories, but the support for the combination of both is typically weak.
I introduce a novel sequent calculus for first-order logic modulo linear integer arithmetic that combines ideas from free-variable constraint tableaux (mostly building on the work by Martin Giese) with the Omega quantifier elimination procedure. The calculus is complete for theorems of first-order logic (without functions, but with arbitrary uninterpreted predicates) and can decide Presburger arithmetic. In addition, a substantial fragment of the combination of both can be handled, in particular many cases of formulae containing quantifiers where trigger-matching techniques fail. The calculus is complete for showing the unsatisfiability of formulae that only contain universal quantifiers and constants ranging over finite domains.
An implementation of the presented calculus ("Princess") is under development.
http://www.cs.chalmers.se/~philipp/publications/princess08.pdf
http://www.cs.chalmers.se/~philipp/princess/
Philipp Rümmer is a Ph.D. student at the Chalmers University of Technology in Gothenburg, Sweden. He received his M.Sc. in Computing Science in 2004 from the University of Karlsruhe in Germany and plans to defend his Ph.D. thesis in December. His current research interests include theorem proving in first-order logic and theories and deductive verification techniques for imperative and object-oriented programs. Philipp is member of the KeY project at Chalmers and is currently working as intern with Rustan Leino at the Microsoft Research Lab in Redmond (for the second time this year), developing the next version of the Boogie verification back-end.
Appointments:
dcm@cs.cmu.edu
|