Automated theorem proving is a method to establish or disprove logical theorems. While these can be theorems in the classical mathematical sense, we are more concerned with logical encodings of properties of algorithms, hardware and software. Especially in the area of hardware verification, propositional logic is used widely in industry. Satisfiability Module Theories (SMT) is a set of logics which extend propositional logic with theories relevant for specific application domains. In particular, software verification has received much attention, and efficient algorithms have been devised for reasoning over arithmetic and data types. Built-in support for theories by decision procedures is often significantly more efficient than reductions to propositional logic (SAT). Most efficient SAT solvers are based on the DPLL architecture, which is also the basis for most efficient SMT solvers. The main shortcoming of both kinds of logics is the weak support for non-ground reasoning, which noticeably limits the applicability to real world systems.
The Model Evolution Calculus (ME) was devised as a lifting of the DPLL architecture from the propositional setting to full first-order logic. In previous work, we created the solver Darwin as an implementation of ME, and showed how to adapt improvements from the DPLL setting. The first half of this thesis is concerned with ME and Darwin. First, we lift a further crucial ingredient of SAT and SMT solvers, lemma-learning, to Darwin and evaluate its benefits. Then, we show how to use Darwin for finite model finding, and how this application benefits from lemma-learning.
In the second half of the thesis we present Model Evolution with Linear Integer Arithmetic (MELIA), a calculus combining function-free first-order logic with linear integer arithmetic (LIA). MELIA is based on ME and supports similar inference rules and redundancy criteria. We prove the correctness of the calculus, and show how to obtain complete proof procedures and decision procedures for some interesting classes of MELIA's logic. Finally, we explain in detail how MELIA can be implemented efficiently based on the techniques employed in SMT solvers and Darwin.
| Identifer | oai:union.ndltd.org:uiowa.edu/oai:ir.uiowa.edu:etd-1546 |
| Date | 01 December 2009 |
| Creators | Fuchs, Alexander |
| Contributors | Tinelli, C. (Cesare) |
| Publisher | University of Iowa |
| Source Sets | University of Iowa |
| Language | English |
| Detected Language | English |
| Type | dissertation |
| Format | application/pdf |
| Source | Theses and Dissertations |
| Rights | Copyright 2009 Alexander Fuchs |
Page generated in 0.0021 seconds