Efficient Equational Reasoning for the Inst-Gen Framework

Access to files

•   FULL-TEXT.PDF (pdf)

Abstract

We can classify several quite different calculi for automated reasoning in first-order logic as instantiation-based methods (IMs). Broadly speaking, unlike in traditional calculi such as resolution where the first-order satisfiability problem is tackled by deriving logical conclusions, IMs attempt to reduce the first-order satisfiability problem to propositional satisfiability by intelligently instantiating clauses. The Inst-Gen-Eq method is an instantiation-based calculus which is complete for first-order clause logic modulo equality. Its distinctive feature is that it combines first-order reasoning with efficient ground satisfiability checking, which is delegated in a modular way to any state-of-the-art ground solver for satisfiability modulo theories (SMT). The first-order reasoning modulo equality employs a superposition-style calculus which generates the instances needed by the ground solver to refine a model of a ground abstraction or to witness unsatisfiability. The thesis addresses the main issue in the Inst-Gen-Eq method, namely efficient extraction of instances, while providing powerful redundancy elimination techniques. To that end we introduce a novel labelled unit superposition calculus with sets, AND/OR trees and ordered binary decision diagrams (OBDDs) as labels. The different label structures permit redundancy elimination each to a different extent. We prove completeness of redundancy elimination from labels and further integrate simplification inferences based on term rewriting. All presented approaches, in particular the three labelled calculi are implemented in the iProver-Eq system and evaluated on standard benchmark problems.

Layman's Abstract

How can we be sure that software which we entrust more and more vital tasks to is free of flaws? Incidents of software maliciously being exploited or accidentally failing have had consequences that range from severe financial losses to threats to the lives of people. Good engineering is just a weak safeguard, and in particular in an ever faster paced and more complex world no guarantee that no flaw in the final product has been overlooked. Only formal verification can prove that a program will always behave as specified or that a specification is actually without loopholes. Unfortunately, verification of real world applications is tantamount to finding a needle in a haystack. The problems are too large and too complex to tackle for any one person even with all human intuition and creativity. This is where automated reasoning comes in. It offers a mechanisation of the process of finding logical conclusions, sifting through the haystack and in relevant practical cases actually finding a needle. Then, either defects in the implementation or specification can be fixed, or the reliability of the software has been formally established. This research is focused on a recent approach to automated reasoning that has already shown success in a range of cases. The goal is to allow specifications to use more expressive theories, leading to more concise formulations, in turn making the automated reasoning process more powerful. Ultimately, automated reasoning for verification will have an integral place in design processes, resulting in better and safer software.

Keyword(s)

automated reasoning; equational reasoning; first-order logic; instantiation-based methods

Bibliographic metadata

Institutional metadata

Record metadata