A framework for checking proofs naturally

We propose a natural framework, called NF, which supports development of formal proofs on a computer. NF is based on a theory of Judgments and Derivations. NF is designed by observing how working mathematical theories are created and developed. Our observation is that the notions of judgments and derivations are the two fundamental notions used in any mathematical activity. We have therefore developed a theory of judgments and derivations and designed a framework in which the theory provides a uniform and common play ground on which various mathematical theories can be defined as derivation games and can be played, namely, can write and check proofs. NF is equipped with a higher-order intuitionistic logic and derivations (proofs) are described following Gentzen's natural deduction style. NF is part of an interactive computer environment CAL (Computation and Logic) and it is also referred to as NF/CAL. CAL is written in Emacs Lisp and it is run within a special buffer of the Emacs ...

• Type: Journal
• Year: 2008
• Where: JIIS
• Authors: Masahiko Sato
• Keywords: Derivation Games, JIIS 2008, Judgments, Mathematical Theories