Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Minimal Binary Resolution Trees
Speaker:Prof. E. Bruce Spencer
coming from:Faculty of Computer Science, Fredericton, New Brunswick, Canada
Speakers Bio:
Event Type:DFKI-Kolloquium
Visibility:D1, D2, D3, INET, D4, D5, RG1, MMCI, SWS
We use this to send out email in the morning.
Level:AG Audience
Language:English
Date, Time and Location
Date:Tuesday, 15 October 96
Time:14:00
Duration:60 Minutes
Location:Saarbr├╝cken
Building:43.1 - DFKI
Room:1.01
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.
Contact
Name(s):Dr. Dieter Hutter / Sekretariat Prof. J. Siekmann
Phone:Tel.: (++49) 681 302 5276
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Note:
Attachments, File(s):