@incollection(AB98,
 author       = "Wolfgang Ahrendt and Bernhard Beckert and Reiner H\"ahnle and Wolfram Menzel and Wolfgang Reif and Gerhard Schellhorn and Peter H. Schmitt",
 year         = "1998",
 title        = "Integrating Automated and Interactive Theorem Proving",
 editor       = "Wolfgang Bibel and Peter H. Schmitt",
 booktitle    = "Automated Deduction --- A Basis for Applications",
 series       = "Applied Logic Series, No. 9",
 volume       = "{II}: Systems and Implementation Techniques",
 publisher    = "Kluwer, Dordrecht",
 pages        = "97--116",
)
@inproceedings(hints,
 author       = "Andrea Asperti and Wilmer Ricciotti and Claudio Sacerdoti Coen and Enrico Tassi",
 year         = "2009",
 title        = "Hints in Unification",
 editor       = "Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel",
 booktitle    = "TPHOLs",
 series       = "Lecture Notes in Computer Science",
 volume       = "5674",
 publisher    = "Springer",
 pages        = "84--98",
 doi          = "10.1007/978-3-642-03359-9\_8",
)
@inproceedings(auto-driver,
 author       = "Andrea Asperti and Enrico Tassi",
 year         = "2009",
 title        = "An interactive driver for goal directed proof strategies",
 booktitle    = "Proc. of User Interfaces for Theorem Provers 2008. Montreal, CA, August 2008",
 series       = "ENTCS",
 volume       = "226",
 pages        = "89--105",
 doi          = "10.1016/j.entcs.2008.12.099",
)
@article(BG94,
 author       = "Leo Bachmair and Harald Ganzinger",
 year         = "1994",
 title        = "Rewrite-Based Equational Theorem Proving with Selection and Simplification",
 journal      = "J. Log. Comput.",
 volume       = "4",
 number       = "3",
 pages        = "217--247",
 doi          = "10.1093/logcom/4.3.217",
)
@inproceedings(omega,
 author       = "Christoph Benzm{\"u}ller and Armin Fiedler and Andreas Meier and Martin Pollet and J{\"o}rg H. Siekmann",
 year         = "2006",
 title        = "Omega",
 booktitle    = "The Seventeen Provers of the World",
 series       = "Lecture Notes in Computer Science",
 volume       = "3600",
 publisher    = "Springer",
 pages        = "127--141",
 doi          = "10.1007/11542384\_17",
)
@article(BHN02,
 author       = "Marc Bezem and Dimitri Hendriks and Hans de Nivelle",
 year         = "2002",
 title        = "Automated Proof Construction in Type Theory Using Resolution",
 journal      = "J. Autom. Reasoning",
 volume       = "29",
 number       = "3-4",
 pages        = "253--275",
 doi          = "10.1007/1072195i\_10",
)
@incollection(equality-handbook,
 author       = "Anatoli Degtyarev and Andrei Voronkov",
 year         = "2001",
 title        = "Equality Reasoning in Sequent-Based Calculi",
 editor       = "John Alan Robinson and Andrei Voronkov",
 booktitle    = "Handbook of Automated Reasoning",
 publisher    = "Elsevier and MIT Press",
 pages        = "611--706",
 doi          = "10.1016/B978-044450813-3/50012-6",
)
@article(Dershowitz82,
 author       = "Nachum Dershowitz",
 year         = "1982",
 title        = "Orderings for Term-Rewriting Systems",
 journal      = "Theor. Comput. Sci.",
 volume       = "17",
 pages        = "279--301",
 doi          = "10.1016/0304-3975(82)90026-3",
)
@inproceedings(assoccommut,
 author       = "Nachum Dershowitz and Jieh Hsiang and N. Alan Josephson and David A. Plaisted",
 year         = "1983",
 title        = "Associative-Commutative Rewriting",
 booktitle    = "IJCAI",
 pages        = "940--944",
)
@article(modulo,
 author       = "Gilles Dowek and Th{\'e}r{\`e}se Hardin and Claude Kirchner",
 year         = "2003",
 title        = "Theorem Proving Modulo",
 journal      = "J. Autom. Reasoning",
 volume       = "31",
 number       = "1",
 pages        = "33--72",
 doi          = "10.1007/3-540-46508-1\_1",
)
@article(codedcontexttrees,
 author       = "Harald Ganzinger and Robert Nieuwenhuis and Pilar Nivela",
 year         = "2004",
 title        = "Fast Term Indexing with Coded Context Trees",
 journal      = "J. Autom. Reasoning",
 volume       = "32",
 number       = "2",
 pages        = "103--120",
 doi          = "10.1023/B:JARS.0000029963.64213.ac",
)
@inproceedings(Graf95,
 author       = "Peter Graf",
 year         = "1995",
 title        = "Substitution Tree Indexing",
 editor       = "Jieh Hsiang",
 booktitle    = "Rewriting Techniques and Applications, 6th International Conference, RTA-95, Kaiserslautern, Germany, April 5-7, 1995, Proceedings",
 series       = "Lecture Notes in Computer Science",
 volume       = "914",
 publisher    = "Springer",
 pages        = "117--131",
)
@book(harrison-book,
 author       = "John Harrison",
 year         = "2009",
 title        = "Handbook of Practical Logic and Automated Reasoning",
 publisher    = "Cambridge University Press",
)
@inproceedings(Hurd99,
 author       = "Joe Hurd",
 year         = "1999",
 title        = "Integrating Gandalf and HOL",
 editor       = "Yves Bertot and Gilles Dowek and Andr{\'e} Hirschowitz and C. Paulin and Laurent Th{\'e}ry",
 booktitle    = "TPHOLs",
 series       = "Lecture Notes in Computer Science",
 volume       = "1690",
 publisher    = "Springer",
 pages        = "311--322",
 doi          = "10.1007/3-540-48256-3\_21",
 url          = "http://link.springer.de/link/service/series/0558/bibs/1690/16900311.htm",
)
@techreport(metis,
 author       = "Joe Hurd",
 year         = "2003",
 title        = "First-Order Proof Tactics in Higher-Order Logic Theorem Provers",
 type         = "Technical Report",
 number       = "NASA/CP-2003-212448",
 institution  = "Nasa technical reports",
)
@article(Knuth-Bendix,
 author       = "Donald Knuth and P. Bendix",
 year         = "1970",
 title        = "Simple word problems in universal algebras",
 journal      = "Computational problems in Abstract Algebra (J. Leech ed.)",
 pages        = "263--297",
)
@article(McCune,
 author       = "W. McCune",
 year         = "1992",
 title        = "Experiments with discrimination tree indexing and path indexing for term retrieval",
 journal      = "Journal of Automated Reasoning",
 volume       = "9(2)",
 pages        = "147--167",
 doi          = "10.1007/BF00245458",
)
@article(MP08,
 author       = "Jia Meng and Lawrence C. Paulson",
 year         = "2008",
 title        = "Translating Higher-Order Clauses to First-Order Clauses",
 journal      = "J. Autom. Reasoning",
 volume       = "40",
 number       = "1",
 pages        = "35--60",
 doi          = "10.1007/s10817-007-9085-y",
)
@article(MQP06,
 author       = "Jia Meng and Claire Quigley and Lawrence C. Paulson",
 year         = "2006",
 title        = "Automation for interactive proof: First prototype",
 journal      = "Inf. Comput.",
 volume       = "204",
 number       = "10",
 pages        = "1575--1596",
 doi          = "10.1016/j.ic.2005.05.010",
)
@incollection(paramodulation,
 author       = "Robert Nieuwenhuis and Alberto Rubio",
 year         = "2001",
 title        = "Paramodulation-based thorem proving",
 editor       = "John Alan Robinson and Andrei Voronkov",
 booktitle    = "Handbook of Automated Reasoning",
 publisher    = "Elsevier and MIT Press",
 pages        = "471--443",
 doi          = "10.1016/B978-044450813-3/50009-6",
 note         = "ISBN-0-262-18223-8",
)
@article(blast,
 author       = "Lawrence C. Paulson",
 year         = "1999",
 title        = "A Generic Tableau Prover and its Integration with Isabelle",
 journal      = "J. UCS",
 volume       = "5",
 number       = "3",
 pages        = "73--87",
)
@article(vampire_annals,
 author       = "Alexandre Riazanov and Andrei Voronkov",
 year         = "2002",
 title        = "The Design and Implementation of Vampire",
 journal      = "AI Communications",
 volume       = "15(2-3)",
 pages        = "91--110",
)
@article(LRS,
 author       = "Alexandre Riazanov and Andrei Voronkov",
 year         = "2003",
 title        = "Limited resource strategy in resolution theorem proving",
 journal      = "J. Symb. Comput.",
 volume       = "36",
 number       = "1-2",
 pages        = "101--115",
 doi          = "10.1016/S0747-7171(03)00040-3",
)
@article(setoidrewriting,
 author       = "Matthieu Sozeau",
 year         = "2009",
 title        = "A New Look at Generalized Rewriting in Type Theory",
 journal      = "Journal of Formalized Reasoning",
 volume       = "2",
 number       = "1",
 pages        = "41--62",
)
@article(Sutcliffe09,
 author       = "Geoff Sutcliffe",
 year         = "2009",
 title        = "The 4th IJCAR Automated Theorem Proving System Competition - CASC-J4",
 journal      = "AI Commun.",
 volume       = "22",
 number       = "1",
 pages        = "59--72",
)
@article(demodulation,
 author       = "Larry Wos and George A. Robinson and Daniel F. Carson and Leon Shalla",
 year         = "1967",
 title        = "The Concept of Demodulation in Theorem Proving",
 journal      = "J. ACM",
 volume       = "14",
 number       = "4",
 pages        = "698--709",
 doi          = "10.1145/321420.321429",
)