The Isabelle/Naproche natural language proof assistant
type: Item
instance of: scholarly article
title: The Isabelle/Naproche natural language proof assistant
DOI: 10.1007/978-3-030-79876-5_36
author: Adrian De Lon
author: Peter Koepke
author: Anton Lorenzen
author: Adrian Marti
author: Marcel Schütz
author: Makarius Wenzel
publication date: 2021-12-01T00:00:00Z
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7437104
describes a project that uses: Isabelle/HOL
describes a project that uses: Naproche
describes a project that uses: HOL Light
describes a project that uses: Mizar
describes a project that uses: E Theorem Prover
describes a project that uses: LaTeX
describes a project that uses: Isar
describes a project that uses: ForTheL
describes a project that uses: Lean
MaRDI profile type: Publication
full work available at URL: 978-3-030-79876-5 36
OpenAlex ID: W3178653101
cites work: Premise Selection in the Naproche System
cites work: A survey of languages for formalizing mathematics
cites work: MizAR 40 for Mizar 40
cites work: The Lean Theorem Prover (System Description)
cites work: From LCF to Isabelle/HOL
cites work: Q3150301
cites work: System for Automated Deduction (SAD): A Tool for Proof Verification
cites work: On Correctness of Mathematical Texts from a Logical and Practical Point of View
cites work: Interaction with formal mathematical documents in Isabelle/PIDE
cites work: Q4790672
description: scientific article; zbMATH DE number 7437104