A brief Introduction to First-Order Logic Unification at the example of Corbin and Bidoit's variation of Robinson's Unification Algorithm

Automated reasoning and deduction have interested computer scientists and logicians since the earliest days of modern information technology. One of the fundamental processes of this field is unification, meaning the automated solving of equations containing symbolic expressions. This paper revisits the 1965 Robinson Unification algorithm, which is now recognized as being the first machine-oriented unification algorithm for first-order logic. The primary criticism to be brought against this algorithm is its exponential space complexity. Corbin and Bidoit proposed a revised version of the algorithm that aims to address this problem in 1983, which is discussed here as well.

Originally published by LMU Munich, Master Seminar “Unification” SS21.

PDF

Links

• ResearchGate
• Internet Archive Scholar

Identifiers

• fatcat: release_b2graaepdfhn7ayluo45gholyu

BibTeX

Johannah Sprinz, 2021. A brief Introduction to First-Order Logic Unification at the example of Corbin and Bidoit's variation of Robinson's Unification Algorithm. Munich: LMU Munich, Master Seminar “Unification” SS21. https://www.cip.ifi.lmu.de/~sprinz/sprinz_2021_unification.pdf

@misc{e77bd99be3a083788f04d5fe54251f5d,
  author       = "Johannah Sprinz",
  title        = "A brief Introduction to First-Order Logic Unification at the example of Corbin and Bidoit's variation of Robinson's Unification Algorithm",
  year         = 2021,
  month        = "Sep",
  howpublished = "Munich, LMU Munich, Master Seminar “Unification” SS21",
  note         = "\url{https://www.cip.ifi.lmu.de/~sprinz/sprinz_2021_unification.pdf}, Accessed: October 29, 2022"
}