Conference Paper June 22, 2021

What, Again? Automatic Deductive Synthesis of the Unification Algorithm

SRI Authors Richard J. Waldinger

Citation

COPY

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

Abstract

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?

Area of interest

Country

First name

Last name

Company name

Your email address

Your message

Select all that apply(optional)Discovery ServicesPreclinical/Early Clinical Development ServicesPartnership/CollaborationsBasic Research

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