Supporting the formal verification of mathematical texts

DOI10.1016/J.JAL.2005.10.010MaRDI QIDQ865656zbMATH OpenOpenAlexFDO

Authors Claus Zinn

Publication date 20 February 2007

Published in Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jal.2005.10.010

zbMATH Keywords

proof planningdiscourse processingmodelling mathematical language and reasoning

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• On Correctness of Mathematical Texts from a Logical and Practical Point of View
• Computer theorem proving in mathematics
• Mathematical Knowledge Management
• Formal proof -- theory and practice
• Mathematical Knowledge Management

Cites work

• scientific article; zbMATH DE number 1629953 (Why is no real title available?)
• scientific article; zbMATH DE number 1696759 (Why is no real title available?)
• scientific article; zbMATH DE number 4148033 (Why is no real title available?)
• scientific article; zbMATH DE number 4072439 (Why is no real title available?)
• scientific article; zbMATH DE number 4074537 (Why is no real title available?)
• scientific article; zbMATH DE number 3624817 (Why is no real title available?)
• scientific article; zbMATH DE number 2154392 (Why is no real title available?)
• scientific article; zbMATH DE number 2190569 (Why is no real title available?)
• scientific article; zbMATH DE number 3231608 (Why is no real title available?)
• scientific article; zbMATH DE number 3331288 (Why is no real title available?)
• A comparison of Mizar and Isar
• A refinement of de Bruijn's formal language of mathematics
• Anaphora and discourse structure
• Assertion-level proof representation with under-specification
• Combining superposition, sorts and splitting
• Isabelle/HOL. A proof assistant for higher-order logic
• Productive use of failure in inductive proof
• Rippling: A heuristic for guiding inductive proofs
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• The OYSTER-CLAM system
• Theorem proving in higher order logics. 12th international conference, TPHOLs '99. Nice, France, September 14--17, 1999. Proceedings
• Toward Mechanical Mathematics
• \(\Omega\)\textsc{mega}: towards a mathematical assistant

Cited in

(9)

• Computer verification of mathematical reasoning
• Mathematical Knowledge Management
• A user-friendly interface for a lightweight verification system
• Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors
• scientific article; zbMATH DE number 1951637 (Why is no real title available?)
• Verifying and Invalidating Textbook Proofs Using Scunak
• Mathematical Knowledge Management
• Towards verified handwritten calculational proofs (short paper)
• Faithfully reflecting the structure of informal mathematical proofs into formal type theories

Describes a project that uses

Uses Software

• Coq
• Isabelle/HOL
• Isabelle/Isar
• IsaPlanner
• OTTER
• Isar
• Mizar
• Proof General
• Nuprl
• Automath
• Lambda-Clam
• CLAM
• XBarnacle
• Oyster

This page was built for publication: Supporting the formal verification of mathematical texts

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