American Mathematical Society

My Account · My Cart · Customer Services · FAQ  

AMS Sectional Meeting Program by Special Session

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


Program  |  Deadlines  |  Registration/Housing/Etc.  |  Inquiries:  meet@ams.org

2002 AMS and MAA Spring Southeastern Section Meetings
Atlanta, GA, March 8-10, 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
      (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