Automated Constructivization of Proofs

DOI10.1007/978-3-662-54458-7_28zbMath1486.03025OpenAlexW2614058880MaRDI QIDQ2988387

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)

Uses Software

• TPTP
• Zenon
• leanCoP

Cites Work

• Unnamed Item
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Polarizing Double-Negation Translations
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
• Über das Verhältnis zwischen intuitionistischer und klassischer Arithmetik
• Intuitionistische Untersuchungen der formalistischen Logik
• Eine Darstellung der Intuitionistischen Logik in der Klassischen

This page was built for publication: Automated Constructivization of Proofs