On Correctness of Mathematical Texts from a Logical and Practical Point of View
From MaRDI portal
Publication:5505538
DOI10.1007/978-3-540-85110-3_47zbMATH Open1166.68353OpenAlexW1486518179MaRDI QIDQ5505538FDOQ5505538
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
Recommendations
Cites Work
- Title not available (Why is that?)
- System for Automated Deduction (SAD): A Tool for Proof Verification
- SAD as a mathematical assistant -- how should we go from here to there?
- Isabelle/HOL. A proof assistant for higher-order logic
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Mathematical Knowledge Management
- Some problems in the theories of automata and artificial intelligence
- Toward Mechanical Mathematics
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
- A refinement of de Bruijn's formal language of mathematics
- Mathematical Knowledge Management
Cited In (15)
- A user-friendly interface for a lightweight verification system
- Interpreting mathematical texts in Naproche-SAD
- Title not available (Why is that?)
- Beautiful formalizations in Isabelle/Naproche
- System for Automated Deduction (SAD): A Tool for Proof Verification
- Supporting the formal verification of mathematical texts
- Narrative Structure of Mathematical Texts
- N. G. de Bruijn's contribution to the formalization of mathematics
- Title not available (Why is that?)
- Glushkov's evidence algorithm
- A Review of Mathematical Knowledge Management
- The Isabelle/Naproche natural language proof assistant
- Proof assistants: history, ideas and future
- Verifying and Invalidating Textbook Proofs Using Scunak
- SAD as a mathematical assistant -- how should we go from here to there?
Uses Software
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)