|
Abstract:
From the beginning of the twentieth century, mathematicians thought about formalizing their activity. First, they formalized some logics, mainly arithmetics. Later, they wanted to define clearly what is a proof. Then came the formalization of meta-properties of a logical system: consistency, completeness. Computer science entered that field
with the development of logical frameworks. A logical framework is a formal system in which one can define logics, write and check some proofs in these logics. Hopefully, logical frameworks will also soon be able to handle meta-properties. Natural Framework (NF for short) is a logical framework. It is intended to be as simple as possible, understandable without the heavy classical logic background, e.g. dependent types which are needed for the judgments-as-types approach used in LF.
|