Deductive synthesis of the unification algorithm
From MaRDI portal
Publication:1157924
DOI10.1016/0167-6423(81)90004-6zbMath0472.68054OpenAlexW4210732998MaRDI QIDQ1157924
Richard Waldinger, Zohar Manna
Publication date: 1981
Published in: Science of Computer Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0167-6423(81)90004-6
correctnessderivation of a program from a given specificationformal program construction methodtheorem-proving task
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (8)
Constructing recursion operators in intuitionistic type theory ⋮ Unification: A case-study in data refinement ⋮ Set theory for verification. II: Induction and recursion ⋮ Formalization of the resolution calculus for first-order logic ⋮ Structure sharing for quantified terms: Fundamentals ⋮ Partial and nested recursive function definitions in higher-order logic ⋮ A higher-order interpretation of deductive tableau ⋮ A strong restriction of the inductive completion procedure
This page was built for publication: Deductive synthesis of the unification algorithm
