The Isabelle/Naproche natural language proof assistant

DOI10.1007/978-3-030-79876-5_36MaRDI QIDQ2055899zbMATH OpenOpenAlexFDO

Authors Adrian De Lon, Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz, Makarius Wenzel

Publication date 1 December 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-79876-5_36

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Interpreting mathematical texts in Naproche-SAD
• Beautiful formalizations in Isabelle/Naproche
• scientific article; zbMATH DE number 1696759
• scientific article; zbMATH DE number 3922016
• A proof-centric approach to mathematical assistants

Cites work

• scientific article; zbMATH DE number 1809862 (Why is no real title available?)
• scientific article; zbMATH DE number 1863397 (Why is no real title available?)
• A survey of languages for formalizing mathematics
• From LCF to Isabelle/HOL
• Interaction with formal mathematical documents in Isabelle/PIDE
• MizAR 40 for Mizar 40
• On Correctness of Mathematical Texts from a Logical and Practical Point of View
• Premise selection in the Naproche system
• System for Automated Deduction (SAD): A Tool for Proof Verification
• The Lean theorem prover (system description)

Cited in

(5)

• Eisbach: a proof method language for Isabelle
• Tinycals: step by step tacticals
• CICM'22 system entries
• Isabelle/jEdit – A Prover IDE within the PIDE Framework
• ProofLang: the language of arXiv proofs

Describes a project that uses

Uses Software

• LaTeX
• Naproche
• Lean
• E Theorem Prover
• ForTheL
• HOL Light
• Mizar
• Isar
• Isabelle/HOL

This page was built for publication: The Isabelle/Naproche natural language proof assistant

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