The Isabelle/Naproche natural language proof assistant

DOI10.1007/978-3-030-79876-5_36OpenAlexW3178653101MaRDI QIDQ2055899FDOQ2055899

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

Publication date: 1 December 2021

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

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

Mathematics Subject Classification ID

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

Cites Work

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

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

Uses Software

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

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)