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
Related Items
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
