Metis_

Metis is an automatic theorem prover for first order logic with equality Features of Metis: Coded in Standard ML (SML), with an emphasis on keeping the code as simple as possible. Compiled using MLton to give respectable performance on standard benchmarks. Reads in problems in the standard .tptp file format of the TPTP problem set. Outputs detailed proofs in TSTP format, where each refutation step is one of 6 simple rules. Outputs saturated clause sets when input problems are discovered to be unprovable.


References in zbMATH (referenced in 53 articles )

Showing results 1 to 20 of 53.
Sorted by year (citations)

1 2 3 next

  1. Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
  2. Bentkamp, Alexander; Blanchette, Jasmin Christian; Klakow, Dietrich: A formal proof of the expressiveness of deep learning (2019)
  3. Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
  4. Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
  5. Benzmüller, C.; Weber, Leon; Woltzenlogel Paleo, Bruno: Computer-assisted analysis of the Anderson-Hájek ontological controversy (2017)
  6. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  7. Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas: Encoding monomorphic and polymorphic types (2016)
  8. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  9. Berger, Ulrich; Lawrence, Andrew; Forsberg, Fredrik Nordvall; Seisenberger, Monika: Extracting verified decision procedures: DPLL and resolution (2015)
  10. Kaliszyk, Cezary; Urban, Josef: HOL(y)Hammer: online ATP service for HOL Light (2015)
  11. Sultana, Nik; Benzmüller, Christoph; Paulson, Lawrence C.: Proofs and reconstructions (2015)
  12. Wenzel, Makarius: Interactive theorem proving from the perspective of Isabelle/Isar (2015)
  13. Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef: Premise selection for mathematics by corpus analysis and kernel methods (2014)
  14. Gransden, Thomas; Walkinshaw, Neil; Raman, Rajeev: Mining state-based models from proof corpora (2014)
  15. Johansson, Moa; Rosén, Dan; Smallbone, Nicholas; Claessen, Koen: Hipster: integrating theory exploration in a proof assistant (2014)
  16. Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with (\mathsfFlyspeck) (2014)
  17. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
  18. Kaliszyk, Cezary; Urban, Josef: PRocH: proof reconstruction for HOL Light (2013)
  19. Kaliszyk, Cezary; Urban, Josef: Automated reasoning service for HOL Light (2013)
  20. Sultana, Nik; Blanchette, Jasmin Christian; Paulson, Lawrence C.: LEO-II and Satallax on the Sledgehammer test bench (2013)

1 2 3 next