scientific article; zbMATH DE number 7178362

MaRDI QIDQ5219927zbMATH OpenFDO

Authors Christine Paulin-Mohring

Publication date 9 March 2020

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cited in

(12)

• Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
• Variants of Gödel's ontological proof in a natural deduction calculus
• Interacting with Modal Logics in the Coq Proof Assistant
• Para-disagreement logics and their implementation through embedding in Coq and SMT
• Formal Verification of Bit-Vector Invertibility Conditions in Coq
• Learning Proof Transformations and Its Applications in Interactive Theorem Proving
• A Coq implementation of the program algebra in Jifeng He's new roadmap for linking theories of programming
• Lean4Less: eliminating definitional equalities from Lean via an extensional-to-intensional translation
• Conservativity of type theory over higher-order arithmetic
• Countability of inductive types formalized in the object-logic level
• An interactive SMT tactic in Coq using abductive reasoning
• Types, Tableaus and Gödel’s God in Isabelle/HOL

Describes a project that uses

Uses Software

• Ynot
• A3PAT
• Coq

This page was built for publication:

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