swMATH4439MaRDI QIDQ16615FDOQ16615
Author name not available (Why is that?)
Official website: https://www.gilith.com/software/metis/
Source code repository: https://github.com/gilith/metis
Cited In (only showing first 100 items - show all)
- FPTaylor
- tuCLEVER
- Dependently Typed Programming Based on Automated Theorem Proving
- Mining state-based models from proof corpora
- Proofs and reconstructions
- Extracting verified decision procedures: DPLL and resolution
- Title not available (Why is that?)
- Extracting a DPLL algorithm
- Title not available (Why is that?)
- Computer assisted reasoning. A Festschrift for Michael J. C. Gordon
- Modular SMT proofs for fast reflexive checking inside Coq
- Title not available (Why is that?)
- MOIN
- A formal proof of the expressiveness of deep learning
- Proving Valid Quantified Boolean Formulas in HOL Light
- Large theory reasoning with SUMO at CASC
- Extending Sledgehammer with SMT solvers
- Scalable fine-grained proofs for formula processing
- Faster and more complete extended static checking for the Java modeling language
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Computer-assisted analysis of the Anderson-Hájek ontological controversy
- Title not available (Why is that?)
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
- The Isabelle Framework
- Extending a Resolution Prover for Inequalities on Elementary Functions
- Semi-intelligible Isar proofs from machine-generated proofs
- Fast LCF-Style Proof Reconstruction for Z3
- Expressing polymorphic types in a many-sorted language
- Combining and automating classical and non-classical logics in classical higher-order logics
- Machine learning guidance for connection tableaux
- TacticToe: learning to prove with tactics
- Automated verification of refinement laws
- HOL-Boogie
- LEO-II
- Prosper
- distcc
- Isar
- Omnibus
- Proof General
- Sledgehammer
- ML4PG
- ESC4
- veriT
- Premise selection in the Naproche system
- JACK
- CVC Lite
- Epigram
- Mella
- CondLean
- SmallCheck
- CSLLean
- Squolem
- KLMLean
- Gandalf
- NESCOND
- E Theorem Prover
- PRocH
- MaLARea
- Monotonox
- SystemOnTPTP
- Jahob
- Eisbach
- Encoding monomorphic and polymorphic types
- Tactician
- A learning-based fact selector for Isabelle/HOL
- The CADE-22 automated theorem proving system competition -- CASC-22
- Automated reasoning and presentation support for formalizing mathematics in MizAR
- FloPoCo
- GAPT
- LoAT
- Coq Interval
- Psyche
- Lambda Free RPOs
- Jinja not Java
- Robbins Conjecture
- Automated reasoning service for HOL Light
- Walnut
- GoedelGod
- Groebner_Bases
- Group-Ring-Module
- Matrix_Tensor
- Network Security Policy Verification
- Sqrt_Babylonian
- Model evolution with equality -- revised and implemented
- Interactive theorem proving from the perspective of Isabelle/Isar
- ATP and presentation service for Mizar formalizations
- HOL(y)Hammer: online ATP service for HOL Light
- From LCF to Isabelle/HOL
- Extending Sledgehammer with SMT solvers
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Premise selection for mathematics by corpus analysis and kernel methods
- Translating higher-order clauses to first-order clauses
- Frontiers of Combining Systems
- The TPTP World -- infrastructure for automated reasoning
- The Matita interactive theorem prover
- Automatic proof and disproof in Isabelle/HOL
- Hammer for Coq: automation for dependent type theory
- PRocH: proof reconstruction for HOL Light
- Hipster: integrating theory exploration in a proof assistant
This page was built for software: Metis
