Dec 11: U.Egly, Translation to Normal Form

Thread View: comp.theory

1 messages

[T] Back to Threads [V] Tree View [G] Group Articles

1 total messages Started by Helmut Veith Wed, 06 Dec 1995 00:00

#2134

Author: Helmut Veith
Date: Wed, 06 Dec 1995 00:00

68 lines
3584 bytes



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

Uwe Egly
============
Institut fuer Informationssysteme, TU Wien
mailto:uwe@kr.tuwien.ac.at


On Different Structure-Preserving Translations to Normal Form    
--------------------------------------------------------------
Monday, December 11, 1995, 16:45



ABSTRACT:

Translations to clause form are required for many automated theorem
provers. Besides the common translation which is based on
distributivity laws, there are approaches introducing labels as
abbreviations for subformulae. The latter translations are called
definitional (or structure-preserving) because they introduce
definitions for subformulae and preserve the structure of the formula.
An obvious optimization is to use implications instead of equivalences
in the definitions, if the subformula occurs in one polarity only, in
order to reduce the length of the resulting clause form.

We compare the optimized transformation with the unoptimized one with
respect to the Herbrand complexity of the resulting clause forms.  We
show that the optimization has a severe drawback. We identify a
sequence of formulae H1, H2,..., for which the optimized translation
yields a clause form of Hk with Herbrand complexity non-elementary in
k.  In contrast, the unoptimized translation results in a clause form
with Herbrand complexity exponential in k. Hence, the optimization
results in a non-elementary decrease of proof length if, for instance,
resolution or a cut-free sequent calculus is applied.

Finally, we demonstrate that definitional translations to clause form
have some practical value. We show that there are many theorems for
which a definitional translation is required in order to find a proof
with an automated theorem prover. (This last part is joined work with
Thomas Rath, TH Darmstadt.)



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: mailto:kgs@logic.tuwien.ac.at
http://logic.tuwien.ac.at:80/kgs/home.html 
listserver: mailto:listproc@dbai.tuwien.ac.at

Mit Unterstuetzung des
Bundesministeriums fuer Wissenschaft und Forschung

Thread Navigation

This is a paginated view of messages in the thread with full content displayed inline.

Messages are displayed in chronological order, with the original post highlighted in green.

Use pagination controls to navigate through all messages in large threads.

Back to All Threads