From the universality of mathematical truth to the interoperability of proof systems

DOI10.1007/978-3-031-10769-6_2MaRDI QIDQ2104491zbMATH OpenOpenAlexFDO

Authors Gilles Dowek

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-10769-6_2

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• scientific article; zbMATH DE number 7034428 (Why is no real title available?)
• scientific article; zbMATH DE number 6614320 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• A framework for defining logics
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• On the unity of logic
• Programming with higher-order logic.
• Proof normalization modulo
• Some Axioms for Mathematics
• Theorem proving modulo
• Unifying classical and intuitionistic logics for computational control

Cited in

(2)

• Evidence for Set-Theoretic Truth and the Hyperuniverse Programme
• Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics

Describes a project that uses

Uses Software

• GeoCoq
• Lean
• Agda
• Matita
• HOL
• Mizar
• Isabelle/HOL
• Coq

This page was built for publication: From the universality of mathematical truth to the interoperability of proof systems

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