The following pages link to Metis_ (Q16615):
Displaying 50 items.
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Model evolution with equality -- revised and implemented (Q429586) (← links)
- Computer-assisted analysis of the Anderson-Hájek ontological controversy (Q523303) (← links)
- Combining and automating classical and non-classical logics in classical higher-order logics (Q656826) (← links)
- Automated verification of refinement laws (Q1037397) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- ATP and presentation service for Mizar formalizations (Q1945905) (← links)
- LEO-II and Satallax on the Sledgehammer test bench (Q1948289) (← links)
- HOL(y)Hammer: online ATP service for HOL Light (Q2018657) (← links)
- TacticToe: learning to prove with tactics (Q2031416) (← links)
- Machine learning guidance for connection tableaux (Q2031418) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Extending Sledgehammer with SMT solvers (Q2351158) (← links)
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
- Premise selection for mathematics by corpus analysis and kernel methods (Q2352489) (← links)
- Automation for interactive proof: first prototype (Q2432769) (← links)
- Translating higher-order clauses to first-order clauses (Q2471742) (← links)
- Computer assisted reasoning. A Festschrift for Michael J. C. Gordon (Q2655321) (← links)
- Faster and more complete extended static checking for the Java modeling language (Q2655328) (← links)
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler (Q2655335) (← links)
- Automated Reasoning Service for HOL Light (Q2843009) (← links)
- Dependently Typed Programming Based on Automated Theorem Proving (Q2908568) (← links)
- Proofs and Reconstructions (Q2964467) (← links)
- Encoding Monomorphic and Polymorphic Types (Q2974796) (← links)
- The TPTP World – Infrastructure for Automated Reasoning (Q3066085) (← links)
- Proving Valid Quantified Boolean Formulas in HOL Light (Q3088006) (← links)
- Modular SMT Proofs for Fast Reflexive Checking Inside Coq (Q3100210) (← links)
- Automatic Proof and Disproof in Isabelle/HOL (Q3172879) (← links)
- Expressing Polymorphic Types in a Many-Sorted Language (Q3172884) (← links)
- Extracting a DPLL Algorithm (Q3178287) (← links)
- Extending a Resolution Prover for Inequalities on Elementary Functions (Q3498456) (← links)
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs (Q3498463) (← links)
- Source-Level Proof Reconstruction for Interactive Theorem Proving (Q3523178) (← links)
- The Isabelle Framework (Q3543647) (← links)
- A Polymorphic Intermediate Verification Language: Design and Logical Encoding (Q3557085) (← links)
- The CADE-22 automated theorem proving system competition – CASC-22 (Q3561621) (← links)
- Large theory reasoning with SUMO at CASC (Q3568226) (← links)
- Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar (Q3582702) (← links)
- (Q3809309) (← links)
- (Q3830509) (← links)
- (Q4296179) (← links)
- PRocH: Proof Reconstruction for HOL Light (Q4928443) (← links)
- (Q4989394) (← links)
- Extracting verified decision procedures: DPLL and Resolution (Q5177337) (← links)
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic (Q5191100) (← links)
- The Matita Interactive Theorem Prover (Q5200015) (← links)
- Extending Sledgehammer with SMT Solvers (Q5200019) (← links)
- (Q5219926) (← links)
- Frontiers of Combining Systems (Q5491905) (← links)
