Labelled Unit Superposition Calculi for Instantiation-Based Reasoning

8 years 3 months ago
Labelled Unit Superposition Calculi for Instantiation-Based Reasoning
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 SMT solver. 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 bstraction or to witness unsatisfiability. In this paper we present and compare different labelling mechanisms in the unit superposition calculus that facilitates finding the necessary instances. We demonstrate and evaluate how different label structures such as sets, AND/OR trees and OBDDs affect the interplay between the proof procedure and blocking mechanisms for redundancy elimination.
Konstantin Korovin, Christoph Sticksel
Added 29 Jan 2011
Updated 29 Jan 2011
Type Journal
Year 2010
Where LPAR
Authors Konstantin Korovin, Christoph Sticksel
Comments (0)