Basic Paramodulation and Decidable Theories (Extended Abstract)
Robert Nieuwenhuis · 1996
) Robert Nieuwenhuis Technical University of Catalonia Pau Gargallo 5, 08028 Barcelona, Spain E-mail: [email protected]. 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 polynom...