Superposition for Fixed Domains

Details Superposition for Fixed Domains Superposition for Fixed Domains

2008-09-04

arxiv.org/abs/0809.0922v3

Computer Science

Artificial Intelligence

34 pages; to appear in ACM Transactions on Computational Logic

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

Superposition for Fixed Domains does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Superposition for Fixed Domains, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Superposition for Fixed Domains will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-658470