## Tractable inference systems: an extension with a deducibility predicate

** Tractable inference systems: an extension with a deducibility predicate**. Hubert Comon-Lundh, Véronique Cortier, and Guillaume Scerri. In * Proceedings of the 25th International
Conference on Automated Deduction (CADE'13)*, pp. 91–108, Lecture Notes in Computer Science 7898, Springer, Lake Placid, USA, June 2013.

### Download

### Abstract

The main contribution of the paper is a PTIME decision procedure for the satisfiability problem in a class of first-order Horn clauses.
Our result is an extension of the tractable classes of Horn clauses of Basin & Ganzinger in several respects.
For instance, our clauses may contain atomic formulas S |- t where |- is a predicate symbol and S is a finite set of terms instead of a term.
|- is used to represent any possible computation of an attacker, given a set of messages S.
The class of clauses that we consider encompasses the clauses designed by Bana & Comon-Lundh for security proofs of protocols in a computational model.

Because of the (variadic) |- predicate symbol, we cannot use ordered resolution strategies only, as in Basin & Ganzinger: given S |- t, we must avoid computing S' |- t for all subsets S' of S. Instead, we design PTIME entailment procedures for increasingly expressive fragments, such procedures being used as oracles for the next fragment.

Finally, we obtain a PTIME procedure for arbitrary ground clauses and saturated Horn clauses (as in Basin & Ganzinger), together with a particular class of (non saturated) Horn clauses with the |- predicate and constraints (which are necessary to cover the application).

### BibTeX

@InProceedings{cade2013, abstract = {The main contribution of the paper is a PTIME decision procedure for the satisfiability problem in a class of first-order Horn clauses. Our result is an extension of the tractable classes of Horn clauses of Basin & Ganzinger in several respects. For instance, our clauses may contain atomic formulas S |- t where |- is a predicate symbol and S is a finite set of terms instead of a term. |- is used to represent any possible computation of an attacker, given a set of messages S. The class of clauses that we consider encompasses the clauses designed by Bana & Comon-Lundh for security proofs of protocols in a computational model. \par Because of the (variadic) |- predicate symbol, we cannot use ordered resolution strategies only, as in Basin \& Ganzinger: given S |- t, we must avoid computing S' |- t for all subsets S' of S. Instead, we design PTIME entailment procedures for increasingly expressive fragments, such procedures being used as oracles for the next fragment. \par Finally, we obtain a PTIME procedure for arbitrary ground clauses and saturated Horn clauses (as in Basin & Ganzinger), together with a particular class of (non saturated) Horn clauses with the |- predicate and constraints (which are necessary to cover the application).}, author = {Hubert Comon-Lundh and V\'eronique Cortier and Guillaume Scerri}, title = {Tractable inference systems: an extension with a deducibility predicate}, booktitle = {{P}roceedings of the 25th {I}nternational {C}onference on {A}utomated {D}eduction ({CADE}'13)}, pages = {91-108}, year = {2013}, OPTeditor = {}, volume = {7898}, OPTnumber = {}, series = {Lecture Notes in Computer Science}, address = {Lake Placid, USA}, month = {June}, OPTorganization = {}, publisher = {Springer}, DOI = {10.1007/978-3-642-38574-2_6}, }