Deductive synthesis of the unification algorithm
- 31 October 1981
- journal article
- Published by Elsevier in Science of Computer Programming
- Vol. 1 (1-2) , 5-48
- https://doi.org/10.1016/0167-6423(81)90004-6
Abstract
No abstract availableKeywords
This publication has 11 references indexed in Scilit:
- Algorithm classification through synthesisThe Computer Journal, 1980
- A Deductive Approach to Program SynthesisACM Transactions on Programming Languages and Systems, 1980
- Linear unificationJournal of Computer and System Sciences, 1978
- Non-resolution theorem provingArtificial Intelligence, 1977
- Knowledge and reasoning in program synthesisArtificial Intelligence, 1975
- A unification algorithm for typed -calculusTheoretical Computer Science, 1975
- Proving Theorems about LISP FunctionsJournal of the ACM, 1975
- Reasoning about programsArtificial Intelligence, 1974
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965
- An improved proof procedure1Theoria, 1960