\begin{thebibliography}{12}
\providecommand{\natexlab}[1]{#1}
\providecommand{\url}[1]{\texttt{#1}}
\expandafter\ifx\csname urlstyle\endcsname\relax
  \providecommand{\doi}[1]{doi: #1}\else
  \providecommand{\doi}{doi: \begingroup \urlstyle{rm}\Url}\fi

\bibitem[Barras et~al.(1999--2003)Barras, Boutin, Cornes, Courant,
  Filli{\^a}tre, Gim{\'e}nez, Herbelin, Huet, Mu{\~n}oz, Murthy, Parent,
  Paulin-Mohring, Saibi, and Werner]{Coq74}
B.~Barras, S.~Boutin, C.~Cornes, J.~Courant, J.-C. Filli{\^a}tre,
  E.~Gim{\'e}nez, H.~Herbelin, G.~Huet, C.~Mu{\~n}oz, C.~Murthy, C.~Parent,
  C.~Paulin-Mohring, A.~Saibi, and B.~Werner.
\newblock The {C}oq proof assistant reference manual: Version 7.4.
\newblock Rapport technique, INRIA, France, 1999--2003.
\newblock \url{http://coq.inria.fr/doc/main.html}.

\bibitem[Blanchet(2001)]{Blanchet:Prolog}
B.~Blanchet.
\newblock An efficient cryptographic protocol verifier based on {P}rolog rules.
\newblock In \emph{14th IEEE Computer Security Foundations Workshop (CSFW-14)},
  pages 82--96. IEEE Computer Society Press, 2001.

\bibitem[Boudet and Comon(1996)]{ComonBoudet:Presburger}
A.~Boudet and H.~Comon.
\newblock Diophantine equations, {P}resburger arithmetic and finite automata.
\newblock In H.~Kirchner, editor, \emph{Colloquium on Trees in Algebra and
  Programming (CAAP'96)}, pages 30--43. Springer Verlag LNCS 1059, 1996.

\bibitem[Devienne et~al.(1996)Devienne, Leb{\`e}gue, Parrain, Routier, and
  W{\"u}rtz]{3French:oneclause}
P.~Devienne, P.~Leb{\`e}gue, A.~Parrain, J.-C. Routier, and J.~W{\"u}rtz.
\newblock Smallest {H}orn clause programs.
\newblock \emph{Journal of Logic Programming}, 27\penalty0 (3):\penalty0
  227--267, 1996.
\newblock URL \url{citeseer.nj.nec.com/devienne94smallest.html}.

\bibitem[Fr{\"u}hwirth et~al.(1991)Fr{\"u}hwirth, Shapiro, Vardi, and
  Yardeni]{FSVY:Prolog:types=programs}
T.~Fr{\"u}hwirth, E.~Shapiro, M.~Y. Vardi, and E.~Yardeni.
\newblock Logic programs as types for logic programs.
\newblock In \emph{Proc.\ 6th Symp Logic in Computer Science}, pages 300--309,
  1991.

\bibitem[Goubault{-}Larrecq(2005)]{JGL:H1}
J.~Goubault{-}Larrecq.
\newblock Deciding {\(\mathcal{\MakeUppercase{h}}_1\)} by resolution.
\newblock \emph{Information Processing Letters}, 95\penalty0 (3):\penalty0
  401--408, Aug. 2005.
\newblock URL
  \url{http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Goubault-h1.pdf}.

\bibitem[Goubault-Larrecq(2004)]{JGL:JFLA04}
J.~Goubault-Larrecq.
\newblock Une fois qu'on n'a pas trouv{\'e} de preuve, comment le faire
  comprendre {\`a} un assistant de preuve~?
\newblock In \emph{Actes 15{\`e}mes journ{\'e}es francophones sur les langages
  applicatifs (JFLA'04), Sainte-Marie-de-R{\'e}, France, Jan.\ 2004}, pages
  1--20. INRIA, collection didactique, 2004.
\newblock URL \url{http://www.lsv.ens-cachan.fr/Publis/PAPERS/JGL-JFLA2004.ps}.

\bibitem[Goubault{-}Larrecq and Parrennes(2005)]{GLP:VMCAI}
J.~Goubault{-}Larrecq and F.~Parrennes.
\newblock Cryptographic protocol analysis on real {C}~code.
\newblock In R.~Cousot, editor, \emph{{P}roceedings of the 6th {I}nternational
  {C}onference on {V}erification, {M}odel {C}hecking and {A}bstract
  {I}nterpretation ({VMCAI}'05)}, volume 3385 of \emph{Lecture Notes in
  Computer Science}, Paris, France, Jan. 2005. Springer.
\newblock URL
  \url{http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GouPar-VMCAI2005.pdf}.
\newblock To appear.

\bibitem[Nielson et~al.(2002)Nielson, Nielson, and Seidl]{NNS:H1}
F.~Nielson, H.~R. Nielson, and H.~Seidl.
\newblock Normalizable {H}orn clauses, strongly recognizable relations and
  {S}pi.
\newblock In \emph{9th Static Analysis Symposium (SAS)}. Springer Verlag LNCS
  2477, 2002.

\bibitem[Pelletier(1986)]{Pelletier:75pbs}
F.~J. Pelletier.
\newblock Seventy-five problems for testing automatic theorem provers.
\newblock \emph{Journal of Automated Reasoning}, 2:\penalty0 191--216, 1986.

\bibitem[Selinger(2001)]{Selinger:LACPV}
P.~Selinger.
\newblock Models for an adversary-centric protocol logic.
\newblock \emph{Electronic Notes in Theoretical Computer Science}, 55\penalty0
  (1):\penalty0 73--87, 2001.
\newblock Proceedings of the 1st Workshop on Logical Aspects of Cryptographic
  Protocol Verification (LACPV'01), J. Goubault-Larrecq, ed.

\bibitem[Suttner and Sutcliffe(2002)]{SS:TPTP}
C.~B. Suttner and G.~Sutcliffe.
\newblock The {TPTP} problem library v2.5.0, 2002.
\newblock URL \url{http://www.cs.miami.edu/~tptp/TPTP/TR/TPTPTR.shtml}.

\end{thebibliography}
