Item

Abstract

A number of first-order calculi employ an explicit model representation
formalism for automated reasoning and for detecting satisfiability. Many of
these formalisms can represent infinite Herbrand models. The first-order
fragment of monadic, shallow, linear, Horn (MSLH) clauses, is such a formalism
used in the approximation refinement calculus. Our first result is a finite
model property for MSLH clause sets. Therefore, MSLH clause sets cannot
represent models of clause sets with inherently infinite models. Through a
translation to tree automata, we further show that this limitation also applies
to the linear fragments of implicit generalizations, which is the formalism
used in the model-evolution calculus, to atoms with disequality constraints,
the formalisms used in the non-redundant clause learning calculus (NRCL), and
to atoms with membership constraints, a formalism used for example in decision
procedures for algebraic data types. Although these formalisms cannot represent
models of clause sets with inherently infinite models, through an additional
approximation step they can. This is our second main result. For clause sets
including the definition of an equivalence relation with the help of an
additional, novel approximation, called reflexive relation splitting, the
approximation refinement calculus can automatically show satisfiability through
the MSLH clause set formalism.