×

Metis_

swMATH ID: 4439
Software Authors: Joe Leslie-Hurd; metis-users@gilith.com
Description: 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.
Homepage: http://www.gilith.com/software/metis/
Related Software: Isabelle/HOL; E Theorem Prover; TPTP; VAMPIRE; z3; HOL Light; Sledgehammer; HOL; Coq; Isabelle; Mizar; MaLARea; Flyspeck; Isar; ML; Satallax; Proof General; SPASS; LEO-II; Gandalf
Cited in: 56 Publications
all top 5

Cited by 94 Authors

10 Blanchette, Jasmin Christian
10 Paulson, Lawrence Charles
10 Urban, Josef
8 Kaliszyk, Cezary
7 Sutcliffe, Geoff
6 Böhme, Sascha
4 Benzmüller, Christoph Ewald
3 Kühlwein, Daniel
3 Nipkow, Tobias
3 Wenzel, Makarius
2 Bentkamp, Alexander
2 Berger, Ulrich
2 Fleury, Mathias
2 Lawrence, Andrew
2 Meng, Jia
2 Seisenberger, Monika
2 Smallbone, Nicholas
2 Struth, Georg
2 Sultana, Nik
1 Abel, Andreas M.
1 Akbarpour, Behzad
1 Alama, Jesse
1 Armstrong, Alasdair
1 Asperti, Andrea
1 Barbosa, Haniel
1 Baumgartner, Peter
1 Besson, Frédéric
1 Bobot, François
1 Bonichon, Richard
1 Boulton, Richard J.
1 Brown, Chad Edward
1 Bulwahn, Lukas
1 Chalin, Patrice
1 Claessen, Koen
1 Coquand, Thierry
1 Cornilleau, Pierre-Emmanuel
1 Cramer, Marcos
1 Cruanes, Simon
1 Czajka, Łukasz
1 Delahaye, David
1 Doligez, Damien
1 Färber, Michael
1 Fontaine, Pascal
1 Foster, Simon
1 Gauthier, Thibault
1 Gransden, Thomas
1 Greenaway, David
1 Hagiya, Masami
1 Heskes, Tom M.
1 Höfner, Peter
1 Hurd, Joe
1 James, Perry R.
1 Johansson, Moa
1 Klakow, Dietrich
1 Koepke, Peter
1 Kumar, Ramana
1 Kunčar, Ondřej
1 Leino, K. Rustan M.
1 Moskal, Michał
1 Nakata, Ikuo
1 Nordvall Forsberg, Fredrik
1 Norell, Ulf
1 Norrish, Michael
1 Paskevich, Andrei
1 Pease, Adam
1 Pelzer, Björn
1 Pichardie, David
1 Popescu, Andrei
1 Quigley, Claire
1 Raman, Rajeev
1 Ricciotti, Wilmer
1 Rosen, Dan
1 Rudnicki, Piotr
1 Rümmer, Philipp
1 Sacerdoti Coen, Claudio
1 Sakai, Kô
1 Schröder, Bernhard
1 Schulte, Wolfram
1 Siegel, Nick
1 Slind, Konrad
1 Smolka, Steffen Juilf
1 Steckermeier, Albert
1 Susanto, Kong Woei
1 Tassi, Enrico
1 Theiss, Frank
1 Tinelli, Cesare
1 Trac, Steven
1 Tsivtsivadze, Evgeni
1 Waldmann, Uwe
1 Walkinshaw, Neil
1 Weber, Leon
1 Weber, Tjark
1 Wolff, Burkhart
1 Woltzenlogel Paleo, Bruno

Citations by Year