情報処理学会 第74回全国大会講演要旨

A term rewriting system, which is frequently used in the field of theorem proving, is a set of rewrite rules that transform a term to another. Proving termination of term rewriting system is becoming an active research area for recent years. Many research have been done on the traditional method for automated termination proofs of term rewriting system to improve it. The power of these methods has been significantly extended by the dependency pair method based on the work of Arts and Giesl . However, its efficiency is still one of the obstacles to further improvement of proving termination. In this paper we propose some parallel methods to accelerate the dependency pair method by using multi-core CPU. Meanwhile we present useful methods to solve the synchronization problem occurred in the parallelization. We evaluate the proposed methods with the experiment, and discuss the future work.