Abstract of FKI-186-93
Title: Anwendung des Theorembeweisers SETHEO auf angeordnete Körper
Authors: Joachim Draeger
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
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