AMS Sectional Meeting Program by Special Session
Current as of Tuesday, April 12, 2005 15:10:41
2002 AMS and MAA Spring Southeastern Section Meetings
Atlanta, GA, March 810, 2002
Meeting #975
Associate secretaries: John L Bryant, AMS bryant@math.fsu.edu
Special Session on Automated Reasoning in Mathematics and Logic

Friday March 8, 2002, 2:10 p.m.5:30 p.m.
Special Session on Automated Reasoning in Mathematics and Logic, I
Room 240, Skiles Classroom Building
Organizers:
Johan G. F. Belinfante, Georgia Institute of Technology belinfan@math.gatech.edu

2:10 p.m.
Machines Reasoning about Machines.
J Strother Moore*, University of Texas at Austin
(9756885) 
2:40 p.m.
The Method of Proof Sketches.
Robert L Veroff*, University of New Mexico
(9756895) 
3:10 p.m.
A Spectrum of Applications of Automated Reasoning.
Larry Wos*, Argonne National Laboratory
(9750384) 
3:40 p.m.
Extending Decision Procedures with Induction Schemes.
Deepak Kapur*, University of New Mexico
(9756897) 
4:10 p.m.
A logical framework for computerverified proofs in undergraduate mathematics.
Richard Sommer*, Stanford University
(97503133) 
4:40 p.m.
The Comprehension Schema in Tableaux: Toward Wos' Eighth Research Problem.
Benjamin Price Shults*, Western Carolina University
(9750391) 
5:10 p.m.
Automated Reasoning about the Zermelovon Neumann Cumulative Hierarchy.
Johan G. F. Belinfante*, Georgia Inst. Technology
(9750383)

2:10 p.m.

Saturday March 9, 2002, 10:15 a.m.12:35 p.m.
Special Session on Automated Reasoning in Mathematics and Logic, II
Room 240, Skiles Classroom Building
Organizers:
Johan G. F. Belinfante, Georgia Institute of Technology belinfan@math.gatech.edu

10:15 a.m.
Algorithms for Reducing Structures in Verification.
Raffaella Gentilini, University of Udine
Carla Piazza, University of Udine
Alberto Policriti*, University of Udine
(97568226) 
10:45 a.m.
A modularization mechanism for interactive proofdevelopment.
Eugenio G. Omodeo*, Universita` di L'Aquila, Dipartimento di Informatica
Jacob T. Schwartz, New York University, Dept. of Computer Science
(97503104) 
11:15 a.m.
Automated validation of threevariable formulations of setpairing.
Andrea Formisano*, Dip. di Matematica e Informatica, Univ. di Perugia
Eugenio G Omodeo, Dip. di Matematica Pura e Applicata, Univ. di L'Aquila
Alberto Policriti, Dip. di Matematica e Informatica, Univ. di Udine
(97503102) 
11:45 a.m.
Translation of Resolution Proofs into Higher Order Natural Deduction.
Hans de Nivelle*, Max Planck Institut
(97503135) 
12:15 p.m.
Discussion

10:15 a.m.

Saturday March 9, 2002, 3:05 p.m.5:25 p.m.
Special Session on Automated Reasoning in Mathematics and Logic, III
Room 240, Skiles Classroom Building
Organizers:
Johan G. F. Belinfante, Georgia Institute of Technology belinfan@math.gatech.edu

3:05 p.m.
Mechanization of the System of the Principia Mathematica of Russell and Whitehead.
M. Randall Holmes*, Boise State University
(97503109) 
3:35 p.m.
Interpreting set theory in the variablefree, equational calculus of relations.
Steven R Givant*, Mills College
(9750390) 
4:05 p.m.
Finite Model Search and Single Axioms.
William McCune*, Argonne National Laboratory
(9750393) 
4:35 p.m.
Proving theorems automatically and interactively with TPS.
Peter B. Andrews*, Carnegie Mellon University
(9750386) 
5:05 p.m.
Specifying Tournament Schedules for General Model Generators.
Hantao Zhang*, University of Iowa
(97568111)

3:05 p.m.

Sunday March 10, 2002, 10:10 a.m.12:20 p.m.
Special Session on Automated Reasoning in Mathematics and Logic, IV
Room 105, Instructional Center
Organizers:
Johan G. F. Belinfante, Georgia Institute of Technology belinfan@math.gatech.edu

10:10 a.m.
Mathematics in the TPTP Problem Library.
Geoff Sutcliffe*, University of Miami
(9756896) 
10:40 a.m.
A Framework for Verification of Software Specifications.
Olga Shumsky Matlin, Argonne National Laboratory
Lawrence J Henschen*, Northwestern University
(97568110) 
11:10 a.m.
Semantics and Heuristics in OSHL.
Swaha Das*, UNC Chapel Hill
Shelby Funk, UNC Chapel Hill
David A. Plaisted, UNC Chapel Hill
(9756894) 
11:40 a.m.
The Nature of Monotonicity in HigherOrder ContextOriented Mathematical Logic.
Damon A. Scott*, Francis Marion University
(97503128) 
12:00 p.m.
Discussion

10:10 a.m.