Proofs and Reconstructions

DOI10.1007/978-3-319-24246-0_16zbMath1471.68319OpenAlexW2222056609WikidataQ57382545 ScholiaQ57382545MaRDI QIDQ2964467

Nik Sultana, Christoph Benzmüller, Lawrence Charles 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)

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Isabelle. A generic theorem prover
• 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
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• THF0 – The Core of the TPTP Language for Higher-Order Logic
• Cut-Simulation and Impredicativity
• Foundational Proof Certificates in First-Order Logic

This page was built for publication: Proofs and Reconstructions