The Isabelle/Naproche natural language proof assistant

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

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

Publication date: 1 December 2021

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)

Related Items (2)

CICM'22 system entries ⋮ Tinycals: Step by Step Tacticals

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• MizAR 40 for Mizar 40
• A survey of languages for formalizing mathematics
• From LCF to Isabelle/HOL
• Interaction with formal mathematical documents in Isabelle/PIDE
• The Lean Theorem Prover (System Description)
• System for Automated Deduction (SAD): A Tool for Proof Verification
• On Correctness of Mathematical Texts from a Logical and Practical Point of View
• Premise Selection in the Naproche System

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