Automated Reasoning in First-Order Logic Modulo Built-In Theories - The Hierarchic Superposition Calculus with Weak Abstraction
Peter Baumgartner (NICTA and ANU)
LOGIC AND COMPUTATION SEMINARDATE: 2013-05-28
TIME: 13:30:00 - 14:30:00
LOCATION: NICTA - 7 London Circuit
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
Many applications of automated deduction require reasoning in first-order logic modulo background theories. Analysing software systems, for instance, typically requires modelling data structures like lists, records and arrays in combination with some form of integer arithmetic. The practically most successful systems today for these applications are SMT solvers (Satisfiability Modulo Theories). SMT-solvers, however, are geared towards quantifier-free (ground) input formulas and often have difficulties with quantified formulas. This is an intrinsic limitation that is addressed only partially by the state-of-the-art, which relies on incomplete instantiation heuristics. On the other hand, quantified formulas are needed, e.g., to describe properties of the data structures at hand, e.g., that a given list is sorted. Not being able to properly deal with quantified formulas hence is a serious practical limitation.
From that point of view, automated reasoning methods for first-order logic look more promising as they natively support quantifiers. Adding support for reasoning with background theories to these methods has recently been an active area of research (again). The hierarchical superposition calculus mentioned in the title is our latest development in this direction BW13.
The theoretical limits - high undecidability - are, of course, the same for both approaches. From a technical point of view, the challenge hence is to provide reasoning support that is "reasonably complete" in practice, so that the systems can be used more reliably for both proving theorems and finding counterexamples.
In the talk I will explain the issues mentioned above in more detail, summarize the hierarchic superposition calculus, and outline the techniques to achieve completeness for certain fragments. I will also demonstrate our implementation of the hierarchic superposition calculus.
[ BW13 ] Peter Baumgartner and Uwe Waldmann. Hierarchic Superposition With Weak Abstraction. In Maria Paola Bonacina, editor, CADE-24 - The 24th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence. Springer, 2013. To appear.
BIO:
