Deduction by Combining Semantic Tableaux and Integer Programming

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 rst-order logic. The translation into clauses is done incrementally and is controlled by a semantic tableau procedure using uni cation. This amounts to an incremental polynomial CNF transformation which at the same time encodes part of the tableau structure and, therefore, tableau-speci c re nements that reduce the search space. Checking propositional unsatis ability 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.

• Type: Conference
• Year: 1995
• Where: CSL
• Authors: Bernhard Beckert, Reiner Hähnle
• Keywords: Automated Reasoning, CSL 1995, Integer Programming, Semantic Tableau Procedure