1999 | OriginalPaper | Buchkapitel
Solving Equational Problems Efficiently
verfasst von : Reinhard Pichler
Erschienen in: Automated Deduction — CADE-16
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Equational problems (i.e.: first-order formulae with quantifier prefix ∃* ∀*, whose only predicate symbol is syntactic equality) are an important tool in many areas of automated deduction, e.g.: restricting the set of ground instances of a clause via equational constraints allows the definition of stronger redundancy criteria and hence, in general, of more efficient theorem provers. Moreover, also the inference rules themselves can be restricted via constraints. In automated model building, equational problems play an important role both in the definition of an appropriate model representation and in the evaluation of clauses in such models. Also, many problems in the area of logic programming can be reduced to equational problem solving.The goal of this work is a complexity analysis of the satisfiability problem of equational problems in CNF over an infinite Herbrand universe. The main result will be a proof of the NP-completeness (and, in particular, of the NP-membership) of this problem.