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_47zbMath1166.68353OpenAlexW1486518179MaRDI QIDQ5505538
Andrei Paskevich, Konstantin Verchinine, Anatoly V. Anisimov, Alexander Lyaletski
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
Related Items (7)
Beautiful formalizations in Isabelle/Naproche ⋮ Glushkov's evidence algorithm ⋮ A User-friendly Interface for a Lightweight Verification System ⋮ N. G. de Bruijn's contribution to the formalization of mathematics ⋮ The Isabelle/Naproche natural language proof assistant ⋮ A Review of Mathematical Knowledge Management ⋮ Proof assistants: history, ideas and future
Uses Software
Cites Work
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- SAD as a mathematical assistant -- how should we go from here to there?
- Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
- Isabelle/HOL. A proof assistant for higher-order logic
- A refinement of de Bruijn's formal language of mathematics
- Toward Mechanical Mathematics
- System for Automated Deduction (SAD): A Tool for Proof Verification
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- Some problems in the theories of automata and artificial intelligence
This page was built for publication: On Correctness of Mathematical Texts from a Logical and Practical Point of View