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

DOI10.1007/978-3-031-10769-6_2OpenAlexW4289104007MaRDI QIDQ2104491

Gilles Dowek

Publication date: 7 December 2022

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)

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the unity of logic
• Theorem proving modulo
• Programming with Higher-Order Logic
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• A framework for defining logics
• Proof normalization modulo
• Unifying Classical and Intuitionistic Logics for Computational Control
• Some Axioms for Mathematics

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