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

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

Mathematics Subject Classification ID

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

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

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

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