Datensatz

Zusammenfassung

We extend previous results on theorem proving for first-order clauses with
equality to hierarchic first-order theories. Semantically such theories are
confined to conservative extensions of the base models. It is shown that
superposition together with variable abstraction and constraint refutation is
refutationally complete for theories that are sufficiently complete with
respect to simple instances. For the proof we introduce a concept of
approximation between theorem proving systems, which makes it possible to
reduce the problem to the known case of (flat) first-order theories. These
results allow the modular combination of a superposition-based theorem prover
with an arbitrary refutational prover for the primitive base theory, whose
axiomatic representation in some logic may remain hidden. Furthermore they can
be used to eliminate existentially quantified predicate symbols from certain
second-order formulae.