Löfwall, Clas and Sjödin, Gunnar (1997) *Informal and formal constructive mathematics.* [SICS Report]

Full text not available from this repository.

## Abstract

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