hide
Free keywords:
-
Abstract:
Superposition is an established decision procedure for a variety of first-order
logic theories represented by sets of clauses. A satisfiable theory, saturated
by superposition, implicitly defines a minimal Herbrand model for the theory.
This raises the question in how far superposition calculi can be employed for
reasoning about such minimal models. This is indeed often possible when
existential properties are considered. However, proving universal properties
directly leads to a modification of the minimal model's term-generated domain,
as new Skolem functions are introduced. For many applications, this is not
desired because it changes the problem.
In this thesis, I propose the first superposition calculus that can explicitly
represent existentially quantified variables and can thus compute with respect
to a given fixed domain. It does not eliminate existential variables by
Skolemization, but handles them using additional constraints with which each
clause is annotated. This calculus is sound and refutationally complete in the
limit for a fixed domain semantics. For saturated Horn theories and classes of
positive formulas, the calculus is even complete for proving properties of the
minimal model itself, going beyond the scope of known superposition-based
approaches.
The calculus is applicable to every set of clauses with equality and does not
rely on any syntactic restrictions of the input. Extensions of the calculus
lead to various new decision procedures for minimal model validity. A main
feature of these decision procedures is that even the validity of queries
containing one quantifier alternation can be decided. In particular, I prove
that the validity of any formula with at most one quantifier alternation is
decidable in models represented by a finite set of atoms and that the validity
of several classes of such formulas is decidable in models represented by
so-called disjunctions of implicit generalizations. Moreover, I show that the
decision of minimal model validity can be reduced to the superposition-based
decision of first-order validity for models of a class of predicative Horn
clauses where all function symbols are at most unary.
