@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@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},
}