Source-Level Proof Reconstruction for Interactive Theorem Proving
From MaRDI portal
Publication:3523178
DOI10.1007/978-3-540-74591-4_18zbMath1144.68364OpenAlexW1524804222MaRDI QIDQ3523178
Kong Woei Susanto, Lawrence Charles Paulson
Publication date: 2 September 2008
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-74591-4_18
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (25)
Semi-intelligible Isar proofs from machine-generated proofs ⋮ Automatic Proof and Disproof in Isabelle/HOL ⋮ Extracting a DPLL Algorithm ⋮ A learning-based fact selector for Isabelle/HOL ⋮ Faster and more complete extended static checking for the Java modeling language ⋮ Hammer for Coq: automation for dependent type theory ⋮ Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs ⋮ Encoding Monomorphic and Polymorphic Types ⋮ The Isabelle Framework ⋮ Translating higher-order clauses to first-order clauses ⋮ Computer-assisted analysis of the Anderson-Hájek ontological controversy ⋮ A light-weight integration of automated and interactive theorem proving ⋮ Sledgehammer: Judgement Day ⋮ HOL(y)Hammer: online ATP service for HOL Light ⋮ A formal proof of the expressiveness of deep learning ⋮ From LCF to Isabelle/HOL ⋮ A formal proof of the expressiveness of deep learning ⋮ Extending Sledgehammer with SMT Solvers ⋮ Scalable fine-grained proofs for formula processing ⋮ Proving Valid Quantified Boolean Formulas in HOL Light ⋮ Modular SMT Proofs for Fast Reflexive Checking Inside Coq ⋮ Mining State-Based Models from Proof Corpora ⋮ Extending Sledgehammer with SMT solvers ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) ⋮ Premise selection for mathematics by corpus analysis and kernel methods
Uses Software
This page was built for publication: Source-Level Proof Reconstruction for Interactive Theorem Proving
