🚀 go-pugleaf

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.