Metis_
From MaRDI portal
Software:16615
swMATH4439MaRDI QIDQ16615FDOQ16615
Author name not available (Why is that?)
Cited In (56)
- Mining State-Based Models from Proof Corpora
- Extracting verified decision procedures: DPLL and Resolution
- 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
- Dependently Typed Programming Based on Automated Theorem Proving
- Computer-assisted analysis of the Anderson-Hájek ontological controversy
- The TPTP World – Infrastructure for Automated Reasoning
- Automatic Proof and Disproof in Isabelle/HOL
- Title not available (Why is that?)
- 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
- Premise Selection in the Naproche System
- Fast LCF-Style Proof Reconstruction for Z3
- Combining and automating classical and non-classical logics in classical higher-order logics
- A Polymorphic Intermediate Verification Language: Design and Logical Encoding
- Title not available (Why is that?)
- Machine learning guidance for connection tableaux
- TacticToe: learning to prove with tactics
- Automated verification of refinement laws
- Title not available (Why is that?)
- Computer assisted reasoning. A Festschrift for Michael J. C. Gordon
- PRocH: Proof Reconstruction for HOL Light
- Proofs and Reconstructions
- Extending Sledgehammer with SMT Solvers
- The Matita Interactive Theorem Prover
- A learning-based fact selector for Isabelle/HOL
- Title not available (Why is that?)
- Model evolution with equality -- revised and implemented
- ATP and presentation service for Mizar formalizations
- Hipster: Integrating Theory Exploration in a Proof Assistant
- HOL(y)Hammer: online ATP service for HOL Light
- Expressing Polymorphic Types in a Many-Sorted Language
- From LCF to Isabelle/HOL
- Extracting a DPLL Algorithm
- 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
- Modular SMT Proofs for Fast Reflexive Checking Inside Coq
- Encoding Monomorphic and Polymorphic Types
- Automated Reasoning Service for HOL Light
- Hammer for Coq: automation for dependent type theory
- A formal proof of the expressiveness of deep learning
- Automation for interactive proof: first prototype
- LEO-II and Satallax on the Sledgehammer test bench
- Proving Valid Quantified Boolean Formulas in HOL Light
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- The CADE-22 automated theorem proving system competition – CASC-22
- Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar
- Large theory reasoning with SUMO at CASC
This page was built for software: Metis_