On Correctness of Mathematical Texts from a Logical and Practical Point of View

DOI10.1007/978-3-540-85110-3_47MaRDI QIDQ5505538zbMATH OpenOpenAlexFDO

Authors Konstantin Verchinine, Andrei Paskevich, Alexander Lyaletski, Anatoly V. Anisimov

Publication date 27 January 2009

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

Full work available at URL https://doi.org/10.1007/978-3-540-85110-3_47

Mathematics Subject Classification ID

Computing methodologies for text processing; mathematical typography (68U15)

Recommendations

• System for Automated Deduction (SAD): A Tool for Proof Verification
• SAD as a mathematical assistant -- how should we go from here to there?
• Mathematical Knowledge Management
• Interpreting mathematical texts in Naproche-SAD
• scientific article; zbMATH DE number 2079533

Cites work

• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• A refinement of de Bruijn's formal language of mathematics
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Mathematical Knowledge Management
• Mathematical Knowledge Management
• SAD as a mathematical assistant -- how should we go from here to there?
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Some problems in the theories of automata and artificial intelligence
• System for Automated Deduction (SAD): A Tool for Proof Verification
• Toward Mechanical Mathematics

Cited in

(15)

• Proof assistants: history, ideas and future
• The Isabelle/Naproche natural language proof assistant
• Beautiful formalizations in Isabelle/Naproche
• Interpreting mathematical texts in Naproche-SAD
• System for Automated Deduction (SAD): A Tool for Proof Verification
• A Review of Mathematical Knowledge Management
• scientific article; zbMATH DE number 4099291 (Why is no real title available?)
• scientific article; zbMATH DE number 1961525 (Why is no real title available?)
• Glushkov's evidence algorithm
• A user-friendly interface for a lightweight verification system
• Narrative Structure of Mathematical Texts
• Verifying and Invalidating Textbook Proofs Using Scunak
• N. G. de Bruijn's contribution to the formalization of mathematics
• SAD as a mathematical assistant -- how should we go from here to there?
• Supporting the formal verification of mathematical texts

Describes a project that uses

Uses Software

• Theorema
• PVS
• SAD
• ForTheL
• Mizar
• Isar
• Automath

This page was built for publication: On Correctness of Mathematical Texts from a Logical and Practical Point of View

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