Supporting the formal verification of mathematical texts

DOI10.1016/j.jal.2005.10.010zbMath1107.68104OpenAlexW2086329789MaRDI QIDQ865656

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)

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Rippling: A heuristic for guiding inductive proofs
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Isabelle/HOL. A proof assistant for higher-order logic
• Theorem proving in higher order logics. 12th international conference, TPHOLs '99. Nice, France, September 14--17, 1999. Proceedings
• A comparison of Mizar and Isar
• A refinement of de Bruijn's formal language of mathematics
• Productive use of failure in inductive proof
• Anaphora and Discourse Structure
• Toward Mechanical Mathematics
• Ωmega: Towards a mathematical assistant