Proofs and reconstructions

DOI10.1007/978-3-319-24246-0_16MaRDI QIDQ2964467zbMATH OpenOpenAlexWikidataFDO

Authors Nik Sultana, Christoph Benzmüller, Lawrence C. Paulson

Publication date 27 February 2017

Published in Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-24246-0_16

zbMATH Keywords

higher-order logicabstract machinesproof reconstruction

Mathematics Subject Classification ID

Higher-order logic (03B16) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• scientific article; zbMATH DE number 1189109
• Semi-intelligible Isar proofs from machine-generated proofs
• Proof reconstruction in classical and nonclassical logics (Diss., TU Darmstadt, 1999)
• scientific article; zbMATH DE number 1612565
• PRocH: proof reconstruction for HOL Light

Cites work

• scientific article; zbMATH DE number 1948188 (Why is no real title available?)
• scientific article; zbMATH DE number 6780833 (Why is no real title available?)
• Combining superposition, sorts and splitting
• Cut-Simulation and Impredicativity
• Foundational proof certificates in first-order logic
• Isabelle. A generic theorem prover
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• LEO-II and Satallax on the Sledgehammer test bench
• Satallax: An Automatic Higher-Order Prover
• Skolemization in simple type theory: the logical and the theoretical points of view
• THF0 – The Core of the TPTP Language for Higher-Order Logic
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0

Cited in

(4)

• scientific article; zbMATH DE number 1189109 (Why is no real title available?)
• PRocH: proof reconstruction for HOL Light
• Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
• Source-Level Proof Reconstruction for Interactive Theorem Proving

Describes a project that uses

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• THF0
• TPTP
• Metis
• z3
• HOL
• Satallax
• Sledgehammer
• E Theorem Prover

This page was built for publication: Proofs and reconstructions

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