AMS Sectional Meeting Program by Special Session

Current as of Tuesday, April 12, 2005 15:10:41

Associate secretaries:
John L Bryant, AMS bryant@math.fsu.edu

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
  (975-68-85)
- 2:40 p.m.
  The Method of Proof Sketches.
  Robert L Veroff*, University of New Mexico
  (975-68-95)
- 3:10 p.m.
  A Spectrum of Applications of Automated Reasoning.
  Larry Wos*, Argonne National Laboratory
  (975-03-84)
- 3:40 p.m.
  Extending Decision Procedures with Induction Schemes.
  Deepak Kapur*, University of New Mexico
  (975-68-97)
- 4:10 p.m.
  A logical framework for computer-verified proofs in undergraduate mathematics.
  Richard Sommer*, Stanford University
  (975-03-133)
- 4:40 p.m.
  The Comprehension Schema in Tableaux: Toward Wos' Eighth Research Problem.
  Benjamin Price Shults*, Western Carolina University
  (975-03-91)
- 5:10 p.m.
  Automated Reasoning about the Zermelo-von Neumann Cumulative Hierarchy.
  Johan G. F. Belinfante*, Georgia Inst. Technology
  (975-03-83)

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
  (975-68-226)
- 10:45 a.m.
  A modularization mechanism for interactive proof-development.
  Eugenio G. Omodeo*, Universita` di L'Aquila, Dipartimento di Informatica
  Jacob T. Schwartz, New York University, Dept. of Computer Science
  (975-03-104)
- 11:15 a.m.
  Automated validation of three-variable formulations of set-pairing.
  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
  (975-03-102)
- 11:45 a.m.
  Translation of Resolution Proofs into Higher Order Natural Deduction.
  Hans de Nivelle*, Max Planck Institut
  (975-03-135)
- 12:15 p.m.
  Discussion

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
  (975-03-109)
- 3:35 p.m.
  Interpreting set theory in the variable-free, equational calculus of relations.
  Steven R Givant*, Mills College
  (975-03-90)
- 4:05 p.m.
  Finite Model Search and Single Axioms.
  William McCune*, Argonne National Laboratory
  (975-03-93)
- 4:35 p.m.
  Proving theorems automatically and interactively with TPS.
  Peter B. Andrews*, Carnegie Mellon University
  (975-03-86)
- 5:05 p.m.
  Specifying Tournament Schedules for General Model Generators.
  Hantao Zhang*, University of Iowa
  (975-68-111)

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
  (975-68-96)
- 10:40 a.m.
  A Framework for Verification of Software Specifications.
  Olga Shumsky Matlin, Argonne National Laboratory
  Lawrence J Henschen*, Northwestern University
  (975-68-110)
- 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
  (975-68-94)
- 11:40 a.m.
  The Nature of Monotonicity in Higher-Order Context-Oriented Mathematical Logic.
  Damon A. Scott*, Francis Marion University
  (975-03-128)
- 12:00 p.m.
  Discussion

Inquiries: meet@ams.org