Delivery-Date: 
Date: Thu, 20 Jan 94 09:26:50 CST
From: Matt Kaufmann <kaufmann@CLI.COM>
Message-Id: <9401201526.AA02090@thunder.CLI.COM>
To: theorem-provers@mc.lcs.mit.edu, qed@mcs.anl.gov, mind@aisb.ed.ac.uk, 
    indus@herky.cs.uiowa.edu, nqthm-users@CLI.COM, info-hol@cs.uidaho.edu, 
    isabelle-users@cl.cam.ac.uk, dreamers@aisb.ed.ac.uk, risks@csl.sri.com, 
    cade-12@aisb.ed.ac.uk, basin@mpi-sb.mpg.de, fausto@irst.it, 
    kaufmann@CLI.COM
Subject: workshop announcement
Sender: qed-owner@mcs.anl.gov

		       CALL FOR WORKSHOP PARTICIPATION:
				       
		  Correctness and Metatheoretic Extensibility
			of Automated Reasoning Systems
				       
			June 26, 1994 (see Note at end)
				 Nancy, France
				       
			   Held in conjunction with
				    CADE-12
	   (Twelfth International Conference on Automated Deduction)
				 Nancy, France

Please post/circulate.

This one-day workshop will center around three related themes: 

1) How can we guarantee that the formulas proved by theorem provers
   are actually theorems?
2) How can provers themselves be verified or built in some correct
   way?
3) How can theorem provers be soundly extended with new inference
   rules and procedures?
 
These themes are motivated by problems in applying computers to
machine checked mathematics, for example, formal proofs of program
correctness.  They are central issues in many applications, in
particular in constructing software and hardware which provably meet
formal specifications.

The first two themes will address the question of how we can trust the
system we are using and how we can apply formal methods to the
construction of such systems.  This is an important and difficult
question as modern theorem provers (e.g., Never, Nqthm, Nuprl, HOL)
are quite complex, but yet must be more or less trusted if we are to
trust the correctness of proofs built with them.  Little work has been
done in this area to date.  The problem area encompasses for example,
ways we can verify a system within itself, or bootstrapping complex
verified provers from simpler already trusted ones.  It also
encompasses the problem of building simple trusted proof-checkers.

The third theme is significant as it is desirable to extend provers
with the kinds of rules and procedures that humans have found
effective in constructing proofs.  Hence, some framework for
metatheoretic extensibility is desirable.  The primary traditional
solution to this problem is tactics, but they can be inflexible as
they must construct a justification using primitive inference rules.
Other approaches are the meta-functions of Boyer and Moore and the
work at Cornell (e.g., Constable, Howe, and others) in meta-theoretic
extensibility.

The structure of the workshop will be to alternate presentation of
current and past approaches to these questions with discussion and
comparison.  Of particular interest is work, both existing and
proposed, that has potential for realization in an implementation.

Potential participants should apply by submitting a short statement
that contains both an abstract of their work in this area that they
wish to present, if any, and a short description of their current
interests.  This should be sent by email to David Basin,
basin@mpi-sb.mpg.de, before February 27th.  Include also your address,
email address, phone, and fax information.  Participant notification
will be sent out no later than April.  If there is sufficient
interest, an informal workshop proceedings may appear afterwards, in
which case participants will have a chance to revise their statements
for the proceedings.

Organizers: 
   David Basin,          MPI Saarbruecken, basin@mpi-sb.mpg.de
   Fausto Giunchiglia,   IRST and University of Trento, fausto@irst.it
   Matt Kaufmann,        Computational Logic, Inc., kaufmann@cli.com

Note:  The CADE-12 workshop schedule is tentative at this point,
although unlikely to change.  If the date were to change, it would be
1 day later (June 27, 1994).  A final announcement will be sent when
the date is finalized.