Campus Event Calendar
Event Entry
What and Who
Minimal Binary Resolution Trees
Prof. E. Bruce Spencer
Faculty of Computer Science, Fredericton, New Brunswick, Canada
DFKI-Kolloquium
AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, RG1, SWS
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 15 October 96
14:00
60 Minutes
43.1 - DFKI
1.01
Saarbrücken
Abstract
Robinson's binary resolution, often presented in terms of binary trees,
may be restricted to be regular: no atom is resolved upon twice in any
branch. In this work we consider reordering two consecutive resolution
steps, inducing an AVL rotation on the tree, which may expose a new
irregularity. Without sacrificing completeness, we strengthen the
restriction by enforcing regularity after (all sequences of) rotations.
Such a tree is said to be minimal, and the smallest proof tree must be
minimal. Although the number of re-orderings may be intractable, an
efficient algorithm is given to determine minimality. Experiments show
that the theorem prover OTTER spends much effort building non-minimal
trees, and that restricting it to minimal trees sometimes improves
performance.
may be restricted to be regular: no atom is resolved upon twice in any
branch. In this work we consider reordering two consecutive resolution
steps, inducing an AVL rotation on the tree, which may expose a new
irregularity. Without sacrificing completeness, we strengthen the
restriction by enforcing regularity after (all sequences of) rotations.
Such a tree is said to be minimal, and the smallest proof tree must be
minimal. Although the number of re-orderings may be intractable, an
efficient algorithm is given to determine minimality. Experiments show
that the theorem prover OTTER spends much effort building non-minimal
trees, and that restricting it to minimal trees sometimes improves
performance.
Contact
Dr. Dieter Hutter / Sekretariat Prof. J. Siekmann
Tel.: (++49) 681 302 5276
--email hidden
passcode not visible
logged in users only