Formal proof sketches

DOI10.1007/978-3-540-24849-1_24MaRDI QIDQ5712318zbMATH OpenOpenAlexFDO

Authors Freek Wiedijk

Publication date 23 December 2005

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

Full work available at URL https://doi.org/10.1007/b98246

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Formal proof
• On Formal Proofs
• Formal proof -- theory and practice
• Sketch-as-proof
• scientific article; zbMATH DE number 1024410
• Proof versus formalization
• scientific article; zbMATH DE number 5486212
• Informal proof, formal proof, formalism
• Formal Proof: Reconciling Correctness and Understanding

Cited in

(23)

• Flexary connectives in Mizar
• Theorem proving as constraint solving with coherent logic
• Prime simplicity
• Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book
• Computerizing mathematical text with MathLang
• \textsc{Plat}{\(\Omega\)}: a mediator between text-editors and proof assistance systems
• Four decades of \textsc{Mizar}. Foreword
• Checking proofs
• A Brief Overview of Mizar
• Mizar: state-of-the-art and beyond
• A Declarative Language for the Coq Proof Assistant
• Formal Proof: Reconciling Correctness and Understanding
• scientific article; zbMATH DE number 2154392 (Why is no real title available?)
• NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF
• Liquid tensor experiment
• Proof auditing formalised mathematics
• Translating between language and logic: what is easy and what is difficult
• A foundational view on integration problems
• The challenge of computer mathematics
• A path to faithful formalizations of mathematics
• A Dynamic Poincaré Principle
• A formalization of all notions in the statement of a theorem by Deligne
• A proof-centric approach to mathematical assistants

Describes a project that uses

Uses Software

• Isabelle/Isar

This page was built for publication: Formal proof sketches

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