References

  1. J. Backes & C.E. Brown (2010): Analytic Tableaux for Higher-Order Logic with Choice. In: J. Giesl & R. Hähnle: Automated Reasoning, Lecture Notes in Computer Science 6173. Springer Berlin Heidelberg, pp. 76–90, doi:10.1007/978-3-642-14203-1_7.
  2. C. Barrett, C.L. Conway, M. Deters, L. Hadarean, D. Jovanovic, T. King, A. Reynolds & C. Tinelli (2011): CVC4. In: Ganesh Gopalakrishnan & Shaz Qadeer: Computer Aided Verification, LNCS 6806. Springer Berlin Heidelberg, pp. 171–177, doi:10.1007/978-3-642-22110-1_14.
  3. C. Benzmüller (2010): Verifying the Modal Logic Cube is an Easy Task (for Higher-Order Automated Reasoners). In: S. Siegler & N. Wasser: Verification, Induction, Termination Analysis - Festschrift for Christoph Walther on the Occasion of His 60th Birthday, LNCS 6463. Springer, pp. 117–128, doi:10.1007/978-3-642-17172-7_7. Available at http://christoph-benzmueller.de/papers/B12.pdf.
  4. C. Benzmüller (2013): Automating Quantified Conditional Logics in HOL. In: F. Rossi: 23rd International Joint Conference on Artificial Intelligence (IJCAI-13), Beijing, China, pp. 746–753. Available at http://ijcai.org/papers13/Papers/IJCAI13-117.pdf.
  5. C. Benzmüller & B. Woltzenlogel Paleo (2013): Gödel's God in Isabelle/HOL. Archive of Formal Proofs. http://afp.sf.net/entries/GoedelGod.shtml, Formal proof development.
  6. C. Benzmüller & B. Woltzenlogel Paleo (2014): Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers. In: T. Schaub, G. Friedrich & B. O'Sullivan: ECAI 2014, Frontiers in Artificial Intelligence and Applications 263. IOS Press, pp. 93 – 98, doi:10.3233/978-1-61499-419-0-93. Available at http://christoph-benzmueller.de/papers/C40.pdf.
  7. C. Benzmüller & L.C. Paulson (2013): Quantified Multimodal Logics in Simple Type Theory. Logica Universalis (Special Issue on Multimodal Logics) 7(1), pp. 7–20, doi:10.1007/s11787-012-0052-y. Available at http://christoph-benzmueller.de/papers/J23.pdf.
  8. C. Benzmüller, F. Rabe & G. Sutcliffe (2008): THF0 – The Core of the TPTP Language for Classical Higher-Order Logic. In: A. Armando, P. Baumgartner & G. Dowek: Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, LNCS 5195. Springer, pp. 491–506, doi:10.1007/978-3-540-71070-7_41. Available at http://christoph-benzmueller.de/papers/C25.pdf.
  9. C. Benzmüller, F. Theiss, L.C. Paulson & A. Fietzke (2008): LEO-II - A Cooperative Automatic Theorem Prover for Higher-Order Logic (System Description). In: A. Armando, P. Baumgartner & G. Dowek: Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, LNCS 5195. Springer, pp. 162–170, doi:10.1007/978-3-540-71070-7_14. Available at http://christoph-benzmueller.de/papers/C26.pdf.
  10. J.C. Blanchette & T. Nipkow (2010): Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: M. Kaufmann & L. Paulson: Interactive Theorem Proving (ITP 2010) 6172, pp. 131–146, doi:10.1007/978-3-642-14052-5_11.
  11. J. Hurd (2003): First-Order Proof Tactics in Higher-Order Logic Theorem Provers. In: M. Archer, B. Di Vito & C. Muñoz: Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), NASA Technical Reports, pp. 56–68. Available at http://www.gilith.com/research/papers.
  12. L. Kovács & A. Voronkov (2013): First-Order Theorem Proving and Vampire. In: N. Sharygina & H. Veith: Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, LNCS 8044. Springer, pp. 1–35, doi:10.1007/978-3-642-39799-8_1.
  13. L.M. de Moura & N. Bjørner (2008): Z3: An Efficient SMT Solver. In: C.R. Ramakrishnan & J. Rehof: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, LNCS 4963. Springer, pp. 337–340, doi:10.1007/978-3-540-78800-3_24.
  14. T. Nipkow, L.C. Paulson & M. Wenzel (2002): Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS 2283. Springer.
  15. L.C. Paulson & J.C. Blanchette (2012): Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. In: G. Sutcliffe, S. Schulz & E. Ternovska: IWIL 2010, EPiC Series 2. EasyChair, pp. 1–11.
  16. F. Rabe, P. Pudlak, G. Sutcliffe & W. Shen (2009): Solving the $ 100 modal logic challenge. Journal of Applied Logic 7, pp. 113–130, doi:10.1016/j.jal.2007.07.007.
  17. S. Schulz (2013): System Description: E 1.8. In: K.L. McMillan, A. Middeldorp & A. Voronkov: Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings, LNCS 8312. Springer, pp. 735–743, doi:10.1007/978-3-642-45221-5_49.
  18. N. Sultana (2015): Higher-order proof translation. Computer Laboratory, University of Cambridge. Available as Tech Report UCAM-CL-TR-867.
  19. C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. Suda & P. Wischnewski (2009): SPASS Version 3.5. In: R.A. Schmidt: Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings, LNCS 5663. Springer, pp. 140–145, doi:10.1007/978-3-642-02959-2_10.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org