Metis_

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_