References

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