Ground confluence prover based on rewriting induction

Takahito Aoto; Yoshihito Toyama

doi:10.4230/LIPIcs.FSCD.2016.33

Ground confluence prover based on rewriting induction

Takahito Aoto, Yoshihito Toyama

Systems & Software Division

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016
Editors	Delia Kesner, Brigitte Pientka
Publisher	Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)	9783959770101
DOIs	https://doi.org/10.4230/LIPIcs.FSCD.2016.33
Publication status	Published - 2016 Jun 1
Event	1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 - Porto, Portugal Duration: 2016 Jun 22 → 2016 Jun 26

Publication series

Name	Leibniz International Proceedings in Informatics, LIPIcs
Volume	52
ISSN (Print)	1868-8969

Other

Other	1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016
Country	Portugal
City	Porto
Period	16/6/22 → 16/6/26

Keywords

Ground confluence
Non-orientable equations
Rewriting induction
Term rewriting systems

ASJC Scopus subject areas

Software

Access to Document

10.4230/LIPIcs.FSCD.2016.33

Cite this

Aoto, T., & Toyama, Y. (2016). Ground confluence prover based on rewriting induction. In D. Kesner, & B. Pientka (Eds.), 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 [33] (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 52). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.FSCD.2016.33

Ground confluence prover based on rewriting induction. / Aoto, Takahito; Toyama, Yoshihito.

1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016. ed. / Delia Kesner; Brigitte Pientka. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2016. 33 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 52).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Aoto, T & Toyama, Y 2016, Ground confluence prover based on rewriting induction. in D Kesner & B Pientka (eds), 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016., 33, Leibniz International Proceedings in Informatics, LIPIcs, vol. 52, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, Porto, Portugal, 16/6/22. https://doi.org/10.4230/LIPIcs.FSCD.2016.33

Aoto T, Toyama Y. Ground confluence prover based on rewriting induction. In Kesner D, Pientka B, editors, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2016. 33. (Leibniz International Proceedings in Informatics, LIPIcs). https://doi.org/10.4230/LIPIcs.FSCD.2016.33

@inproceedings{d603248d8a164858b3090a5918605474,

title = "Ground confluence prover based on rewriting induction",

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.",

keywords = "Ground confluence, Non-orientable equations, Rewriting induction, Term rewriting systems",

author = "Takahito Aoto and Yoshihito Toyama",

note = "Funding Information: Thanks are due to the anonymous reviewers for helpful comments. This work is partially supported by JSPS KAKENHI Nos. 15K00003, 25280025.; 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 ; Conference date: 22-06-2016 Through 26-06-2016",

year = "2016",

month = jun,

day = "1",

doi = "10.4230/LIPIcs.FSCD.2016.33",

language = "English",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",

editor = "Delia Kesner and Brigitte Pientka",

booktitle = "1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016",

}

TY - GEN

T1 - Ground confluence prover based on rewriting induction

AU - Aoto, Takahito

AU - Toyama, Yoshihito

N1 - Funding Information: Thanks are due to the anonymous reviewers for helpful comments. This work is partially supported by JSPS KAKENHI Nos. 15K00003, 25280025.

PY - 2016/6/1

Y1 - 2016/6/1

N2 - 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.

AB - 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.

KW - Ground confluence

KW - Non-orientable equations

KW - Rewriting induction

KW - Term rewriting systems

UR - http://www.scopus.com/inward/record.url?scp=84977589981&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84977589981&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.FSCD.2016.33

DO - 10.4230/LIPIcs.FSCD.2016.33

M3 - Conference contribution

AN - SCOPUS:84977589981

T3 - Leibniz International Proceedings in Informatics, LIPIcs

BT - 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016

A2 - Kesner, Delia

A2 - Pientka, Brigitte

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

T2 - 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016

Y2 - 22 June 2016 through 26 June 2016

ER -