Source-Level Proof Reconstruction for Interactive Theorem Proving

DOI10.1007/978-3-540-74591-4_18MaRDI QIDQ3523178zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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
• Semi-intelligible Isar proofs from machine-generated proofs
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• The Isabelle Framework
• Mining state-based models from proof corpora
• Extracting a DPLL algorithm
• Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version)
• Modular SMT proofs for fast reflexive checking inside Coq
• A learning-based fact selector for Isabelle/HOL
• Encoding monomorphic and polymorphic types
• Sledgehammer: judgement day
• HOL(y)Hammer: online ATP service for HOL Light
• From LCF to Isabelle/HOL
• Extending Sledgehammer with SMT solvers
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Premise selection for mathematics by corpus analysis and kernel methods
• A light-weight integration of automated and interactive theorem proving
• 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

Describes a project that uses

Uses Software

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

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)