Metis_

swMATH4439MaRDI QIDQ16615FDOQ16615

Author name not available (Why is that?)

Cited In (56)

• 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
• Dependently Typed Programming Based on Automated Theorem Proving
• 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
• Mining state-based models from proof corpora
• Proofs and reconstructions
• 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
• Extracting verified decision procedures: DPLL and resolution
• Title not available (Why is that?)
• Machine learning guidance for connection tableaux
• TacticToe: learning to prove with tactics
• Extracting a DPLL algorithm
• Automated verification of refinement laws
• 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
• Premise selection in the Naproche system
• Encoding monomorphic and polymorphic types
• A learning-based fact selector for Isabelle/HOL
• Title not available (Why is that?)
• The CADE-22 automated theorem proving system competition -- CASC-22
• Automated reasoning and presentation support for formalizing mathematics in MizAR
• Automated reasoning service for HOL Light
• 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
• A formal proof of the expressiveness of deep learning
• PRocH: proof reconstruction for HOL Light
• Hipster: integrating theory exploration in a proof assistant
• 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
• A polymorphic intermediate verification language: design and logical encoding
• Large theory reasoning with SUMO at CASC

This page was built for software: Metis_