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

[PDF] [HTML]

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},
}