Delivery-Date: 
Date: Thu, 27 Apr 1995 12:52 -0700 (PDT)
From: ma_friesel@gate.pnl.gov
Subject: Re: QED Workshop.
To: qed@mcs.anl.gov, JanFriso.Groote@phil.ruu.nl
Cc: jfg@phil.ruu.nl
Message-id: <01HPU1JCKIXE00004Y@pnl.gov>
MIME-version: 1.0
Content-transfer-encoding: 7BIT
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

For that matter, have the characteristics of the optimal achievable proof 
search technique been identified?  Some techniques may be better for some 
categories of formulation than for others


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)