Löfwall, Clas and Sjödin, Gunnar (1997) Informal and formal constructive mathematics. [SICS Report]
Full text not available from this repository.
We first prove, informally but constructively, that Z is a ring without zero-divisors. Then, using Per Martin-Löf's type theory, we establish the same result formally. This is done following the informal reasoning closely. The proofs are automatically checked by using the proof-checker ``TWB'' developed by us at SICS. In the proofs we use only the basic set-theoretic axioms in type theory.
|Item Type:||SICS Report|
|Uncontrolled Keywords:||Type theory, Constructive mathematics, Automatic proof checking, Formal and informal basic arithmetic|
|Deposited By:||Vicki Carleson|
|Deposited On:||05 Nov 2007|
|Last Modified:||18 Nov 2009 16:09|
Repository Staff Only: item control page