Automated constructivization of proofs

DOI10.1007/978-3-662-54458-7_28MaRDI QIDQ2988387zbMATH OpenOpenAlexFDO

Authors Frédéric Gilbert

Publication date 19 May 2017

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-01516788/file/constructivization.pdf

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07)

Recommendations

• scientific article; zbMATH DE number 65537
• scientific article; zbMATH DE number 517083
• Herbrand constructivization for automated intuitionistic theorem proving
• A translation characterizing the constructive content of classical theories
• Classical proofs as programs: how, what and why

Cites work

• Eine Darstellung der Intuitionistischen Logik in der Klassischen
• scientific article; zbMATH DE number 3614784 (Why is no real title available?)
• Intuitionistische Untersuchungen der formalistischen Logik
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
• Polarizing double-negation translations
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• Über das Verhältnis zwischen intuitionistischer und klassischer Arithmetik

Cited in

(17)

• Autarkic computations in formal proofs
• Herbrand constructivization for automated intuitionistic theorem proving
• Automation for interactive proof: first prototype
• Classical mathematics for a constructive world
• Automated Certification of Implicit Induction Proofs
• Proof Documents for Automated Origami Theorem Proving
• Automating Change of Representation for Proofs in Discrete Mathematics
• Automating Proofs in Category Theory
• scientific article; zbMATH DE number 978243 (Why is no real title available?)
• Automatic Learning of Proof Methods in Proof Planning
• scientific article; zbMATH DE number 2100042 (Why is no real title available?)
• Automating Inductive Proofs Using Theory Exploration
• How to make ad hoc proof automation less ad hoc
• scientific article; zbMATH DE number 3894495 (Why is no real title available?)
• scientific article; zbMATH DE number 6938205 (Why is no real title available?)
• Automated Improving of Proof Legibility in the Mizar System
• Improving automation for higher-order proof steps

Describes a project that uses

Uses Software

• Zenon
• leanCoP
• TPTP

This page was built for publication: Automated constructivization of proofs

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