# Item

ITEM ACTIONSEXPORT

Released

Journal Article

#### Refutational Theorem Proving for Hierarchic First-Order Theories

##### MPS-Authors

##### Locator

There are no locators available

##### Fulltext (public)

There are no public fulltexts available

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Bachmair, L., Ganzinger, H., & Waldmann, U. (1994). Refutational Theorem Proving
for Hierarchic First-Order Theories.* Applicable Algebra in Engineering, Communication and Computing
(Aaecc),* *5*(3/4), 193-212.

Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-AD9C-E

##### Abstract

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.