Ground confluence prover based on rewriting induction

Takahito Aoto, Yoshihito Toyama

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Citations (Scopus)

Abstract

Ground confluence of term rewriting systems guarantees that all ground terms are confluent. Recently, interests in proving confluence of term rewriting systems automatically has grown, and confluence provers have been developed. But they mainly focus on confluence and not ground confluence. In fact, little interest has been paid to developing tools for proving ground confluence automatically. We report an implementation of a ground confluence prover based on rewriting induction, which is a method originally developed for proving inductive theorems.

Original languageEnglish
Title of host publication1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016
EditorsDelia Kesner, Brigitte Pientka
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959770101
DOIs
Publication statusPublished - 2016 Jun 1
Event1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 - Porto, Portugal
Duration: 2016 Jun 222016 Jun 26

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume52
ISSN (Print)1868-8969

Other

Other1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016
CountryPortugal
CityPorto
Period16/6/2216/6/26

Keywords

  • Ground confluence
  • Non-orientable equations
  • Rewriting induction
  • Term rewriting systems

ASJC Scopus subject areas

  • Software

Cite this