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 37 articles )

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

1 2 next

  1. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  2. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  3. Berger, Ulrich; Lawrence, Andrew; Forsberg, Fredrik Nordvall; Seisenberger, Monika: Extracting verified decision procedures: DPLL and resolution (2015)
  4. Kaliszyk, Cezary; Urban, Josef: HOL(y)Hammer: online ATP service for HOL Light (2015)
  5. Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef: Premise selection for mathematics by corpus analysis and kernel methods (2014)
  6. Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with $\mathsfFlyspeck$ (2014)
  7. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
  8. Kaliszyk, Cezary; Urban, Josef: Proch: proof reconstruction for HOL light (2013)
  9. Kaliszyk, Cezary; Urban, Josef: Automated reasoning service for HOL light (2013)
  10. Sultana, Nik; Blanchette, Jasmin Christian; Paulson, Lawrence C.: LEO-II and Satallax on the Sledgehammer test bench (2013)
  11. Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoff: ATP and presentation service for Mizar formalizations (2013)
  12. Armstrong, Alasdair; Foster, Simon; Struth, Georg: Dependently typed programming based on automated theorem proving (2012)
  13. Baumgartner, Peter; Pelzer, Björn; Tinelli, Cesare: Model evolution with equality -- revised and implemented (2012)
  14. Lawrence, Andrew; Berger, Ulrich; Seisenberger, Monika: Extracting a DPLL algorithm (2012)
  15. Benzmüller, Christoph: Combining and automating classical and non-classical logics in classical higher-order logics (2011)
  16. Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias: Automatic proof and disproof in Isabelle/HOL (2011)
  17. Kunčar, Ondřej: Proving valid quantified Boolean formulas in HOL Light (2011)
  18. Böhme, Sascha; Moskal, Michał; Schulte, Wolfram; Wolff, Burkhart: HOL-Boogie -- an interactive prover-backend for the verifying C compiler (2010)
  19. Böhme, Sascha; Weber, Tjark: Fast LCF-style proof reconstruction for Z3 (2010)
  20. Cramer, Marcos; Koepke, Peter; Kühlwein, Daniel; Schröder, Bernhard: Premise selection in the Naproche system (2010)

1 2 next