[logic-ml] Prof. Aart Middeldorp at NII Logic Seminar

[Makoto Tatsuta]

	      Prof. Aart Middeldorp at NII Logic Seminar


Date: September 22, 2014, 14:00--16:00

Place: National Institute of Informatics, Room 2005 (20th floor)
場所: 国立情報学研究所 20階 2005室
    (半蔵門線,都営地下鉄三田線・新宿線 神保町駅または東西線 竹橋駅より徒歩5分)
    (地図 http://www.nii.ac.jp/about/access/)

Speaker: Prof. Aart Middeldorp (University of Innsbruck)

Title: Proving AC Termination by Knuth-Bendix Orders

Abstract: 
Equational theories that contain axioms expressing associativity and
commutativity (AC) of certain operators are ubiquitous. Theorem proving
methods in such theories rely on well-founded orders that are compatible
with the AC axioms. In this talk we consider various definitions of
AC-compatible Knuth-Bendix orders. The orders of Steinbach and of Korovin
and Voronkov are revisited. The former is enhanced to a more powerful
AC-compatible order and we modify the latter to amend its lack of
monotonicity on non-ground terms. We present new complexity results and
compare the various orders on problems in termination and completion.
The talk is based on joint work with Nao Hirokawa, Sarah Winkler, and
Akihisa Yamada.

問合せ先:
龍田 真 (国立情報学研究所)
e-mail: tatsuta at nii.ac.jp
http://research.nii.ac.jp/~tatsuta