Delivery-Date: 
From: Jan Friso Groote <JanFriso.Groote@phil.ruu.nl>
Message-Id: <199504271610.SAA08809@hardy.staf.phil.ruu.nl>
Subject: QED Workshop.
To: qed@mcs.anl.gov
Date: Thu, 27 Apr 1995 18:10:11 +0200 (MET DST)
Cc: jfg@phil.ruu.nl (Jan Friso Groote)
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Length: 2048
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

>I believe that persons that can not (or do not want to)
>attend the QED Workshop could suggest us interesting
>(and important for QED) topics.

I feel that in the area of automated reasoning there is one
very important question that has not seriously been addressed, as
far as I know, even on the level of classical propositional logic:

WHAT IS THE COMPARABLE DIFFERENCE OF DIFFERENT PROOF SEARCH TECHNIQUES.

Formulated in a more concrete way, which is the best system
(from a theoretical perspective !) to use to prove a propositional
formula a tautology. This is not straightforward, as we are
dealing with an NP complete problem. An interesting tool are
polynomial simulations between the lengths of proof searches of
different systems. As far as I know this has only been investigated
for lengths of proofs with Frege systems as an absolute winner.
A remarkable result of this kind
is due to d'Agostino who proves that truth tables
and Beth's tableaux are polynomially incomparable and that a
sligh change of the tableau system makes it substantially better.

I find this issue of extreme importance and would be glad to
hear any outcome of a discussion, but also pointers to literature that
I did overlook on this question.

With friendly greetings,
Jan Friso Groote


---------------------------------------------------------------
My addresses are:

Jan Friso Groote                    Visitors address:
Department of Philosophy            Heidelberglaan 8
Utrecht University                  3584 CS  Utrecht
P.O.Box 80126                       The Netherlands
3508 TC  Utrecht
The Netherlands                     Tel. +31-30-532761 (office)
                                         +31-30-531831 (secretary)
                                    Fax. +31-30-532816

Home address:                       E-mail JanFriso.Groote@phil.ruu.nl
Jan Friso Groote                        or jfg@phil.ruu.nl
Schoenerstraat 49                   (e-mail may be unreliable)
3534 RL  Utrecht
The Netherlands                     Tel. +31-30-431045 (home)