摘要：
Equational problems (i.e.: first-order formulae with quantifier prefix 9 8 , whose only predicate symbol is syntactic equality) are an important tool in many areas of Computer Science like automated deduction, automated model building, logic programming, functional programming, etc. The aim of this work is a complexity analysis of the satisfiability problem of equational problems over a finite domain. Our main result is the Sigma p 2 -completeness proof for equational problems in CNF.
展開