@inproceedings{0ae9b2d133304489ae5ee9d8999d014f,
title = "On the complexity of equational Horn clauses",
abstract = "Security protocols employing cryptographic primitives with algebraic properties are conveniently modeled using Horn clauses modulo equational theories. We consider clauses corresponding to the class H3 of Nielson, Nielson and Seidl. We show that modulo the theory ACU of an associative-commutative symbol with unit, as well as its variants like the theory XOR and the theory AG of Abelian groups, unsatisfiability is NP-complete. Also membership and intersection-non-emptiness problems for the closely related class of one-way as well as two-way tree automata modulo these equational theories are NP-complete. A key technical tool is a linear time construction of an existential Presburger formula corresponding to the Parikh image of a context-free language. Our algorithms require deterministic polynomial time using an oracle for existential Presburger formulas, suggesting efficient implementations are possible.",
author = "Verma, {Kumar Neeraj} and Helmut Seidl and Thomas Schwentick",
year = "2005",
doi = "10.1007/11532231_25",
language = "English",
isbn = "3540280057",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "337--352",
booktitle = "Automated Deduction - CADE-20 - 20th International Conference on Automated Deduction, Proceedings",
note = "20th International Conference on Automated Deduction, CADE-20 ; Conference date: 22-07-2005 Through 27-07-2005",
}