References

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