Proofs and reconstructions

DOI10.1007/978-3-319-24246-0_16zbMATH Open1471.68319OpenAlexW2222056609WikidataQ57382545 ScholiaQ57382545MaRDI QIDQ2964467FDOQ2964467

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

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

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)

Cites Work

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

Cited In (4)

• Title not available (Why is that?)
• Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
• PRocH: proof reconstruction for HOL Light
• Source-Level Proof Reconstruction for Interactive Theorem Proving

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)