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)