Search Results

Documents authored by Aoto, Takahito

Document
DOI: 10.4230/LIPIcs.FSCD.2024.31
Equational Theories and Validity for Logically Constrained Term Rewriting

Authors: Takahito Aoto, Naoki Nishida, and Jonas Schöpf

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Logically constrained term rewriting is a relatively new formalism where rules are equipped with constraints over some arbitrary theory. Although there are many recent advances with respect to rewriting induction, completion, complexity analysis and confluence analysis for logically constrained term rewriting, these works solely focus on the syntactic side of the formalism lacking detailed investigations on semantics. In this paper, we investigate a semantic side of logically constrained term rewriting. To this end, we first define constrained equations, constrained equational theories and validity of the former based on the latter. After presenting the relationship of validity and conversion of rewriting, we then construct a sound inference system to prove validity of constrained equations in constrained equational theories. Finally, we give an algebraic semantics, which enables one to establish invalidity of constrained equations in constrained equational theories. This algebraic semantics derives a new notion of consistency for constrained equational theories.
Cite as

Takahito Aoto, Naoki Nishida, and Jonas Schöpf. Equational Theories and Validity for Logically Constrained Term Rewriting. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 31:1-31:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{aoto_et_al:LIPIcs.FSCD.2024.31,
  author =	{Aoto, Takahito and Nishida, Naoki and Sch\"{o}pf, Jonas},
  title =	{{Equational Theories and Validity for Logically Constrained Term Rewriting}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{31:1--31:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.31},
  URN =		{urn:nbn:de:0030-drops-203607},
  doi =		{10.4230/LIPIcs.FSCD.2024.31},
  annote =	{Keywords: constrained equation, constrained equational theory, logically constrained term rewriting, algebraic semantics, consistency}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2021.49
Simple Derivation Systems for Proving Sufficient Completeness of Non-Terminating Term Rewriting Systems

Authors: Kentaro Kikuchi and Takahito Aoto

Published in: LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

Abstract
A term rewriting system (TRS) is said to be sufficiently complete when each function yields some value for any input. Proof methods for sufficient completeness of terminating TRSs have been well studied. In this paper, we introduce a simple derivation system for proving sufficient completeness of possibly non-terminating TRSs. The derivation system consists of rules to manipulate a set of guarded terms, and sufficient completeness of a TRS holds if there exists a successful derivation for each function symbol. We also show that variations of the derivation system are useful for proving special cases of local sufficient completeness of TRSs, which is a generalised notion of sufficient completeness.
Cite as

Kentaro Kikuchi and Takahito Aoto. Simple Derivation Systems for Proving Sufficient Completeness of Non-Terminating Term Rewriting Systems. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 49:1-49:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kikuchi_et_al:LIPIcs.FSTTCS.2021.49,
  author =	{Kikuchi, Kentaro and Aoto, Takahito},
  title =	{{Simple Derivation Systems for Proving Sufficient Completeness of Non-Terminating Term Rewriting Systems}},
  booktitle =	{41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
  pages =	{49:1--49:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-215-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{213},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.49},
  URN =		{urn:nbn:de:0030-drops-155602},
  doi =		{10.4230/LIPIcs.FSTTCS.2021.49},
  annote =	{Keywords: Term rewriting, Sufficient completeness, Local sufficient completeness, Non-termination, Derivation rule, Well-founded induction schema}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2020.11
A Fast Decision Procedure For Uniqueness of Normal Forms w.r.t. Conversion of Shallow Term Rewriting Systems

Authors: Masaomi Yamaguchi and Takahito Aoto

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
Uniqueness of normal forms w.r.t. conversion (UNC) of term rewriting systems (TRSs) guarantees that there are no distinct convertible normal forms. It was recently shown that the UNC property of TRSs is decidable for shallow TRSs (Radcliffe et al., 2010). The existing procedure mainly consists of testing whether there exists a counterexample in a finite set of candidates; however, the procedure suffers a bottleneck of having a sheer number of such candidates. In this paper, we propose a new procedure which consists of checking a smaller number of such candidates and enumerating such candidates more efficiently. Correctness of the proposed procedure is proved and its complexity is analyzed. Furthermore, these two procedures have been implemented and it is experimentally confirmed that the proposed procedure runs much faster than the existing procedure.
Cite as

Masaomi Yamaguchi and Takahito Aoto. A Fast Decision Procedure For Uniqueness of Normal Forms w.r.t. Conversion of Shallow Term Rewriting Systems. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 11:1-11:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{yamaguchi_et_al:LIPIcs.FSCD.2020.11,
  author =	{Yamaguchi, Masaomi and Aoto, Takahito},
  title =	{{A Fast Decision Procedure For Uniqueness of Normal Forms w.r.t. Conversion of Shallow Term Rewriting Systems}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{11:1--11:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.11},
  URN =		{urn:nbn:de:0030-drops-123338},
  doi =		{10.4230/LIPIcs.FSCD.2020.11},
  annote =	{Keywords: uniqueness of normal forms w.r.t. conversion, shallow term rewriting systems, decision procedure}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.32
Confluence Competition 2018

Authors: Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani, and Harald Zankl

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
We report on the 2018 edition of the Confluence Competition, a competition of software tools that aim to (dis)prove confluence and related properties of rewrite systems automatically.
Cite as

Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani, and Harald Zankl. Confluence Competition 2018. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 32:1-32:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{aoto_et_al:LIPIcs.FSCD.2018.32,
  author =	{Aoto, Takahito and Hamana, Makoto and Hirokawa, Nao and Middeldorp, Aart and Nagele, Julian and Nishida, Naoki and Shintani, Kiraku and Zankl, Harald},
  title =	{{Confluence Competition 2018}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{32:1--32:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.32},
  URN =		{urn:nbn:de:0030-drops-92023},
  doi =		{10.4230/LIPIcs.FSCD.2018.32},
  annote =	{Keywords: Confluence, competition, rewrite systems}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.7
Improving Rewriting Induction Approach for Proving Ground Confluence

Authors: Takahito Aoto, Yoshihito Toyama, and Yuta Kimura

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract
In (Aoto&Toyama, FSCD 2016), a method to prove ground confluence of many-sorted term rewriting systems based on rewriting induction is given. In this paper, we give several methods that add wider flexibility to the rewriting induction approach for proving ground confluence. Firstly, we give a method to deal with the case in which suitable rules are not presented in the input system. Our idea is to construct additional rewrite rules that supplement or replace existing rules in order to obtain a set of rules that is adequate for applying rewriting induction. Secondly, we give a method to deal with non-orientable constructor rules. This is accomplished by extending the inference system of rewriting induction and giving a sufficient criterion for the correctness of the system. Thirdly, we give a method to deal with disproving ground confluence. The presented methods are implemented in our ground confluence prover AGCP and experiments are reported. Our experiments reveal the presented methods are effective to deal with problems for which state-of-the-art ground confluence provers can not handle.
Cite as

Takahito Aoto, Yoshihito Toyama, and Yuta Kimura. Improving Rewriting Induction Approach for Proving Ground Confluence. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{aoto_et_al:LIPIcs.FSCD.2017.7,
  author =	{Aoto, Takahito and Toyama, Yoshihito and Kimura, Yuta},
  title =	{{Improving Rewriting Induction Approach for Proving Ground Confluence}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{7:1--7:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.7},
  URN =		{urn:nbn:de:0030-drops-77310},
  doi =		{10.4230/LIPIcs.FSCD.2017.7},
  annote =	{Keywords: Ground Confluence, Rewriting Induction, Non-Orientable Equations, Term Rewriting Systems}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.33
Ground Confluence Prover based on Rewriting Induction

Authors: Takahito Aoto and Yoshihito Toyama

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

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.
Cite as

Takahito Aoto and Yoshihito Toyama. Ground Confluence Prover based on Rewriting Induction. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 33:1-33:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{aoto_et_al:LIPIcs.FSCD.2016.33,
  author =	{Aoto, Takahito and Toyama, Yoshihito},
  title =	{{Ground Confluence Prover based on Rewriting Induction}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{33:1--33:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.33},
  URN =		{urn:nbn:de:0030-drops-59873},
  doi =		{10.4230/LIPIcs.FSCD.2016.33},
  annote =	{Keywords: Ground Confluence, Rewriting Induction, Non-Orientable Equations, Term Rewriting Systems}
}
Document
DOI: 10.4230/LIPIcs.RTA.2015.301
Confluence of Orthogonal Nominal Rewriting Systems Revisited

Authors: Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, and Yoshihito Toyama

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract
Nominal rewriting systems (Fernandez, Gabbay, Mackie, 2004; Fernandez, Gabbay, 2007) have been introduced as a new framework of higher-order rewriting systems based on the nominal approach (Gabbay, Pitts, 2002; Pitts, 2003), which deals with variable binding via permutations and freshness conditions on atoms. Confluence of orthogonal nominal rewriting systems has been shown in (Fernandez, Gabbay, 2007). However, their definition of (non-trivial) critical pairs has a serious weakness so that the orthogonality does not actually hold for most of standard nominal rewriting systems in the presence of binders. To overcome this weakness, we divide the notion of overlaps into the self-rooted and proper ones, and introduce a notion of alpha-stability which guarantees alpha-equivalence of peaks from the self-rooted overlaps. Moreover, we give a sufficient criterion for uniformity and alpha-stability. The new definition of orthogonality and the criterion offer a novel confluence condition effectively applicable to many standard nominal rewriting systems. We also report on an implementation of a confluence prover for orthogonal nominal rewriting systems based on our framework.
Cite as

Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, and Yoshihito Toyama. Confluence of Orthogonal Nominal Rewriting Systems Revisited. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 301-317, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{suzuki_et_al:LIPIcs.RTA.2015.301,
  author =	{Suzuki, Takaki and Kikuchi, Kentaro and Aoto, Takahito and Toyama, Yoshihito},
  title =	{{Confluence of Orthogonal Nominal Rewriting Systems Revisited}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{301--317},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.301},
  URN =		{urn:nbn:de:0030-drops-52042},
  doi =		{10.4230/LIPIcs.RTA.2015.301},
  annote =	{Keywords: Nominal rewriting, Confluence, Orthogonality, Higher-order rewriting, alpha-equivalence}
}
Document
DOI: 10.4230/LIPIcs.RTA.2011.91
A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems

Authors: Takahito Aoto and Yoshihito Toyama

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract
We give a method to prove confluence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity. Usually, confluence of term rewriting systems containing such rules is proved by treating them as equational term rewriting systems and considering E-critical pairs and/or termination modulo E. In contrast, our method is based solely on usual critical pairs and usual termination. We first present confluence criteria for term rewriting systems whose rewrite rules can be partitioned into terminating part and possibly non-terminating part. We then give a reduction-preserving completion procedure so that the applicability of the criteria is enhanced. In contrast to the well-known Knuth-Bendix completion procedure which preserves the equivalence relation of the system, our completion procedure preserves the reduction relation of the system, by which confluence of the original system is inferred from that of the completed system.
Cite as

Takahito Aoto and Yoshihito Toyama. A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 91-106, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{aoto_et_al:LIPIcs.RTA.2011.91,
  author =	{Aoto, Takahito and Toyama, Yoshihito},
  title =	{{A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{91--106},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.91},
  URN =		{urn:nbn:de:0030-drops-31105},
  doi =		{10.4230/LIPIcs.RTA.2011.91},
  annote =	{Keywords: Confluence, Completion, Equational Term Rewriting Systems, Confluence Modulo Equations}
}
Document
DOI: 10.4230/LIPIcs.RTA.2011.107
Natural Inductive Theorems for Higher-Order Rewriting

Authors: Takahito Aoto, Toshiyuki Yamada, and Yuki Chiba

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract
The notion of inductive theorems is well-established in first-order term rewriting. In higher-order term rewriting, in contrast, it is not straightforward to extend this notion because of extensionality (Meinke, 1992). When extending the term rewriting based program transformation of Chiba et al. (2005) to higher-order term rewriting, we need extensibility, a property stating that inductive theorems are preserved by adding new functions via macros. In this paper, we propose and study a new notion of inductive theorems for higher-order rewriting, natural inductive theorems. This allows to incorporate properties such as extensionality and extensibility, based on simply typed S-expression rewriting (Yamada, 2001).
Cite as

Takahito Aoto, Toshiyuki Yamada, and Yuki Chiba. Natural Inductive Theorems for Higher-Order Rewriting. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 107-121, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{aoto_et_al:LIPIcs.RTA.2011.107,
  author =	{Aoto, Takahito and Yamada, Toshiyuki and Chiba, Yuki},
  title =	{{Natural Inductive Theorems for Higher-Order Rewriting}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{107--121},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.107},
  URN =		{urn:nbn:de:0030-drops-31119},
  doi =		{10.4230/LIPIcs.RTA.2011.107},
  annote =	{Keywords: Inductive Theorems, Higher-Order Equational Logic, Simply-Typed S-Expression Rewriting Systems, Term Rewriting Systems}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.7
Automated Confluence Proof by Decreasing Diagrams based on Rule-Labelling

Authors: Takahito Aoto

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
Decreasing diagrams technique (van Oostrom, 1994) is a technique that can be widely applied to prove confluence of rewrite systems. To directly apply the decreasing diagrams technique to prove confluence of rewrite systems, rule-labelling heuristic has been proposed by van Oostrom (2008). We show how constraints for ensuring confluence of term rewriting systems constructed based on the rule-labelling heuristic are encoded as linear arithmetic constraints suitable for solving the satisfiability of them by external SMT solvers. We point out an additional constraint omitted in (van Oostrom, 2008) that is needed to guarantee the soundness of confluence proofs based on the rule-labelling heuristic extended to deal with non-right-linear rules. We also present several extensions of the rule-labelling heuristic by which the applicability of the technique is enlarged.
Cite as

Takahito Aoto. Automated Confluence Proof by Decreasing Diagrams based on Rule-Labelling. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 7-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{aoto:LIPIcs.RTA.2010.7,
  author =	{Aoto, Takahito},
  title =	{{Automated Confluence Proof by Decreasing Diagrams based on Rule-Labelling}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{7--16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.7},
  URN =		{urn:nbn:de:0030-drops-26418},
  doi =		{10.4230/LIPIcs.RTA.2010.7},
  annote =	{Keywords: Confluence, Decreasing Diagrams, Automation, Term Rewriting Systems}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2008.1737
Sound Lemma Generation for Proving Inductive Validity of Equations

Authors: Takahito Aoto

Published in: LIPIcs, Volume 2, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2008)

Abstract
In many automated methods for proving inductive theorems, finding a suitable generalization of a conjecture is a key for the success of proof attempts. On the other hand, an obtained generalized conjecture may not be a theorem, and in this case hopeless proof attempts for the incorrect conjecture are made, which is against the success and efficiency of theorem proving. Urso and Kounalis (2004) proposed a generalization method for proving inductive validity of equations, called sound generalization, that avoids such an over-generalization. Their method guarantees that if the original conjecture is an inductive theorem then so is the obtained generalization. In this paper, we revise and extend their method. We restore a condition on one of the characteristic argument positions imposed in their previous paper and show that otherwise there exists a counterexample to their main theorem. We also relax a condition imposed in their framework and add some flexibilities to some of other characteristic argument positions so as to enlarge the scope of the technique.
Cite as

Takahito Aoto. Sound Lemma Generation for Proving Inductive Validity of Equations. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 2, pp. 13-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{aoto:LIPIcs.FSTTCS.2008.1737,
  author =	{Aoto, Takahito},
  title =	{{Sound Lemma Generation for Proving Inductive Validity of Equations}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{13--24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-08-8},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{2},
  editor =	{Hariharan, Ramesh and Mukund, Madhavan and Vinay, V},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2008.1737},
  URN =		{urn:nbn:de:0030-drops-17379},
  doi =		{10.4230/LIPIcs.FSTTCS.2008.1737},
  annote =	{Keywords: Sound generalization, inductive theorem, automated theorem proving, term rewriting}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact