-------------------------------------------------------------------------------
				       
				       
		       B O S T O N   U N I V E R S I T Y
				       
			  Computer Science Department
				       
			      C O L L O Q U I U M
				       
			  Wednesday December 8, 1993
				       
				    3:00pm
			    (Tea served at 2:30pm)
				       
			    Seminar Room / MCS 135
				       

------------------------------------------------------------------------------
				       
				       
	     IMPS: A Human-Oriented Mathematical Reasoning System
				       
			       William M. Farmer
				       
			     The MITRE Corporation
				  Bedford, MA
				       
				       
       IMPS is an  Interactive  Mathematical Proof System developed   by
       W. M. Farmer, J. D.  Guttman, and F. J.  Thayer and now available
       to the public without fee (under  a public license) via anonymous
       ftp  at math.harvard.edu.   It   is a  computer   environment for
       practicing  rigorous   mathematics using  traditional techniques.
       Its primary objective is to reinforce and  improve human modes of
       mathematical    reasoning,      not   to    perform    automated,
       human-independent deductions.  The  paramount importance given to
       supporting human reasoning sets IMPS apart from most contemporary
       mathematical reasoning systems.  The system consists of a library
       of axiomatic theories  (linked by  theory interpretations) and  a
       collection   of tools for   exploring,  applying, extending,  and
       communicating the  mathematics   stored in  the  theory  library.
       Currently, the theory  library  contains significant portions  of
       logic, algebra, and  analysis  with over 1100  replayable proofs.
				       
       The talk will have two parts.  The first will be a brief overview
       of the system emphasizing the human-oriented nature of IMPS.  The
       second   will  discuss   potential  applications    of  IMPS   in
       mathematics,    formal   methods,    symbolic    computation, and
       education.  A demonstration of IMPS will follow the talk.
				       
       Host: Professor Wayne Snyder

-------------------------------------------------------------------------------
    For more information contact Prof. Azer Bestavros <bestavros@cs.bu.edu>
-------------------------------------------------------------------------------