Hyper tableau reasoning is a version of clausal form tableau reasoning where all negative literals in a clause are resolved away in a single inference step. Constrained hyper tableaux are a generalization of hyper tableaux, where branch closing substitutions, from the point of view of model generation, give rise to constraints on satisfying assignments for the branch. These variable constraints eliminate the need for the awkward ‘purifying substitutions’ of hyper tableaux. The paper presents a non-destructive and proof confluent calculus for (...) constrained hyper tableaux, together with a soundness and completeness proof, with completeness based on a new way to generate models from open tableaux. It is pointed out that the variable constraint approach applies to free variable tableau reasoning in general. (shrink)

An extension of tableaux is presented. The extension is threefold: a new rule allowing the use of information deduced during the building of the tableau in order to simplify formulae occurring in it, integration of semantic strategies that prune the search space and a new way of extracting a model for a given branch. These features are combined with a former method for simultaneous search for refutations and models. The capabilities of the new method w.r.t. the original one are clearly (...) stated. A non-trivial extension of the standard proof using Hintikka sets is introduced in order to prove the refutational completeness of our method.Finally, it is shown that the method is able to build models for any formula having a model that can be specified by equational constraints. This class contains many existing decidable classes of formulae such as the Bernays-Schönfinkel class, the PVD and OCC1N classes etc. (shrink)