Editing Unification (computer science) (section)

== Further reading ==
* [[Franz Baader]] and [[Wayne Snyder]] (2001). [https://scholar.archive.org/work/lgc4iib23zgjvflvqw3bpuyprq "Unification Theory"]. In [[John Alan Robinson]] and [[Andrei Voronkov]], editors, ''[[Handbook of Automated Reasoning]]'', volume I, pages 447–533. Elsevier Science Publishers.
* [[Gilles Dowek]] (2001). [http://www.lsv.fr/~dowek/Publi/unification.ps "Higher-order Unification and Matching"] {{Webarchive|url=https://web.archive.org/web/20190515113555/http://www.lsv.fr/~dowek/Publi/unification.ps |date=2019-05-15 }}. In ''Handbook of Automated Reasoning''.
* Franz Baader and [[Tobias Nipkow]] (1998). [http://www.in.tum.de/~nipkow/TRaAT/ ''Term Rewriting and All That'']. Cambridge University Press.
* Franz Baader and {{ill|Jörg H. Siekmann|de}} (1993). "Unification Theory". In ''Handbook of Logic in Artificial Intelligence and Logic Programming''.
* Jean-Pierre Jouannaud and [[Claude Kirchner (computer scientist)|Claude Kirchner]] (1991). "Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification". In ''Computational Logic: Essays in Honor of Alan Robinson''.
* [[Nachum Dershowitz]] and [[Jean-Pierre Jouannaud]], ''Rewrite Systems'', in: [[Jan van Leeuwen]] (ed.), ''[[Handbook of Theoretical Computer Science]]'', volume B ''Formal Models and Semantics'', Elsevier, 1990, pp.&nbsp;243–320
* Jörg H. Siekmann (1990). "Unification Theory". In [[Claude Kirchner (computer scientist)|Claude Kirchner]] (editor) ''Unification''. Academic Press.
* {{cite journal| author=Kevin Knight| title=Unification: A Multidisciplinary Survey| journal=ACM Computing Surveys|date=Mar 1989| volume=21| number=1| pages=93–124| url=http://www.isi.edu/natural-language/people/unification-knight.pdf| doi=10.1145/62029.62030| citeseerx=10.1.1.64.8967| s2cid=14619034}}
* [[Gérard Huet]] and [[Derek C. Oppen]] (1980). [http://infolab.stanford.edu/pub/cstr/reports/cs/tr/80/785/CS-TR-80-785.pdf "Equations and Rewrite Rules: A Survey"]. Technical report. Stanford University.
* {{cite journal | last1 = Raulefs | first1 = Peter | last2 = Siekmann | first2 = Jörg | last3 = Szabó | first3 = P. | last4 = Unvericht | first4 = E. | year = 1979 | title = A short survey on the state of the art in matching and unification problems | journal = ACM SIGSAM Bulletin | volume = 13 | issue = 2 | pages = 14–20 | doi = 10.1145/1089208.1089210 | s2cid = 17033087 }}
* Claude Kirchner and Hélène Kirchner. ''Rewriting, Solving, Proving''. In preparation.

[[Category:Unification (computer science)| ]]
[[Category:Automated theorem proving]]
[[Category:Logic programming]]
[[Category:Rewriting systems]]
[[Category:Logic in computer science]]
[[Category:Type theory]]