References

  1. Ali Assaf, Guillaume Burel, Raphaël Cauderlier, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant & Ronan Saillard: Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory. Available at http://www.lsv.fr/~dowek/Publi/expressing.pdf.
  2. Richard Bonichon, David Delahaye & Damien Doligez (2007): Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs. In: Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings, pp. 151–165, doi:10.1007/978-3-540-75560-9_13.
  3. Guillaume Bury, Simon Cruanes & David Delahaye (2018): SMT Solving Modulo Tableau and Rewriting Theories. Available at https://hal.archives-ouvertes.fr/hal-02083232.
  4. Simon Cruanes (2015): Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond. Theses. École polytechnique. Available at https://hal.archives-ouvertes.fr/tel-01223502.
  5. David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand & Olivier Hermant (2013): Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo. In: Ken McMillan, Aart Middeldorp & Andrei Voronkov: Logic for Programming, Artificial Intelligence, and Reasoning. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 274–290, doi:10.1007/978-3-642-45221-5_20.
  6. Gilles Dowek & Benjamin Werner: A constructive proof of Skolem theorem for constructive logic. Available at http://www.lsv.fr/~dowek/Publi/skolem.pdf.
  7. Stephan Schulz (2013): System Description: E 1.8. In: Ken McMillan, Aart Middeldorp & Andrei Voronkov: Proc. of the 19th LPAR, Stellenbosch, LNCS 8312. Springer, doi:10.1007/978-3-642-45221-5_49.
  8. G. Sutcliffe (2017): The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning 59(4), pp. 483–502, doi:10.1007/s10817-017-9407-7.
  9. Geoff Sutcliffe (2018): The 9th IJCAR Automated Theorem Proving System Competition - CASC-J9. AI Commun. 31(6), pp. 495–507, doi:10.3233/AIC-180773.
  10. François Thiré (2018): Sharing a Library between Proof Assistants: Reaching out to the HOL Family. In: Frédéric Blanqui & Giselle Reis: Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2018, Oxford, UK, 7th July 2018., EPTCS 274, pp. 57–71, doi:10.4204/EPTCS.274.5.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org