Informal and formal constructive mathematics

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
ID Code:2492
Deposited By:Vicki Carleson
Deposited On:05 Nov 2007
Last Modified:18 Nov 2009 16:09

Repository Staff Only: item control page