🚀 go-pugleaf

Lecture Series ``Collegium Logicum''
Kurt Goedel Society
University of Technology, Vienna, Austria


Lecture Announcement
--------------------

Christian Fermueller
============================
Technische Universitaet Wien

Nonelementary Speedups in Tableaux
-------------------------------------------------------------
Monday, May 29, 1995, 16:45


ABSTRACT:

Tableau based proof procedures are studied since
the 1950s; but major computational improvements upon the basic calculus
of Beth and Hintikka have only recently been described in [3]
and [1]. Although examples of exponential
speedups were presented in these papers no hint is given
about the real nature of the difference in proof complexity
between these versions of tableau calculi. It also remained
open whether further ``liberalizations of the delta-rule'' 
with significant effects on proof complexity are possible. 

We address the first problem by showing that the version
of tableaux introduced in [1] (which is an improvement
over the one in [3]) admits a nonelementary speedup
in tableau size over the standard version of tableaux as, e.g.,
described in [2]. 

More importantly, we also give an answer to the second question by
introducing a new, computationally simple variant of the strong 
quantifier elimination rule (delta-rule)
that may lead to a nonelementary decrease of tableau-size even w.r.t. the improvements of tableaux mentioned above.


[1] B.Beckert, R.Haehnle and P.Schmitt:
         The even more liberalized delta-rule in free variable
         semantic tableaux. In: Computational Logic and
         Proof Theory, Prooceedings of the 3rd Kurt Goedel Colloquium, Brno,
         August 1993. Springer, LNCS 713, pp.108-119.
[2] M.Fitting:
         First-Order Logic and Automated Theorem Proving.
         Springer, New York, 1990.

[3] R.Haehnle and P.Schmitt:
         The liberalized delta-rule in free variable
         semantic tableaux. Journal of Automated Reasoning, to appear.


PLACE:

Seminarraum SEM 181A, Institut fuer Informationssysteme,
Paniglgasse 16, 1. Stock, 1040 Wien.

------------------------
Kurt-Goedel-Gesellschaft
Technische Universitaet Wien
Institut fuer Computersprachen E185.2
Resselgasse 3/1, A-1040 Wien

Tel: (+43 1) 588 01/4088
Fax: (+43 1) 504 15 89
email: kgs@logic.tuwien.ac.at
http://logic.tuwien.ac.at:80/kgs/home.html 

Mit Unterstuetzung des
Bundesministeriums fuer Wissenschaft und Forschung