A Tableaux Method for Systematic Simultaneous Search for Refutations and Models using Equational Problems

Publisher Website
Google Scholar
Abstract
The problem of model construction is known to be a very important one. An extension of semantic tableaux (that can also be applied to the matings and to the connection method) allowing the building of models in a systematic way is presented. This approach is different from the usual one in semantic tableaux, in which model construction is a by-product of refutation failures (and this only in very particular cases). In fact, we incorporate in the object level, reasoning usually done in an ad hoc manner in the meta-level. Some of the rules introduced by this extension are essentially new. The impossibility of simulating them by the standard tableaux rules and their necessity in extending the class of captured models is shown. These rules and the modified classical ones are based on the use of equational problems. Equational problems are formulae containing only equalities and inequalities, connected by ‘and’, ‘or’ and quantified in a particular way. The method preserves the refutational completeness of semantic tableaux. It subsumes in a simpler and more powerful framework other enhancements such as the incorporation of unification. An algorithm for simultaneous search of refutations and models with extended semantic tableaux is given. One non-trivial example is treated in detail. A model is built for an example in which resolution-based procedures (i.e. resolution with ordering strategies) fails to detect satisfiability. It is also shown that in some cases our method is able to decide satisfiable formulae with only infinite models. Finally, a natural extension to some modal logics is presented.

This publication has 0 references indexed in Scilit: