Pages that link to "Item:Q3523178"
From MaRDI portal
The following pages link to Source-Level Proof Reconstruction for Interactive Theorem Proving (Q3523178):
Displaying 25 items.
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Computer-assisted analysis of the Anderson-Hájek ontological controversy (Q523303) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- HOL(y)Hammer: online ATP service for HOL Light (Q2018657) (← 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)
- Translating higher-order clauses to first-order clauses (Q2471742) (← links)
- Faster and more complete extended static checking for the Java modeling language (Q2655328) (← links)
- Encoding Monomorphic and Polymorphic Types (Q2974796) (← 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)
- Extracting a DPLL Algorithm (Q3178287) (← links)
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs (Q3498463) (← links)
- The Isabelle Framework (Q3543647) (← links)
- Extending Sledgehammer with SMT Solvers (Q5200019) (← links)
- Mining State-Based Models from Proof Corpora (Q5495930) (← links)
- A light-weight integration of automated and interactive theorem proving (Q5741559) (← links)
- Sledgehammer: Judgement Day (Q5747754) (← links)
- A formal proof of the expressiveness of deep learning (Q5915784) (← links)
- Scalable fine-grained proofs for formula processing (Q5919479) (← links)
- A formal proof of the expressiveness of deep learning (Q5919583) (← links)
