Source-Level Proof Reconstruction for Interactive Theorem Proving

DOI10.1007/978-3-540-74591-4_18zbMATH Open1144.68364OpenAlexW1524804222MaRDI QIDQ3523178FDOQ3523178

Authors: Kong Woei Susanto, Lawrence C. 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

Recommendations

• Automation for interactive proof: first prototype
• Semi-intelligible Isar proofs from machine-generated proofs
• Proofs and reconstructions
• scientific article; zbMATH DE number 1614692
• scientific article; zbMATH DE number 1552511

Mathematics Subject Classification ID

Cited In (26)

• Extending Sledgehammer with SMT solvers
• Scalable fine-grained proofs for formula processing
• Faster and more complete extended static checking for the Java modeling language
• Computer-assisted analysis of the Anderson-Hájek ontological controversy
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• The Isabelle Framework
• Semi-intelligible Isar proofs from machine-generated proofs
• Mining state-based models from proof corpora
• Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version)
• Extracting a DPLL algorithm
• Modular SMT proofs for fast reflexive checking inside Coq
• Encoding monomorphic and polymorphic types
• A learning-based fact selector for Isabelle/HOL
• Sledgehammer: judgement day
• HOL(y)Hammer: online ATP service for HOL Light
• From LCF to Isabelle/HOL
• A light-weight integration of automated and interactive theorem proving
• 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
• Automatic proof and disproof in Isabelle/HOL
• Hammer for Coq: automation for dependent type theory
• A formal proof of the expressiveness of deep learning
• A formal proof of the expressiveness of deep learning
• Proving Valid Quantified Boolean Formulas in HOL Light

Uses Software

• Isabelle
• VAMPIRE
• Metis_
• HOL Light
• Gandalf
• E Theorem Prover

This page was built for publication: Source-Level Proof Reconstruction for Interactive Theorem Proving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3523178)