Re: AutoMath

Article View: net.math.symbolic

Article #13

#13

From: Tim Rentsch
Date: Mon, 24 Sep 1984 22:20

13 lines
916 bytes

AutoMath is a tool for proof verification.

The idea is to take a proof and write it in a very formal way, so that the
mechanisms used in the proof can be mechanically verified.  This is done
using a type-checking scheme similar in concept to those used in modern
programming languages.

For references, the mathematician N. G. DeBruijn would be a good place to
start.

cheers,

Tim

Technical Details

Message-ID: <59@unc.UUCP>

Path: arc1-ca.pugleaf.net!utzoo!watmath!clyde!burl!ulysses!unc!rentsch

References: <80@gymble.UUCP>

Show Full Headers

Complete Article Headers

Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.1 6/24/83; site unc.UUCP
Path: arc1-ca.pugleaf.net!utzoo!watmath!clyde!burl!ulysses!unc!rentsch
From: rentsch@unc.UUCP (Tim Rentsch)
Newsgroups: net.math.symbolic
Subject: Re: AutoMath
Message-ID: <59@unc.UUCP>
Date: Mon, 24-Sep-84 18:20:38 EDT
Article-I.D.: unc.59
Posted: Mon Sep 24 18:20:38 1984
Date-Received: Wed, 26-Sep-84 07:25:38 EDT
References: <80@gymble.UUCP>
Organization: CS Dept., U. of N. Carolina at Chapel Hill
Lines: 13

Reply to Parent Message