Conference Paper June 22, 2021
What, Again? Automatic Deductive Synthesis of the Unification AlgorithmSRI Authors Richard J. Waldinger
Richard J. Waldinger; Conference: UNIF 2021: 35th International Workshop on Unification; Buenos Aires, Argentina; ResearchGate.net.
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.