A framework for checking proofs naturally

Abstract. 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 cre-ated 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 deriva-tions 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 editor. CAL consists of user interface, a general purpose parser and a checker for checking proofs of NF derivation games. NF/CAL system has been successfully used as an education system for teaching computation and logic for undergraduate students for about 8 years. We will give an overview of the NF/CAL system both from theoretical and practical sides.