1997 Fall Southeastern Sectional Meeting
Atlanta, GA , October 17-19, 1997
Program of Two Sessions on Computer Proofs
Both sessions are in Skiles Classroom Building, Room 171.
Registration is in Skiles, Room 255.
-
Saturday October 18, 1997, 2:30 p.m.-5:20 p.m.
Special Session on Computer Proofs in Set Theory and Logic
Organizer:
Johan G. F. Belinfante,
Georgia Institute of Technology
belinfan@math.gatech.edu
-
2:30 p.m.
The Emergence of Formalized Mathematics
Robert L. Constable*, Cornell University
(926-03-244)
-
3:00 p.m.
A First-order Logic Interactive Theorem Prover for Teaching Geometry
Richard D. Sommer*, Stanford University
Patrick Suppes, Stanford University
(926-03-249)
-
3:30 p.m.
Computer Proofs in Abstract Algebra
Kenneth Kunen*, University of Wisconsin
(926-20-109)
-
4:00 p.m.
On the decidability of word problems in quasi-varieties.
David A. McAllester*, AT\&T Research
(926-03-245)
-
4:30 p.m.
The Comprehension Schema in Tableaux
Benjamin Price Shults*, Kenyon College
(926-04-102)
-
5:00 p.m.
Mizar - a proof assistant
Piotr Rudnicki*,
(926-00-155)
-
Sunday October 19, 1997, 9:00 a.m.-11:20 a.m.
Special Session on Computer Proofs in Set Theory and Logic
Organizers:
Johan G. F. Belinfante,
Georgia Institute of Technology
belinfan@math.gatech.edu
-
9:00 a.m.
A set theory for mechanized mathematics
William M. Farmer*, St. Cloud State University
(926-04-103)
-
9:30 a.m.
Applications of Set Theoretic Reasoning in Automated Deduction
Robert L Veroff*, University of New Mexico
(926-68-101)
-
10:00 a.m.
Automated Equational Deduction
William McCune*,
Mathematics and Computer Science Division, Argonne National Laboratory
(926-03-176)
-
10:30 a.m.
Instance-based Deduction Techniques for Set Theory
David A Plaisted*, UNC-Chapel Hill
Yunshan Zhu, UNC-Chapel Hill
(926-03-239)
-
11:00 a.m.
Experimenting with OTTER
Thomas Jech*,
(926-03-12)
Evans Harrell has set up a
local website for general information about the conference.
Updated: 1997 October 17.