
@InProceedings{NNS:H1,
  author = 	 {Nielson, Flemming and Nielson, Hanne Riis and Seidl, Helmut},
  title = 	 {Normalizable {H}orn Clauses, Strongly Recognizable Relations and {S}pi},
  booktitle = 	 {9th Static Analysis Symposium (SAS)},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTpages = 	 {},
  year =	 {2002},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  publisher =	 {Springer Verlag LNCS 2477},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@techreport{Coq74,
    author          = {Barras, Bruno and Boutin, Samuel and Cornes, Cristina
        and Courant, Judica{\"e}l and Filli{\^a}tre, Jean-Christophe
        and Gim{\'e}nez, Eduardo and Herbelin, Hugo and Huet, G{\'e}rard
        and Mu{\~n}oz, Cesar and Murthy, Chetan and Parent, Catherine
        and Paulin-Mohring, Christine and Saibi, Amokrane
        and Werner, Benjamin},
    title           = {The {C}oq Proof Assistant Reference Manual: Version
        7.4},
    institution     = {INRIA, France},
    type            = {Rapport technique},
    year            = {1999--2003},
    note          = {\url{http://coq.inria.fr/doc/main.html}}
}

@Article{Selinger:LACPV,
  author = 	 {Selinger, Peter},
  title = 	 {Models for an Adversary-Centric Protocol Logic},
  journal = 	 {Electronic Notes in Theoretical Computer Science},
  year = 	 {2001},
  OPTkey = 	 {},
  volume =	 {55},
  number =	 {1},
  pages =	 {73--87},
  OPTmonth =	 jul,
  note =	 {Proceedings of the 1st Workshop on Logical Aspects of Cryptographic Protocol Verification (LACPV'01), J. Goubault-Larrecq, ed.},
  OPTannote = 	 {}
}

@InProceedings{JGL:JFLA04,
  author =       "Goubault-Larrecq, Jean",
  title =        "Une fois qu'on n'a pas trouv{\'e} de preuve, comment le
                 faire comprendre {\`a} un assistant de preuve~?",
  pages = "1--20",
  booktitle =    "Actes 15{\`e}mes journ{\'e}es francophones sur les langages
                 applicatifs (JFLA'04), Sainte-Marie-de-R{\'e}, France,
                 Jan.\ 2004",
  year =         "2004",
  publisher =    "INRIA, collection didactique",
  lsv-category = "invi",
  lsv-status =   "apar",
  URL =          "http://www.lsv.ens-cachan.fr/Publis/PAPERS/JGL-JFLA2004.ps",
  wwwpublic =    "public ccsb",
}

@InProceedings{ComonBoudet:Presburger,
  author = 	 {Boudet, Alexandre and Comon, Hubert},
  title = 	 {Diophantine Equations, {P}resburger Arithmetic and Finite Automata},
  booktitle = 	 {Colloquium on Trees in Algebra and Programming (CAAP'96)},
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages =	 {30--43},
  year =	 {1996},
  editor =	 {H{\'e}l{\`e}ne Kirchner},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  publisher =	 {Springer Verlag LNCS 1059},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@article{Stickel:ACUnif,
	AUTHOR = "Stickel, Mark",
	TITLE = "A Unification Algorithm for Associative-Commutative Functions",
	JOURNAL = "Journal of the Association for Computing Machinery",
	PAGES = "423--434",
	VOLUME = "28",
	NUMBER = "3",
	PUBLISHER = "{ACM}",
	MONTH = "July",
	YEAR = "1981"
	}

@inproceedings{Fages:ACUnif,
	AUTHOR = "Fages, Fran\c{c}ois",
	TITLE = "Associative-Commutative Unification",
	BOOKTITLE = "7th Intl. Conference on Automated Deduction",
	OPTSERIES = "Lecture Notes in Computer Science",
	OPTVOLUME = "170",
	PAGES = "194--208",
	PUBLISHER = "Springer Verlag LNCS 170",
	YEAR = "1984"
	}

@INPROCEEDINGS{AdvACUnification,
	AUTHOR = "Lincoln, Patrick and Christian, Jim",
	TITLE = "Adventures in Associative-Commutative Unification
		(A Summary)",
	CROSSREF = "CADE9",
	PAGES = "358--367"
	}

@Proceedings{CADE9,
  title = 	"9th Intl. Conference on Automated Deduction",
  booktitle = 	"9th Intl. Conference on Automated Deduction",
  year = 	"1988",
  editor = 	"Lusk, E. and Overbeek, R.",
  publisher = 	"Springer Verlag LNCS 310",
  OPTseries = "Lecture Notes in Computer Science",
  OPTvolume = "310",
  OPTorganization = 	"",
  OPTaddress = 	"Argonne, Illinois, USA",
  month = 	"May",
  OPTnote = 	""
}

@article{Plotkin:EqUnif,
	author = "Plotkin, Gordon",
	title = "Building in Equational Theories",
	journal = "Machine Intelligence",
	volume = "7",
	number = "",
	pages = "73--90",
	year = "1972"
	}

@BOOK{ChangLee,
	AUTHOR = "Chang, Chin-Liang and Lee, Richard Char-Tung",
	TITLE = "Symbolic Logic and Mechanical Theorem Proving",
	SERIES = "Computer Science Classics",
	PUBLISHER = "Academic Press",
	YEAR = "1973"
	}

@InCollection{BG:HAR,
  author =	 {Bachmair, Leo and Ganzinger, Harald},
  ALTeditor =	 {},
  title = 	 {Resolution Theorem Proving},
  booktitle = 	 {Handbook of Automated Reasoning},
  chapter = 	 {2},
  pages = "19--99",
  crossref = "HAR",
  publisher = 	 {North-Holland},
  year = 	 {2001},
  volume = "I",
  OPTyear = 	 {},
  OPTkey = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTtype = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTpages = 	 {},
  OPTnote =	 {In \cite{HAR}},
  OPTannote = 	 {}
}

@Book{HAR,
  ALTauthor = 	 {},
  editor =	 {Robinson, J. Alan and Voronkov, Andrei},
  title = 	 {Handbook of Automated Reasoning},
  publisher = 	 {North-Holland},
  year = 	 {2001},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{Vampire,
  author = 	 {Riazanov, Alexandre and Voronkov, Andrei},
  title = 	 {Vampire 1.1 (System Description)},
  booktitle = 	 {1st Intl.\ Joint Conf.\ Automated Reasoning (IJCAR)},
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages =	 {376--380},
  crossref = "IJCAR01",
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{Voronkov:IJCAR,
  author = 	 {Voronkov, Andrei},
  title = 	 {Algorithms, Datastructures, and Other Issues in Efficient Automated Deduction},
  booktitle = 	 {1st Intl.\ Joint Conference on Automated Reasoning (IJCAR'01)},
  pages = "13--28",
  crossref =	 {IJCAR01},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTorganization = {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Proceedings{IJCAR01,
  title = 	 {1st Intl.\ Joint Conference on Automated Reasoning (IJCAR'01)},
  year = 	 {2001},
  OPTkey = 	 {},
  editor =	 {Gor{\'e}, Rajeev and Leitsch, Alexander and Nipkow, Tobias},
  address =	 {Siena, Italy},
  month =	 jun,
  OPTorganization = {},
  publisher =	 {Springer Verlag LNAI 2083},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Article{Joyner:dec,
  author =       "Joyner Jr., William H.",
  title =        "Resolution Strategies as Decision Procedures",
  journal =      "Journal of the Association for Computing Machinery",
  volume =       "23",
  number =       "3",
  pages =        "398--417",
  month =        jul,
  year =         "1976",
  coden =        "JACOAH",
  ISSN =         "0004-5411",
  bibdate =      "Wed Jan 15 18:12:53 MST 1997",
  abstract =     "The resolution principle, an automatic inference
                 technique, is studied as a possible decision procedure
                 for certain classes of first-order formulas. It is
                 shown that most previous resolution strategies do not
                 decide satisfiability even for ``simple'' solvable
                 classes. Two new resolution procedures are described
                 and are shown to be complete (i.e. semidecision
                 procedures) in the general case and, in addition, to be
                 decision procedures for successively wider classes of
                 first-order formulas. These include many previously
                 studied solvable classes. The proofs that a complete
                 resolution procedure will always halt (without
                 producing the empty clause) when applied to satisfiable
                 formulas in certain classes provide demonstrations of
                 the solvability of these classes. A technique for
                 constructing a model for a formula shown satisfiable in
                 this way is also described.",
  acknowledgement = ack-nhfb,
  classification = "723; 912",
  journalabr =   "J Assoc Comput Mach",
  keywords =     "computer metatheory --- Programming Theory; systems
                 science and cybernetics",
}

@article{3French:oneclause,
    author = "Devienne, Philippe and Leb{\`e}gue, Patrick and Parrain, A. and Routier,  Jean-Christophe and W{\"u}rtz, J{\"o}rg",
    title = "Smallest {H}orn Clause Programs",
    journal = "Journal of Logic Programming",
    volume = "27",
    number = "3",
    pages = "227-267",
    year = "1996",
    url = "citeseer.nj.nec.com/devienne94smallest.html" }

@InProceedings{SPASS,
  author = 	 {Weidenbach, Christoph and Brahm, Uwe and Hillenbrand, Thomas and Keen, Enno and Theobald, Christian and Topi{\'c}, Dalibor},
  title = 	 {{SPASS} Version 2.0},
  booktitle = 	 {Proceedings of the 18th International Conference on Automated Deduction},
  crossref =	 "CADE18",
  OPTkey = 	 {},
  OPTpages = 	 {},
  year =	 {2002},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Proceedings{CADE18,
  title = 	 {Proceedings of the 18th International Conference on Automated Deduction},
  year = 	 {2002},
  OPTkey = 	 {},
  editor =	 {Voronkov, A.},
  OPTvolume =	 {2392},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  publisher =	 {Springer-Verlag LNAI 2392},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@MISC{SS:TPTP,
  AUTHOR = {Suttner, Christian B. and Sutcliffe, Geoff},
  TITLE = {The {TPTP} Problem Library v2.5.0},
  URL = {http://www.cs.miami.edu/~tptp/TPTP/TR/TPTPTR.shtml},
  YEAR = {2002}
}

@TechReport{LRI:UnifSurvey,
  author = 	"Jouannaud, Jean-Pierre and Kirchner, Claude",
  title = 	"Solving Equations in Abstract Algebras: a Rule-Based
		 Survey of Unification",
  institution = 	"{LRI}, {CNRS UA} 410: Al Khowarizmi",
  year = 	"1990",
  OPTtype = 	"",
  OPTnumber = 	"",
  OPTaddress = 	"",
  month = 	mar,
  OPTnote = 	""
}

@PhdThesis{deNivelle:PhD,
  author = 	 {de Nivelle, Hans},
  title = 	 {Ordering Refinements of Resolution},
  school = 	 {Technische Universiteit Delft},
  year = 	 {1995},
  OPTkey = 	 {},
  OPTtype = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Article{KH:semtree,
  author = 	 {Kowalski, Robert and Hayes, P. J.},
  title = 	 {Semantic Trees in Automatic Theorem-Proving},
  journal = 	 {Machine Intelligence},
  year = 	 {1969},
  OPTkey = 	 {},
  volume =	 {4},
  OPTnumber = 	 {},
  pages =	 {87--101},
  OPTmonth = 	 {},
  note =	 {Reprinted in \cite{SW:classic2}},
  OPTannote = 	 {}
}

@Book{SW:classic2,
  ALTauthor = 	 {},
  editor =	 {Siekmann, J{\"o}rg and Wrightson, Graham},
  title = 	 {Automation of Reasoning: Classical Papers in Computational Logic},
  publisher = 	 {Springer Verlag},
  year = 	 {1983},
  OPTkey = 	 {},
  volume =	 {2, 1967--1970},
  OPTnumber =	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Article{JGL:H1,
  author = 	 {Goubault-Larrecq, Jean},
  title = 	 {Deciding {$\mathcal H_1$} by Resolution},
  journal = 	 {Information Processing Letters},
  year = 	 {2005},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTpages = 	 {},
  OPTmonth = 	 {},
  note =	 {Submitted},
  OPTannote = 	 {}
}

@InCollection{Blanchet:prolog,
  author = 	 {Blanchet, Bruno},
  title = 	 {An Efficient Cryptographic Protocol Verifier Based on {P}rolog Rules},
  booktitle = 	 {14th IEEE Computer Security Foundations Workshop (CSFW-14)},
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages =	 {82--96},
  publisher =	 {IEEE Computer Society Press},
  year =	 {2001},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTtype = 	 {},
  OPTchapter = 	 {},
  OPTaddress =	 {Cape Breton, Nouvelle-{\'E}cosse, Canada},
  OPTedition = 	 {},
  OPTmonth =	 jun,
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Article{Pelletier:75pbs,
  author = 	"Pelletier, Francis Jeffry",
  title = 	"Seventy-Five Problems for Testing Automatic Theorem Provers",
  journal = 	"Journal of Automated Reasoning",
  year = 	"1986",
  volume = 	"2",
  OPTnumber = 	"",
  pages = 	"191--216",
  OPTmonth = 	"",
  OPTnote = 	""
}

@INPROCEEDINGS{Satchmo,
	AUTHOR = "Manthey, Rainer and Bry, Fran\c{c}ois",
	TITLE = "{SATCHMO}: a theorem prover implemented in {P}rolog",
	CROSSREF = "CADE9",
	PAGES = "415--434"
	}

@Proceedings{CADE9,
  title = 	"9th International Conference on Automated Deduction",
  booktitle = 	"9th International Conference on Automated Deduction",
  year = 	"1988",
  editor = 	"Lusk, E. and Overbeek, R.",
  publisher = 	"Springer Verlag LNCS 310",
  OPTseries = "Lecture Notes in Computer Science",
  OPTvolume = "310",
  OPTorganization = 	"",
  address = 	"Argonne, Illinois, USA",
  month = 	may,
  OPTnote = 	""
}

@inproceedings{GLP:VMCAI,
  abstract =      {Implementations of cryptographic protocols, such as
                   OpenSSL for example, contain bugs affecting security,
                   which cannot be detected by just analyzing abstract
                   protocols (e.g., SSL or TLS). We describe how
                   cryptographic protocol verification techniques based
                   on solving clause sets can be applied to detect
                   vulnerabilities of C programs in the Dolev-Yao model,
                   statically. This involves integrating fairly simple
                   pointer analysis techniques with an analysis of which
                   messages an external intruder may collect and forge.
                   This also involves relating concrete run-time data
                   with abstract, logical terms representing messages.
                   To this end, we make use of so-called trust
                   assertions. The output of the analysis is a set of
                   clauses in the decidable class H1, which can then be
                   solved independently. This can be used to establish
                   secrecy properties, and to detect some other bugs.},
  address =       {Paris, France},
  author =        {Goubault{-}Larrecq, Jean and Parrennes, Fabrice},
  booktitle =     {{P}roceedings of the 6th {I}nternational {C}onference
                   on {V}erification, {M}odel {C}hecking and {A}bstract
                   {I}nterpretation ({VMCAI}'05)},
  editor =        {Cousot, Radhia},
  month =         jan,
  note =          {To appear},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  title =         {Cryptographic Protocol Analysis on Real {C}~Code},
  volume =        {3385},
  year =          {2005},
  nmonth =        {1},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GouPar-VMCAI2005.pdf},
  lsv-category =  {intc},
  lsv-status =    {apar},
  wwwpublic =     {public and ccsb},
}

@InProceedings{FSVY:Prolog:types=programs,
  author = 	 {Fr{\"u}hwirth, Thom and Shapiro, Ehud and Vardi, Moshe Y. and Yardeni, Eyal},
  title = 	 {Logic Programs as Types for Logic Programs},
  booktitle = 	 {Proc.\ 6th Symp Logic in Computer Science},
  SHORTbooktitle = 	 {LICS'91},
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages =	 {300--309},
  OPTpublisher = {},
  year =	 {1991},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTtype = 	 {},
  OPTchapter = 	 {},
  OPTaddress =	 {Amsterdam, NL},
  OPTedition = 	 {},
  OPTmonth =	 jul,
  OPTnote = 	 {},
  OPTannote = 	 {},
  abstract = "Type checking can be extremely useful to the program
  development process.  Of particular interest are descriptive type
  systems, which let the programmer write programs without having to
  define or mention types.  We consider here optimistic type systems
  for logic programs.  In such systems types are conservative
  approximations to the success set of the program predicates.  We
  propose the use of logic programs to describe types.  We argue that
  this approach unifies the denotational and operational approaches to
  descriptive type systems and is simpler and more natural than
  previous approaches.  We focus on the use of unary-predicate
  programs to describe types.  We identify a proper class of
  unary-predicate programs and show that it is expressive enough to
  express several notions of types.  We use an analogy with 2-way
  automata and a correspondence with alternating algorithms to obtain
  a complexity characterization of type inference and type checking.
  This characterization was facilitated by the use of logic programs
  to represent types."
}
