goals and the base logic

Zdzislaw Meglicki <Zdzislaw.Meglicki@arp.anu.edu.au>

Mail folder: QED
Next message: Pat Lincoln: "the base logic"
Previous message: Phil Windley: "Re: a multilingual approach "

Message-id: <sfmpFSeKmlE24qgaoA@arp>
Date: Wed, 14 Apr 1993 10:01:34 +1000 (EST)
From: Zdzislaw Meglicki <Zdzislaw.Meglicki@arp.anu.edu.au>
To: qed@mcs.anl.gov
Subject: goals and the base logic
Sender: qed-owner
Precedence: bulk

Bill McCune writes:

> I hope that there will be many implementations associated with QED,
> with different types of knowledge bases, different user interfaces,
> and written in different programming languages.  Of course there will
> have to be (at some level) a common language for formulas, proofs, etc.,
> but that seems like a small issue once the base logic is fixed.

> It seems to me that the fundamental issues are the goals of the project
> and the base logic.

The impression I got from reading the "Manifesto" was that the goal of
the QED would be to undertake a Bourbaki like project using computer
reasoning as its basis. If that is the case then, I would expect, some
kind of a uniform approach both with respect to the tools and basic
logic should emerge. The beauty of Bourbaki is that such a unified
approach as to the basic logic (set theory) and methodology was agreed
upon and used methodically by all participants of the project. This
resulted in quite a monumental work which had a great impact on XXth
century mathematics. Would anything less than that be worth doing?

Although I may be quite mistaken here, I think that unless real
mathematicians are attracted to QED and begin to use it for their normal
work, the project will be doomed. Hence the need to come up with user
environments, basic logic, and programming language which would be
acceptable to that end user, i.e., the mathematician. Likewise, the need
to develop a unified approach. To have a collage of various systems,
various logics, various languages would hardly be any different from
what we already have today. Why call it QED?

   Zdzislaw Gustav Meglicki, gustav@arp.anu.edu.au,
   Automated Reasoning Program - CISR, and Plasma Theory Group - RSPhysS,
   The Australian National University, G.P.O. Box 4, Canberra, A.C.T., 2601, 
   Australia, fax: (Australia)-6-249-0747, tel: (Australia)-6-249-0158