# Item

ITEM ACTIONSEXPORT

Released

Report

#### Superposition for Fixed Domains

##### MPS-Authors

##### Locator

There are no locators available

##### Fulltext (public)

superFixDom_TR.pdf

(Any fulltext), 334KB

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Horbach, M., & Weidenbach, C.(2009). *Superposition for
Fixed Domains* (MPI-I-2009-RG1-005). Saarbrücken: Max-Planck-Institut für Informatik.

Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-1A71-C

##### 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 term-generated model for the
theory.
Proving universal properties with respect to a saturated theory 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.
Therefore, we propose the first superposition calculus that can explicitly
represent existentially quantified variables and can thus compute with respect
to a given domain. This calculus is sound and refutationally complete in the
limit for a first-order fixed domain semantics.
For saturated Horn theories and classes of positive formulas, we can even
employ the calculus to prove properties of the minimal model itself, going
beyond the scope of known superposition-based approaches.