コンピュータサイエンス研究会

コンピュータサイエンス研究会

研究会名:コンピュータサイエンス研究会

開催日:平成20年8月4日(月)13:00~15:00

テーマ:Multi-Completion with Termination Tools

講師:Aart Middeldorp (University of Innsbruck)

開催場所:東北大学・電気通信研究所2号館4階 中会議室 (W401)


コンピュータサイエンス研究会 講演会の御案内

コンピュータサイエンス研究会
主査   小林  直樹

下記のようにコンピュータサイエンス研究会共催の講演会を開催いたしますので, ご案内申し上げます.

  • 日時:2008年8月4日(月)13:00~15:00
  • 場所:東北大学電気通信研究所2号館4階 中会議室 (W401)
  • 題目:Multi-Completion with Termination Tools
  • 話者:Aart Middeldorp (University of Innsbruck)
  • 概要:Knuth-Bendix completion is a well-known method for transforming equational theories into convergent rewrite systems. Traditional implementations of completion use a fixed reduction order to determine the orientation of rules. This restricts power and requires expertise of the user. In this talk we describe a new tool for performing completion with automatic termination tools. It is based on two ingredients: (1) the inference system for completion with multiple reduction orderings introduced by Kurihara and Kondo (1999) and (2) the inference system for completion with external termination provers proposed by Wehrman, Stump and Westbrook (2006) and implemented in the Slothrop system. Our tool can be used with any termination tool that satisfies certain minimal requirements. Preliminary experimental results show the potential of our tool.