A more efficient tableaux procedure for simultaneous search for refutations and finite models

Abstract

We describe a (many-sorted) tableaux procedure that has the following properties: it is sound, refutationally complete and complete for finite satisfiability (i.e. the procedure terminates if the formula hasa finite model). Asf or standard tableaux methods, models can be extracted from finite open branches. As similar existing procedures, our method relieson a modified δ-rule allowing to reuse existing variables occurring in the same branch. An original notion of complexity measure isi ntroduced in order to control the application of thisrul e (which is potentially time consuming). The procedure is semantically guided: an interpretation (provided by the user) is used for pruning the search space. Thisin terpretation isrefi ned dynamically during proof search until a model or a contradiction isf ound. The method hasb een implemented and some preliminary experimental results are presented.