Logic in Computer Science (LICS 1996)

Paper: Basic Paramodulation and Decidable Theories (at LICS 1996)

Authors: Robert Nieuwenhuis

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 we prove decidability of the full first-order theory of the corresponding quotient term algebra.

BibTeX

  @InProceedings{Nieuwenhuis-BasicParamodulation,
    author = 	 {Robert Nieuwenhuis},
    title = 	 {Basic Paramodulation and Decidable Theories},
    booktitle =  {Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1996},
    year =	 1996,
    editor =	 {Edmund M. Clarke},
    month =	 {July}, 
    pages =      {473-482},
    location =   {New Brunswick, NJ, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }