3.0/2.0 VU Unification Theory (185.289)

Given by: Gernot Salzer

Elective course (Wahllehrveranstaltung) in the master studies "Computational Intelligence" (066931) and "Software Engineering & Internet Computing" (066937), and in the international master program "Computational Logic (Erasmus-Mundus)" (066011).

The default language is German. However, if someone in the audience is not sufficiently fluent in German the course will be given in English.

News

• First meeting: Wednesday, 10.3.2010, 14:30-16:30, SEM 185/2 (1040 Wien, Favoritenstraße 9/staircase 1/4th floor(3.Stock)/yellow area/room HA0308).

• Course dates 2010: every Wednesday, 14:30-16:30
  March: SEM 185/2 (1040 Wien, Favoritenstraße 9/staircase 1/4th floor(3.Stock)/yellow area/room HA0308)
  April-June: Seminar room "Gödel" (Favoritenstraße 9/ground floor/courtyard)

• This course in TUWIS++

Contents

In many symbol-oriented systems like expert systems, automated theorem provers or logic-oriented programming languages (e.g. Prolog) the basic data structures are terms, and the basic operation on terms is unification. Unification tries to make terms equal by replacing variables; algebraically unification can be viewed as the process of solving term equations.

Topics:

• Unification in the free term algebra; efficient algorithms
• Unification in equational theories
• Particular equational theories: A, C, AC, AC1, Boolean rings
• Universial unification
• Combination of unification procedures
• Applications of unification: automated theorem proving, term rewriting, logic programming, linguistics.

Related courses: "Automatisches Beweisen" (Automated Theorem Proving) and "Termersetzungssysteme" (Term Rewriting)

Course dates

The course takes place every Wednesday, 14:30-16:30; the first meeting is on March 10, 2010. In March, we will meet in SEM 185/2 (1040 Wien, Favoritenstraße 9/staircase 1/4th floor(3.Stock)/yellow area/room HA0308); from April onwards we will meet in the seminar room "Gödel".

Please register for the course via TUWIS++, or if this fails, via email to salzer@logic.at.

Course material

The course is based on two introductory articles:

• F.Baader and W.Snyder. Unification theory. In: A.Robinson and A.Voronkov, eds., Handbook of Automated Reasoning, vol. 1, pp. 445-532. Elsevier Science, 2001.
• K.Knight. Unification: a multidisciplinary survey. In: ACM Computing Surveys 21(1), pp. 93-124. ACM Press, 1989.

Further material:

• More survey articles covering slightly different topics (but largely redundant, if you read the above two):
  • F.Baader and J.Siekmann. Unification theory. In: D.M.Gabbay, C.J.Hoffer, J.A.Robinson, and J.H.Siekmann, eds., Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 2, pp. 41-126. Oxford University Press, 1994.
  • F.Baader and K.Schulz. Unification theory – an introduction. In: W.Bibel and P.Schmitt, eds., Automated Deduction – a basis for application. Kluwer Academic Publishers, 1998.

• Origins of unification:
  • J.A.Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM 12 (1), pp. 23-41. ACM Press, 1965.
  • D.Knuth and P.Bendix. Simple word problems in universal algebras. In: J.Leech, ed., Computational Problems in Abstract Algebra, pp. 263-297, 1970.

• A-Unification:
  • G.S.Makanin. The problem of solvability of equations in a free semigroup. Math. USSR Sb. 32, pp. 129-198, 1977.
  • V.Diekert. Makanin's Algorithm. In: M.Lothaire, ed., Algebraic Combinatorics on Words, Chapter 12, pp. 387-442. Cambridge University Press, 2002.

• Unification in Boolean Rings

• Applications:
  • P.Deransart, A.Ed-Dbali,L.Cervoni. Prolog Unification. In: Prolog: The Standard (Reference Manual), pp. 11-17. Springer, 1996.