References

  1. Andreas Abel, Thierry Coquand & Ulf Norell (2005): Connecting a Logical Framework to a First-Order Logic Prover. In: Bernhard Gramlich: Frontiers of Combining Systems (FroCoS 2005), LNCS 3717. Springer, pp. 285–301, doi:10.1007/11559306_17.
  2. Alejandro Aguirre, Cătălin Hri\begingroupłet [Please insert \PrerenderUnicode\unichar539 into preamble]cu, Chantal Keller & Nikhil Swamy (2016): From F^* to SMT (Extended Abstract). In: Hammers for Type Theories, HaTT 2016. To appear.
  3. Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry & Benjamin Werner (2011): A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. In: Jean-Pierre Jouannaud & Zhong Shao: Certified Programs and Proofs (CPP 2011), LNCS 7086. Springer, pp. 135–150, doi:10.1007/978-3-642-25379-9_12.
  4. Andrea Asperti, Wilmer Ricciotti & Claudio Sacerdoti Coen (2014): Matita Tutorial. J. Formalized Reasoning 7(2), pp. 91–199, doi:10.6092/issn.1972-5787/4651.
  5. Andrea Asperti & Enrico Tassi (2007): Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case. In: Manuel Kauers, Manfred Kerber, Robert Miner & Wolfgang Windsteiger: Mathematical Knowledge Management (MKM 2007), LNCS 4573. Springer, pp. 146–160, doi:10.1007/978-3-540-73086-6_14.
  6. Grzegorz Bancerek (2003): On the structure of Mizar types. Electr. Notes Theor. Comput. Sci. 85(7), pp. 69–85, doi:10.1016/S1571-0661(04)80758-8.
  7. Grzegorz Bancerek, Czeslaw Bylinski, Adam Grabowski, Artur Kornilowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak & Josef Urban (2015): Mizar: State-of-the-art and Beyond. In: Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings, pp. 261–279, doi:10.1007/978-3-319-20615-8_17.
  8. Yves Bertot (2008): A Short Presentation of Coq. In: Otmane Aït Mohamed, César A. Muñoz & Sofiène Tahar: Theorem Proving in Higher Order Logics (TPHOLs 2008), LNCS 5170. Springer, pp. 12–16, doi:10.1007/978-3-540-71067-7_3.
  9. 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.1023/A:1021939521172.
  10. Jasmin C. Blanchette, Cezary Kaliszyk, Lawrence C. Paulson & Josef Urban (2016): Hammering towards QED. J. Formalized Reasoning 9(1), pp. 101–148, doi:10.6092/issn.1972-5787/4593. Available at http://jfr.unibo.it/article/view/4593.
  11. Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel K\begingroupłet [Pleaseinsert\PrerenderUnicodeüintopreamble]hlwein & Josef Urban (2016): A Learning-Based Relevance Filter for Isabelle/HOL. J. Autom. Reasoning, to appear. http://cl-informatik.uibk.ac.at/cek/mash2.pdf.
  12. Ana Bove, Peter Dybjer & Ulf Norell (2009): A Brief Overview of Agda - A Functional Language with Dependent Types. In: Stefan Berghofer, Tobias Nipkow, Christian Urban & Makarius Wenzel: Theorem Proving in Higher Order Logics (TPHOLs 2009), LNCS 5674. Springer, pp. 73–78, doi:10.1007/978-3-642-03359-9_6.
  13. Pierre Corbineau (2003): First-Order Reasoning in the Calculus of Inductive Constructions. In: Stefano Berardi, Mario Coppo & Ferruccio Damiani: Types for Proofs and Programs (TYPES 2003), LNCS 3085. Springer, pp. 162–177, doi:10.1007/978-3-540-24849-1_11.
  14. Roy Dyckhoff (1992): Contraction-Free Sequent Calculi for Intuitionistic Logic. J. Symb. Log. 57(3), pp. 795–807, doi:10.2307/2275431.
  15. Jean-Christophe Filliâtre (2013): One Logic to Use Them All. In: Maria Paola Bonacina: International Conference on Automated Deduction (CADE 2013), LNCS 7898. Springer, pp. 1–20, doi:10.1007/978-3-642-38574-2_1.
  16. Jean-Christophe Filliâtre & Andrei Paskevich (2013): Why3 - Where Programs Meet Provers. In: European Symposium on Programming (ESOP 2013), pp. 125–128, doi:10.1007/978-3-642-37036-6_8.
  17. Thomas Hales (2013–2014): Developments in Formal Proofs. S\begingroupłet [Pleaseinsert\PrerenderUnicodeéintopreamble]minaire Bourbaki 1086. abs/1408.6474.
  18. John Harrison (2009): HOL Light: An Overview. In: Stefan Berghofer, Tobias Nipkow, Christian Urban & Makarius Wenzel: Theorem Proving in Higher Order Logics (TPHOLs 2009), LNCS 5674. Springer, pp. 60–66, doi:10.1007/978-3-642-03359-9_4.
  19. Joe Hurd (2003): First-Order Proof Tactics in Higher-Order Logic Theorem Provers. In: Myla Archer, Ben Di Vito & César Muñoz: Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), NASA Technical Reports NASA/CP-2003-212448, pp. 56–68. Available at http://techreports.larc.nasa.gov/ltrs/PDF/2003/cp/NASA-2003-cp212448.pdf.
  20. Cezary Kaliszyk & Josef Urban (2014): Learning-Assisted Automated Reasoning with Flyspeck. J. Autom. Reasoning 53(2), pp. 173–213, doi:10.1007/s10817-014-9303-3.
  21. Cezary Kaliszyk & Josef Urban (2015): MizAR 40 for Mizar 40. J. Autom. Reasoning 55(3), pp. 245–256, doi:10.1007/s10817-015-9330-8.
  22. Laura Kovács & Andrei Voronkov (2013): First-Order Theorem Proving and Vampire. In: Computer-Aided Verification (CAV 2013), pp. 1–35, doi:10.1007/978-3-642-39799-8_1.
  23. Jia Meng & Lawrence C. Paulson (2008): Translating Higher-Order Clauses to First-Order Clauses. Journal of Automated Reasoning 40(1), pp. 35–60, doi:10.1007/s10817-007-9085-y.
  24. Leonardo de Moura & Daniel Selsam (2016): Congruence Closure in Intensional Type Theory. In: International Joint Conference on Automated Reasoning, IJCAR 2016. To appear.
  25. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn & Jakob von Raumer (2005): The Lean Theorem Prover. In: Amy P. Felty & Aart Middeldorp: International Conference on Automated Deduction (CADE 2005), LNCS 9195. Springer, pp. 378–388, doi:10.1007/978-3-319-21401-6_26.
  26. Leonardo Mendonça de Moura & Nikolaj Bjørner (2008): Z3: An Efficient SMT Solver. In: C. R. Ramakrishnan & Jakob Rehof: TACAS 2008, LNCS 4963. Springer, pp. 337–340, doi:10.1007/978-3-540-78800-3_24.
  27. Lawrence C. Paulson & Jasmin Blanchette (2010): Three Years of Experience with Sledgehammer, a Practical Link between Automated and Interactive Theorem Provers. In: 8th IWIL. Available at http://www4.in.tum.de/~schulz/PAPERS/STS-IWIL-2010.pdf.
  28. Stephan Schmitt, Lori Lorigo, Christoph Kreitz & Aleksey Nogin (2001): JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants. In: Rajeev Goré, Alexander Leitsch & Tobias Nipkow: Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, Lecture Notes in Computer Science 2083. Springer, pp. 421–426, doi:10.1007/3-540-45744-5_34.
  29. Aleksy Schubert, PawełUrzyczyn & Konrad Zdanowski (2015): On the Mints Hierarchy in First-Order Intuitionistic Logic. In: Andrew M. Pitts: Foundations of Software Science and Computation Structures (FoSSaCS 2015), Lecture Notes in Computer Science 9034. Springer, pp. 451–465, doi:10.1007/978-3-662-46678-0_29.
  30. Stephan Schulz (2013): System Description: E 1.8. In: Logic for Programming, Artificial Intelligence (LPAR 2013), pp. 735–743, doi:10.1007/978-3-642-45221-5_49.
  31. Konrad Slind & Michael Norrish (2008): A Brief Overview of HOL4. In: Otmane Ait Mohamed, César Muñoz & Sofiène Tahar: TPHOLs 2008, LNCS 5170. Springer, pp. 28–32, doi:10.1007/978-3-540-71067-7_6.
  32. Tanel Tammet & Jan M. Smith (1998): Optimized Encodings of Fragments of Type Theory in First-Order Logic. J. Log. Comput. 8(6), pp. 713–744, doi:10.1093/logcom/8.6.713.
  33. Makarius Wenzel, Lawrence C. Paulson & Tobias Nipkow (2008): The Isabelle Framework. In: Otmane Aït Mohamed, César A. Muñoz & Sofiène Tahar: Theorem Proving in Higher Order Logics (TPHOLs 2008), LNCS 5170. Springer, pp. 33–38, doi:10.1007/978-3-540-71067-7_7.
  34. Freek Wiedijk (2007): Mizar's Soft Type System. In: Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, pp. 383–399, doi:10.1007/978-3-540-74591-4_28.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org