Abstract of FKI-186-93

Document-Name:  fki-186-93.ps.gz
Title:          Anwendung des Theorembeweisers SETHEO auf angeordnete Körper
Authors:        Joachim Draeger 
Revision-Date:  1993/10/28
Category:       Technical Report (Forschungsberichte Künstliche Intelligenz)
Abstract:       An application of the theorem prover SETHEO to problems
                in the domain of fields and ordered fields is presented using
                different axiomatizations with and without equality.
                The results show that the introduction of an explicite equality                 offers several advantages with respect to difficult problems. 
                New methods for the treatment of the partial multiplicative
                inversion function (expressions containing inv(0) must be
                excluded) as well as a mechanism for reducing the size of the 
                proof tree in the equational approach are given. The paper 
                closes with a discussion of possible other improvements of
                the axiomatization and of the proof procedure.
Keywords:       theorem prover, SETHEO, field, ordered field, order relation
                partial funktion, equality,
                relational axiom system, equational axiom system,
                consistency check, lateral branch control,
                proof tree reduction, term construction, term processing
Size:           121 pages
Language:       German
ISSN:           0941-6358
Copyright:      The ``Forschungsberichte Künstliche Intelligenz''
                series includes primarily preliminary publications,
                specialized partial results, and supplementary
                material. In the interest of a subsequent final
                publication these reports should not be copied. All
                rights and the responsability for the contents of the
                report are with the authors, which would appreciate
                critical comments.

Gerhard Weiss