back icon
close icon

Capture phrases in quotes for more specific queries (e.g. "rocket ship" or "Fred Lynn")

Conference Paper  June 22, 2021

What, Again? Automatic Deductive Synthesis of the Unification Algorithm

SRI Authors Richard J. Waldinger



Richard J. Waldinger; Conference: UNIF 2021: 35th International Workshop on Unification; Buenos Aires, Argentina;


We describe work in progress towards deriving a unification algorithm automatically from a declarative specification using deductive methods. The specification is phrased as a logical theorem and the program is extracted from the proof. The theorem is proved using Stickel’s system SNARK, operating over a theory of expressions and substitutions. The theory has been formulated to allow a simpler specification of the algorithm, and the theorem prover has discovered novelties in the implementation. It is hoped that the same techniques may enable the discovery of previously unknown unification algorithms for specific theories. 

How can we help?

Once you hit send…

We’ll match your inquiry to the person who can best help you. Expect a response within 48 hours.

Our Privacy Policy