SASW@MIT-MC.ARPA (Steven A. Swernofsky) (11/04/85)
Received: from CSNET-RELAY.ARPA (csnet-pdn-gw) by rand-unix.ARPA; Sun, 3 Nov 85 18:10:10 pst
Received: from smu by csnet-relay.csnet id ad21012; 3 Nov 85 21:12 EST
Received: by csevax.smu (4.12/4.7)
id AA00249; Sun, 3 Nov 85 11:20:37 cst
Date: 3 Nov 1985 11:20-CST
From: leff%smu.csnet@CSNET-RELAY.ARPA
Subject: Forwarded from AIList to net.math.symbolic
Message-Id: <499886400/leff@smu>
Date: Thu, 31 Oct 85 02:24:17 EST
From: "Steven A. Swernofsky" <SASW@MIT-MC.ARPA>
Subject: Seminar - Mechanical Verification of Mathematics (BBN)
Thursday 31, October 10: 30am Room: BBN Labs, 10 Moulton Street,
2nd floor large conference room
BBN Laboratories
Science Development Program
AI Seminars
Toward the Mechanical Verification of Abstract Mathematics
David McAllester
MIT AI Laboratory
To mechanically verify a mathematical argument one must
translate the argument into some formal language. Many
mathematicians doubt that it will ever be practical to translate
arbitrary mathematical arguments into a completely formal language.
This talk will present a formal language called ONTIC which extends
set theory in a way that supports an "object oriented" style of
mathematical description. Ontic has been used to formally define some
basic concepts of modern algebra, real analysis, and homotopy theory.
We feel that any branch of modern mathematics can be concisely
expressed in ONTIC. Furthermore it seems practical to translate any
mathematical proof into a sequence of ONTIC formulas. A theorem-
proving system has been constructed for ONTIC and some simple
verifications have been done.