Description

Comparing Unification Algorithms in First-Order Theorem Proving Kryštof Hoder, Andrei Voronkov University of Manchester Saturation-based Theorem Provers Try to find a contradiction by generating new clauses

Information

Category:
## Math & Engineering

Publish on:

Views: 10 | Pages: 18

Extension: PDF | Download: 0

Share

Transcript

Comparing Unification Algorithms in First-Order Theorem Proving Kryštof Hoder, Andrei Voronkov University of Manchester Saturation-based Theorem Provers Try to find a contradiction by generating new clauses according to a set of rules Binary resolution: A \/ C B \/ D (C \/ Dσ Need to retrieve all atoms/terms that are unifiable with a query atom/term Often 10 5 or more candidates σ is mgu of A and B Too much to try one by one, indexing structures are used We compared the performance of several unification algorithms inside an indexing structure Unification Algorithms For terms s and t, the algorithm either gives a most general unifier σ (then sσ=tσ, or it fails Robinson algorithm (1965, simple, exponential Martelli-Montanari algorithm (1982, almost linear Escalada-Ghallab (1988, almost linear, efficient Paterson-Wegman (1976, inefficient, linear Occurs Check Cycle detection Avoids situations such as {x - f(y, y- x}* Expensive, in Prolog usually omitted Inline occurs check (Robinson algorithm The cycle detection is done immediately when a variable is bound Only the relevant part is traversed Post occurs check (MM, EG The cycle detection is performed on the whole substitution after the binding part is over PROB The Robinson algorithm's exponential behaviour is rare p(x 0, f(x 0,x 0, x 1,... p(f(y 0,y 0, y 1, f(y 1,y 1,... The triangle form of the substitution is polynomial {x 0 - f(y 0,y 0, y 1 - f(x 0,x 0, x 1 - f(y 1,y 1,...}* (the non-triangle form is {x 0 - f(y 0,y 0, y 1 - f(f(y 0,y 0,f(y 0,y 0,...} Without the repeated work during the occurs check and unifying already unified terms, the algorithm runs in polynomial time Indexing Structures Their key role is in simplifying rules Keeping the collection of clauses small Just matching, not unification Some more suitable for the perfect unifier retrieval Substitution trees (new Vampire, old Fiesta, Spass Context trees (new Fiesta Some are less Discrimination trees (Waldmeister Path Indexing A substitution in each node Substitution Trees Regular: (1 f(x 1,x 1 (2 f(x 1,x 2 (3 f(a,g(d (4 f(g(d,g(x 1 Indexed terms * 0 σ in the leafs σ is a composition of substitutions on path from the root to the leaf Downward subst. trees Downward: A newly inserted term has a deterministic position Unification in Substitution Trees Only a simple interface between a substitution tree and a substitution object is necessary trytoextendtounify(queryterm, indexterm:bool undolastunification( getboundtopsymbol(variable:fnsymbol? not necessary, just allows for an optimization in downward substitution trees Retrieval from Substitution Trees Retrieval of terms unifiable with f(f(a,y 1,y 1 (1 f(x 1,x 1 (2 f(x 1,x 2 (3 f(a,g(d (4 f(g(d,g(x 1 σ: * 0 =f(f(a,y 1,y 1 Checked by inline occurs check Retrieval from Substitution Trees Retrieval of terms unifiable with f(f(a,y 1,y 1 (1 f(x 1,x 1 (2 f(x 1,x 2 (3 f(a,g(d (4 f(g(d,g(x 1 σ: * 0 =f(f(a,y 1,y 1 * 1 =y 1 * 2 =f(a,y 1 Checked by inline occurs check Retrieval from Substitution Trees Retrieval of terms unifiable with f(f(a,y 1,y 1 (1 f(x 1,x 1 (2 f(x 1,x 2 (3 f(a,g(d (4 f(g(d,g(x 1 σ: * 0 =f(f(a,y 1,y 1 * 1 =y 1 * 2 =f(a,y 1 x 1 =f(a,y 1 Checked by inline occurs check Retrieval from Substitution Trees Retrieval of terms unifiable with f(f(a,y 1,y 1 (1 f(x 1,x 1 (2 f(x 1,x 2 (3 f(a,g(d (4 f(g(d,g(x 1 σ: * 0 =f(f(a,y 1,y 1 * 1 =y 1 * 2 =f(a,y 1 x 1 =f(a,y 1 y 1 =x 1 occurs check failure Checked by inline occurs check Retrieval from Substitution Trees Retrieval of terms unifiable with f(f(a,y 1,y 1 (1 f(x 1,x 1 (2 f(x 1,x 2 (3 f(a,g(d (4 f(g(d,g(x 1 σ: * 0 =f(f(a,y 1,y 1 * 1 =y 1 * 2 =f(a,y 1 x 1 =f(a,y 1 x 2 =y 1 success Checked by inline occurs check Retrieval from Substitution Trees Retrieval of terms unifiable with f(f(a,y 1,y 1 (1 f(x 1,x 1 (2 f(x 1,x 2 (3 f(a,g(d (4 f(g(d,g(x 1 σ: * 0 =f(f(a,y 1,y 1 * 1 =y 1 * 2 =f(a,y 1 * 2 =a mismatch In downward subst. trees we can skip the node based on top symbols of the *2 bindings Retrieval from Substitution Trees Retrieval of terms unifiable with f(f(a,y 1,y 1 (1 f(x 1,x 1 (2 f(x 1,x 2 (3 f(a,g(d (4 f(g(d,g(x 1 σ: * 0 =f(f(a,y 1,y 1 * 1 =y 1 * 2 =f(a,y 1 * 2 =g(d mismatch In downward subst. trees we can skip the node based on top symbols of the *2 bindings Our Experiments We created benchmarks from several prover runs Operations on the unification index recorded (insertions, deletions, queries 765 benchmarks (about a half from the resolution index and a half from the backward superposition index ROB, MM, EG and PROB unification algorithms implemented with the required interface The index operations performed on each variant of the substitution trees and the time measured Algorithm Results Rel. time (resolution index Rel. time (superposition index ROB MM EG PROB The inline occurs check algorithms appear to be more suitable for the substitution trees Lots of unification requests on a single substitution Inline o. c. check just the relevant part of a big substitution Post o. c. have to be performed after each unification request, not just once per the result substitution Questions...

Related Search

Similar documents

We Need Your Support

Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks