Characteristics of de Bruijn’s early proof checker Automath

DOI10.3233/FI-222112MaRDI QIDQ5089679zbMATH OpenWikidataFDO

Authors Herman Geuvers, Rob Nederpelt

Publication date 14 July 2022

Published in Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2203.01173

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Zen and the art of formalisation
• N. G. de Bruijn's contribution to the formalization of mathematics
• scientific article; zbMATH DE number 2154395
• A new implementation of Automath

Cites work

• scientific article; zbMATH DE number 3928956 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 108365 (Why is no real title available?)
• scientific article; zbMATH DE number 1531624 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 3331288 (Why is no real title available?)
• scientific article; zbMATH DE number 3076631 (Why is no real title available?)
• A Brief Overview of Agda – A Functional Language with Dependent Types
• A Brief Overview of Mizar
• A new implementation of Automath
• A useful \(\lambda\)-notation
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• On the rules of suppositions in formal logic
• Proof assistants: history, ideas and future
• Proof-assistants using dependent type systems
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• The Lean 4 theorem prover and programming language
• The calculus of constructions
• The seventeen provers of the world. Foreword by Dana S. Scott..
• Translations between Gentzen-Prawitz and Jaśkowski-Fitch natural deduction proofs
• Type theory and formal proof. An introduction

Cited in

(1)

• Characteristics of de Bruijn's early proof checker Automath

Describes a project that uses

Uses Software

• Coq
• Isabelle/HOL
• HOL
• Automath
• Agda
• Lean

This page was built for publication: Characteristics of de Bruijn’s early proof checker Automath

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