@inproceedings(briandais_trie,
 author       = {Ren\'{e} de la Briandais},
 year         = {1959},
 title        = {File searching using variable length keys},
 booktitle    = {Proceedings of the Western Joint Computer Conference},
 pages        = {295--298},
 doi          = {10.1145/1457838.1457895},
)
@article(bry_meta,
 author       = {Fran\c cois Bry},
 year         = {2020},
 title        = {In Praise of Impredicativity: A Contribution to the Formalization of Meta-Programming},
 journal      = {Theory and Practice of Logic Programming},
 volume       = {20},
 number       = {1},
 pages        = {99--146},
 doi          = {10.1017/S1471068419000024},
 url          = {https://pms.ifi.lmu.de/publications/PMS-FB/PMS-FB-2018-2/PMS-FB-2018-2-paper-second-revision.pdf},
)
@article(champeaux_pwunif,
 author       = {Dennis de Champeaux},
 year         = {1986},
 title        = {About the Paterson-Wegman Linear Unification Algorithm},
 journal      = {Journal of Computer and System Sciences},
 volume       = {32},
 number       = {1},
 pages        = {79--90},
 doi          = {10.1016/0022-0000(86)90003-6},
)
@article(chen_hilog,
 author       = {Weidong Chen and Michael Kifer and David Scott Warren},
 year         = {1993},
 title        = {{HILOG:} {A} Foundation for Higher-Order Logic Programming},
 journal      = {Journal of Logic Programming},
 volume       = {15},
 number       = {3},
 pages        = {187--230},
 doi          = {10.1016/0743-1066(93)90039-J},
)
@inproceedings(christian_kbc,
 author       = {Jim Christian},
 year         = {1989},
 title        = {Fast Knuth-Bendix Completion: Summary},
 editor       = {Nachum Dershowitz},
 booktitle    = {Rewriting Techniques and Applications, 3rd International Conference (RTA'89)},
 series       = {LNCS},
 volume       = {355},
 publisher    = {Springer},
 pages        = {551--555},
 doi          = {10.1007/3-540-51081-8\_136},
)
@article(christian_flat,
 author       = {Jim Christian},
 year         = {1993},
 title        = {Flatterms, Discrimination Nets, and Fast Term Rewriting},
 journal      = {Journal of Automated Reasoning},
 volume       = {10},
 number       = {1},
 pages        = {95--113},
 doi          = {10.1007/BF00881866},
)
@article(emden_immconseq,
 author       = {Maarten H. van Emden and Robert A. Kowalski},
 year         = {1976},
 title        = {The Semantics of Predicate Logic as a Programming Language},
 journal      = {Journal of the {ACM}},
 volume       = {23},
 number       = {4},
 pages        = {733--742},
 doi          = {10.1145/321978.321991},
)
@article(escalada_linunif,
 author       = {Escalada-Imaz, Gonzalo and Malik Ghallab},
 year         = {1988},
 title        = {A Practically Efficient and Almost Linear Unification Algorithm},
 journal      = {Artificial Intelligence},
 volume       = {36},
 number       = {2},
 pages        = {249--263},
 doi          = {10.1016/0004-3702(88)90005-7},
)
@article(fredkin_trie,
 author       = {Edward Fredkin},
 year         = {1960},
 title        = {Trie Memory},
 journal      = {Communications of the ACM},
 volume       = {3},
 number       = {9},
 pages        = {490--499},
 doi          = {10.1145/367390.367400},
)
@article(ganzinger_ctxtr,
 author       = {Harald Ganzinger and Robert Nieuwenhuis and Pilar Nivela},
 year         = {2004},
 title        = {Fast Term Indexing with Coded Context Trees},
 journal      = {Journal of Automated Reasoning},
 volume       = {32},
 number       = {2},
 pages        = {103--120},
 doi          = {10.1023/B:JARS.0000029963.64213.ac},
)
@inproceedings(graef_ltrtrpat,
 author       = {Albert Gr{\"{a}}f},
 year         = {1991},
 title        = {Left-to-Right Tree Pattern Matching},
 editor       = {Ronald V. Book},
 booktitle    = {Rewriting Techniques and Applications, 4th International Conference (RTA'91)},
 series       = {LNCS},
 volume       = {488},
 publisher    = {Springer},
 pages        = {323--334},
 doi          = {10.1007/3-540-53904-2\_107},
)
@inproceedings(graf_extpathidx,
 author       = {Peter Graf},
 year         = {1994},
 title        = {Extended Path-Indexing},
 editor       = {Alan Bundy},
 booktitle    = {2nd Conference on Automated Deduction (CADE)},
 series       = {LNCS},
 volume       = {814},
 publisher    = {Springer},
 pages        = {514--528},
 doi          = {10.1007/3-540-58156-1\_37},
)
@inproceedings(graf_substreeidx,
 author       = {Peter Graf},
 year         = {1995},
 title        = {Substitution Tree Indexing},
 editor       = {Jieh Hsiang},
 booktitle    = {6th International Conference on Rewriting Techniques and Applications (RTA'95)},
 series       = {LNCS},
 volume       = {914},
 publisher    = {Springer},
 pages        = {117--131},
 doi          = {10.1007/3-540-59200-8\_52},
)
@book(graf_termidx,
 author       = {Peter Graf},
 year         = {1995},
 title        = {Term Indexing},
 series       = {LNCS},
 volume       = {1053},
 publisher    = {Springer},
 doi          = {10.1007/3-540-61040-5},
)
@inproceedings(green_logprog,
 author       = {C. Cordell Green},
 year         = {1969},
 title        = {Application of Theorem Proving to Problem Solving},
 editor       = {Donald E. Walker and Lewis M. Norton},
 booktitle    = {Proceedings of the 1st International Joint Conference on Artificial Intelligence},
 publisher    = {William Kaufmann},
 pages        = {219--240},
 url          = {http://ijcai.org/Proceedings/69/Papers/023.pdf},
)
@phdthesis(hewitt_planner,
 author       = {Carl Hewitt},
 year         = {1972},
 title        = {Description and Theoretical Analysis (Using Schemata) of Planner},
 school       = {Artificial Intelligence Laboratory, Massachusetts Institute of Technology},
 url          = {http://hdl.handle.net/1721.1/6916},
)
@inproceedings(hoder_unifcmp,
 author       = {Kry\v{s}tof Hoder and Andrei Voronkov},
 year         = {2009},
 title        = {Comparing Unification Algorithms in First-Order Theorem Proving},
 editor       = {B{\"a}rbel Mertsching and Marcus Hund and Muhammad Zaheer Aziz},
 booktitle    = {KI 2009: Advances in Artificial Intelligence (KI'09)},
 series       = {LNCS},
 volume       = {5803},
 address      = {Paderborn, Germany},
 pages        = {435--443},
 doi          = {10.1007/978-3-642-04617-9\_55},
)
@inproceedings(jiang_amblog,
 author       = {Yuejun Jiang},
 year         = {1994},
 title        = {Ambivalent Logic as the Semantic Basis of Metalogic Programming},
 editor       = {Pascal Van Hentenryck},
 booktitle    = {Logic Programming, Proceedings of the Eleventh International Conference},
 publisher    = {MIT Press},
 address      = {Santa Marherita Ligure, Italy},
 pages        = {387--401},
)
@inproceedings(johnson_tst,
 author       = {Ernie Johnson and C. R. Ramakrishnan and I. V. Ramakrishnan and Prasad Rao},
 year         = {1999},
 title        = {A Space Efficient Engine for Subsumption-Based Tabled Evaluation of Logic Programs},
 editor       = {Aart Middeldorp and Taisuke Sato},
 booktitle    = {Functional and Logic Programming, 4th Fuji International Symposium (FLOPS'99)},
 series       = {LNCS},
 volume       = {1722},
 publisher    = {Springer},
 address      = {Tsukuba, Japan},
 pages        = {284--300},
 doi          = {10.1007/10705424\_19},
)
@inbook(kalsbeek_vademecum,
 author       = {Marianne B. Kalsbeek and Yuejun Jiang},
 year         = {1995},
 title        = {Meta-Logics and Logic Programming},
 chapter      = {A Vademecum of Ambivalent Logic},
 pages        = {27--56},
 series       = {Computation and Complexity Theory},
 publisher    = {MIT Press},
 url          = {https://www.illc.uva.nl/Research/Publications/Reports/CT-1995-01.text.pdf},
)
@inproceedings(kowalski_logprog,
 author       = {Robert A. Kowalski},
 year         = {1974},
 title        = {Predicate Logic as Programming Language},
 editor       = {Jack L. Rosenfeld},
 booktitle    = {Information Processing, Proceedings of the 6th {IFIP} Congress},
 publisher    = {North-Holland},
 pages        = {569--574},
 url          = {http://www.doc.ic.ac.uk/~rak/papers/IFIP\%2074.pdf},
)
@article(kowalski_alc,
 author       = {Robert A. Kowalski},
 year         = {1979},
 title        = {Algorithm = Logic + Control},
 journal      = {Communication of the {ACM}},
 volume       = {22},
 number       = {7},
 pages        = {424--436},
 doi          = {10.1145/359131.359136},
)
@article(letz_setheo,
 author       = {Reinhold Letz and Johann Schumann and Stefan Bayerl and Wolfgang Bibel},
 year         = {1992},
 title        = {{SETHEO}: A high-performance theorem prover},
 journal      = {Journal of Automated Reasoning},
 volume       = {8},
 number       = {2},
 pages        = {183--212},
 doi          = {10.1007/BF00244282},
)
@article(martelli_effunif,
 author       = {Alberto Martelli and Ugo Montanari},
 year         = {1982},
 title        = {An Efficient Unification Algorithm},
 journal      = {ACM Transaction on Programming Language Systems (TOPLAS'82)},
 volume       = {4},
 number       = {2},
 pages        = {258--282},
 doi          = {10.1145/357162.357169},
)
@article(mccune_discrimtrees,
 author       = {William McCune},
 year         = {1988},
 title        = {An indexing mechanism for finding more general formulas},
 journal      = {Association for Automated Reasoning Newsletter},
 volume       = {9},
)
@article(mccune_exptermidx,
 author       = {William McCune},
 year         = {1992},
 title        = {Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval},
 journal      = {Journal of Automated Reasoning},
 volume       = {9},
 pages        = {147--167},
 doi          = {10.1007/BF00245458},
)
@inproceedings(ohlbach_abstree,
 author       = {Hans J\"urgen Ohlbach},
 year         = {1990},
 title        = {Abstraction Tree Indexing for Terms},
 booktitle    = {9th European Conference on Artificial Intelligence (ECAI'90)},
 pages        = {479--484},
)
@article(paterson_linunif,
 author       = {Michael Stewart Paterson and M.N. Wegman},
 year         = {1978},
 title        = {Linear Unification},
 journal      = {Journal of Computer and System Sciences},
 volume       = {16},
 number       = {2},
 pages        = {158--167},
 doi          = {10.1016/0022-0000(78)90043-0},
)
@article(pientka_hoti,
 author       = {Brigitte Pientka},
 year         = {2009},
 title        = {Higher-Order Term Indexing Using Substitution Trees},
 journal      = {ACM Transactions on Computational Logic (TOCL)},
 volume       = {11},
 number       = {1},
 pages        = {6:1--6:40},
 doi          = {10.1145/1614431.1614437},
)
@inproceedings(prokosch_reasoningtrie,
 author       = {Thomas Prokosch and Fran\c cois Bry},
 year         = {2020},
 title        = {Give Reasoning a Trie},
 booktitle    = {7th Workshop on Practical Aspects of Automated Reasoning (PAAR'20)},
 series       = {CEUR Workshop Proceedings},
 address      = {Aachen},
 note         = {To appear},
)
@inproceedings(prokosch_unifrun,
 author       = {Thomas Prokosch and Fran\c cois Bry},
 year         = {2020},
 title        = {Unification on the Run},
 editor       = {Temur Kutsia and Andrew M. Marshall},
 booktitle    = {The 34th International Workshop on Unification (UNIF'20)},
 series       = {RISC Report Series},
 volume       = {20-10},
 publisher    = {Research Institute for Symbolic Computation, Johannes Kepler University},
 address      = {Linz, Austria},
 pages        = {13:1--13:5},
 url          = {https://www.risc.jku.at/publications/download/risc_6129/proceedings-UNIF2020.pdf},
)
@article(ramakrishnan_bktrk,
 author       = {I. V. Ramakrishnan and Prasad Rao and Konstantinos Sagonas and Terrance Swift and David Scott Warren},
 year         = {1999},
 title        = {Efficient Access Mechanisms for Tabled Logic Programs},
 journal      = {Journal of Logic Programming},
 volume       = {38},
 number       = {1},
 pages        = {31--54},
 doi          = {10.1016/S0743-1066(98)10013-4},
)
@article(robinson_resolution,
 author       = {John Alan Robinson},
 year         = {1965},
 title        = {A Machine-Oriented Logic Based on the Resolution Principle},
 journal      = {Journal of the ACM},
 volume       = {12},
 number       = {1},
 pages        = {23--41},
 doi          = {10.1145/321250.321253},
)
@book(robinson_har,
 editor       = {John Alan Robinson and Andrei Voronkov},
 year         = {2001},
 title        = {Handbook of Automated Reasoning},
 publisher    = {Elsevier Science Publishers},
)
@inproceedings(schulz_pyres,
 author       = {Stephan Schulz and Adam Pease},
 year         = {2020},
 title        = {Teaching Automated Theorem Proving by Example: PyRes 1.2},
 editor       = {Nicolas Peltier and Sofronie{-}Stokkermans, Viorica},
 booktitle    = {Automated Reasoning - 10th International Joint Conference (IJCAR'20), Proceedings, Part {II}},
 series       = {LNCS},
 volume       = {12167},
 publisher    = {Springer},
 pages        = {158--166},
 doi          = {10.1007/978-3-030-51054-1\_9},
)
@inbook(sekar_termidx,
 author       = {R. Sekar and I. V. Ramakrishnan and Andrei Voronkov},
 year         = {2001},
 title        = {Handbook of Automated Reasoning},
 chapter      = {Term Indexing},
 pages        = {1853--1964},
 volume       = {2},
 publisher    = {Elsevier Science Publishers},
 doi          = {10.1016/B978-044450813-3/50028-X},
 url          = {http://www.cs.man.ac.uk/~voronkov/papers/handbookar_termindexing.ps},
)
@inproceedings(sekar_apm,
 author       = {R. C. Sekar and R. Ramesh and I. V. Ramakrishnan},
 year         = {1992},
 title        = {Adaptive Pattern Matching},
 editor       = {Werner Kuich},
 booktitle    = {Automata, Languages and Programming, 19th International Colloquium (ICALP'92)},
 series       = {LNCS},
 volume       = {623},
 publisher    = {Springer},
 pages        = {247--260},
 doi          = {10.1007/3-540-55719-9\_78},
)
@techreport(stickel_pathidx,
 author       = {Mark E. Stickel},
 year         = {1989},
 title        = {The Path-Indexing Method For Indexing Terms},
 type         = {Technical Note},
 number       = {473},
 institution  = {SRI International},
 address      = {Menlo Park, California, USA},
 url          = {https://www.sri.com/wp-content/uploads/pdf/498.pdf},
)
@inproceedings(tamaki_oldt,
 author       = {Hisao Tamaki and Taisuke Sato},
 year         = {1986},
 title        = {{OLD} Resolution with Tabulation},
 editor       = {Ehud Shapiro},
 booktitle    = {Third International Conference on Logic Programming (LP'86)},
 series       = {LNCS},
 volume       = {225},
 publisher    = {Springer},
 address      = {Imperial College of Science and Technology, London, UK},
 pages        = {84--98},
 doi          = {10.1007/3-540-16492-8\_66},
)
@article(voronkov_avampire,
 author       = {Andrei Voronkov},
 year         = {1995},
 title        = {The Anatomy of Vampire},
 journal      = {Journal of Automated Reasoning},
 volume       = {15},
 number       = {2},
 pages        = {237--265},
 doi          = {10.1007/BF00881918},
)