Deduction by Combining Semantic Tableaux and Integer Programming

Abstract In this paper we propose to extend the current capabilities of automated reasoning systems by making use of techniques from integer programming. We describe the architecture of an automated reasoning system based on a Herbrand procedure (enumeration of formula instances) on clauses. The input are arbitrary sentences of first-order logic. The translation into clauses is done incrementally and is controlled by a semantic tableau procedure using unification. This amounts to an incremental polynomial CNF transformation which at the same time encodes part of the tableau structure and, therefore, tableau-specific refinements that reduce the search space. Checking propositional unsatisfiability of the resulting sequence of clauses can either be done with a symbolic inference system such as the Davis-Putnam procedure or it can be done using integer programming. If the latter is used a number of advantages become apparent.

Authors

• Bernhard Beckert
• Reiner Hähnle

Keywords

No keywords are indexed for this paper.