Basic paramodulation and decidable theories
- 24 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 473-482
- https://doi.org/10.1109/lics.1996.561464
Abstract
We prove that for sets of Horn clauses saturated under basic paramodulation, the word and unifiability problems are in NP, and the number of minimal unifiers is simply exponential (i). For Horn sets saturated wrt. a special ordering under the more restrictive inference rule of basic superposition, the word and unifiability problems are still decidable and unification is finitary (ii). We define standard theories, which include and significantly extend shallow theories. Standard presentations can be finitely closed under superposition and result (ii) applies. Generalizing shallow theories to the Horn case, we obtain (two versions of) a language we call Catalog, a natural extension of Datalog to include functions and equality. The closure under paramodulation is finite for Catalog sets, hence (i) applies. Since for shallow sets this closure is even polynomial, shallow unifiability is in NP, which is optimal: unifiability in ground theories is already NP-hard. We even go beyond: the shallow word problem is tractable and for Catalog sets S we prove decidability of the full first-order theory of T(F)/=/sub s/.Keywords
This publication has 13 references indexed in Scilit:
- Superposition with simplification as a decision procedure for the monadic class with equalityPublished by Springer Nature ,2005
- The unifiability problem in ground AC theoriesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Set constraints are the monadic classPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Normalised rewriting and normalised completionPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Theorem Proving with Ordering and Equality Constrained ClausesJournal of Symbolic Computation, 1995
- On narrowing, refutation proofs and constraintsPublished by Springer Nature ,1995
- Syntacticness, Cycle-Syntacticness, and Shallow TheoriesInformation and Computation, 1994
- Ordered paramodulation and resolution as decision procedurePublished by Springer Nature ,1993
- Any ground associative-commutative theory has a finite canonical systemPublished by Springer Nature ,1991
- On ground AC-completionPublished by Springer Nature ,1991