Metis
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Automated verification of refinement laws
- HOL-Boogie
- LEO-II
- MetiTarski
- Prosper
- THF0
- Hammer for Coq: automation for dependent type theory
- Isar
- Omnibus
- distcc
- Proof General
- Sledgehammer
- ML4PG
- ESC4
- veriT
- ATP and presentation service for Mizar formalizations
- LEO-II and Satallax on the Sledgehammer test bench
- CVC Lite
- JACK
- HOL(y)Hammer: online ATP service for HOL Light
- TacticToe: learning to prove with tactics
- Machine learning guidance for connection tableaux
- Squolem
- Epigram
- Mella
- SmallCheck
- CSLLean
- CondLean
- KLMLean
- NESCOND
- Gandalf
- E Theorem Prover
- PRocH
- MaLARea
- Monotonox
- SystemOnTPTP
- 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
- Jahob
- Automation for interactive proof: first prototype
- Translating higher-order clauses to first-order clauses
- Eisbach
- Computer assisted reasoning. A Festschrift for Michael J. C. Gordon
- Faster and more complete extended static checking for the Java modeling language
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Automated reasoning service for HOL Light
- Semi-intelligible Isar proofs from machine-generated proofs
- Dependently Typed Programming Based on Automated Theorem Proving
- Tactician
- Proofs and reconstructions
- Encoding monomorphic and polymorphic types
- FloPoCo
- The TPTP World -- infrastructure for automated reasoning
- Proving Valid Quantified Boolean Formulas in HOL Light
- Modular SMT proofs for fast reflexive checking inside Coq
- Automatic proof and disproof in Isabelle/HOL
- Expressing polymorphic types in a many-sorted language
- Extracting a DPLL algorithm
- A learning-based fact selector for Isabelle/HOL
- GAPT
- Extending a Resolution Prover for Inequalities on Elementary Functions
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
- LoAT
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- The Isabelle Framework
- A polymorphic intermediate verification language: design and logical encoding
- The CADE-22 automated theorem proving system competition -- CASC-22
- Large theory reasoning with SUMO at CASC
- Automated reasoning and presentation support for formalizing mathematics in MizAR
- scientific article; zbMATH DE number 4078854 (Why is no real title available?)
- scientific article; zbMATH DE number 4106253 (Why is no real title available?)
- Coq Interval
- Psyche
- Lambda Free RPOs
- Jinja not Java
- Robbins Conjecture
- Walnut
- Model evolution with equality -- revised and implemented
- scientific article; zbMATH DE number 590587 (Why is no real title available?)
- Network Security Policy Verification
- Sqrt_Babylonian
- GoedelGod
- Groebner_Bases
- Group-Ring-Module
- Matrix_Tensor
- PRocH: proof reconstruction for HOL Light
- Superposition for lambda-free higher-order logic
- Extracting verified decision procedures: DPLL and resolution
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- The Matita interactive theorem prover
- Extending Sledgehammer with SMT solvers
- Interactive theorem proving from the perspective of Isabelle/Isar
- Computer-assisted analysis of the Anderson-Hájek ontological controversy
- Frontiers of Combining Systems
- Hipster: integrating theory exploration in a proof assistant
- Mining state-based models from proof corpora
- Fast LCF-Style Proof Reconstruction for Z3
- Premise selection in the Naproche system
This page was built for software: Metis
