2026

  1. Termination of Graph Transformation Systems via Generalized Weighted Type Graphs
    Jörg Endrullis, and Roy Overbeek
    Log. Methods Comput. Sci. , 22 (1) (2026)
    paper

    Summary

    We refine the weighted type graph technique for proving termination of double pushout (DPO) graph transformation systems. We increase the power of the approach for graphs, we generalize the technique to other categories, and we allow for variations of DPO that occur in the literature.

    This paper is an extended version of Generalized Weighted Type Graphs for Termination of Graph Transformation Systems (ICGT 2024).

    Bibtex

    @article{graph:termination:type:graphs:2026,
  author = {Endrullis, J{\"{o}}rg and Overbeek, Roy},
  title = {Termination of Graph Transformation Systems via Generalized Weighted
                    Type Graphs},
  journal = {Log. Methods Comput. Sci.},
  volume = {22},
  number = {1},
  year = {2026},
  url = {https://doi.org/10.46298/lmcs-22(1:15)2026},
  doi = {10.46298/LMCS-22(1:15)2026},
  biburl = {https://dblp.org/rec/journals/lmcs/EndrullisO26.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  keywords = {rewriting, termination},
  type = {journal}
}

    Digital Object Identifier

    10.46298/LMCS-22(1:15)2026

2024

  1. Termination of Graph Transformation Systems Using Weighted Subgraph Counting
    Roy Overbeek, and Jörg Endrullis
    Log. Methods Comput. Sci. , 20 (4) (2024)
    paper

    Summary

    We introduce a termination method for the algebraic graph transformation framework PBPO+, in which we weigh objects by summing a class of weighted morphisms targeting them. The method is well-defined in rm-adhesive quasitoposes (which include toposes and therefore many graph categories of interest), and is applicable to non-linear rules. The method is also defined for other frameworks, including SqPO and left-linear DPO, because we have previously shown that they are naturally encodable into PBPO+ in the quasitopos setting. We have implemented our method, and the implementation includes a REPL that can be used for guiding relative termination proofs.

    This paper is an extended version of Termination of Graph Transformation Systems Using Weighted Subgraph Counting (ICGT 2023).

    Bibtex

    @article{graph:termination:subgraph:counting:2024,
  author = {Overbeek, Roy and Endrullis, J{\"{o}}rg},
  title = {Termination of Graph Transformation Systems Using Weighted Subgraph
                    Counting},
  journal = {Log. Methods Comput. Sci.},
  volume = {20},
  number = {4},
  year = {2024},
  url = {https://doi.org/10.46298/lmcs-20(4:12)2024},
  doi = {10.46298/LMCS-20(4:12)2024},
  biburl = {https://dblp.org/rec/journals/lmcs/OverbeekE24.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  keywords = {rewriting, termination},
  type = {journal}
}

    Digital Object Identifier

    10.46298/LMCS-20(4:12)2024
  2. Generalized Weighted Type Graphs for Termination of Graph Transformation Systems
    Jörg Endrullis, and Roy Overbeek
    In: Graph Transformation - 17th International Conference, ICGT 2024, Held as Part of STAF 2024, Enschede, The Netherlands, July 10-11, 2024, Proceedings Harmer, Russ and Kosiol, Jens (eds.) , pp. 39–58 , Springer (2024)
    paper

    Summary

    We refine the weighted type graph technique for proving termination of double pushout (DPO) graph transformation systems. We increase the power of the approach for graphs, we generalize the technique to other categories, and we allow for variations of DPO that occur in the literature.

    An extended version appeared as Termination of Graph Transformation Systems via Generalized Weighted Type Graphs (LMCS 2026).

    Bibtex

    @inproceedings{graph:termination:type:graphs:2024,
  author = {Endrullis, J{\"{o}}rg and Overbeek, Roy},
  editor = {Harmer, Russ and Kosiol, Jens},
  title = {Generalized Weighted Type Graphs for Termination of Graph Transformation
                    Systems},
  booktitle = {Graph Transformation - 17th International Conference, {ICGT} 2024,
                    Held as Part of {STAF} 2024, Enschede, The Netherlands, July 10-11,
                    2024, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {14774},
  pages = {39--58},
  publisher = {Springer},
  year = {2024},
  url = {https://doi.org/10.1007/978-3-031-64285-2\_3},
  doi = {10.1007/978-3-031-64285-2\_3},
  biburl = {https://dblp.org/rec/conf/gg/EndrullisO24.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  keywords = {rewriting, termination},
  type = {conference}
}

    Digital Object Identifier

    10.1007/978-3-031-64285-2_3

2023

  1. Termination of Graph Transformation Systems Using Weighted Subgraph Counting
    Roy Overbeek, and Jörg Endrullis
    In: Graph Transformation - 16th International Conference, ICGT 2023, Held as Part of STAF 2023, Leicester, UK, July 19-20, 2023, Proceedings Fernández, Maribel and Poskitt, Christopher M. (eds.) , pp. 81–101 , Springer (2023)
    paper

    Summary

    We introduce a termination method for the algebraic graph transformation framework PBPO+, in which we weigh objects by summing a class of weighted morphisms targeting them. The method is well-defined in rm-adhesive quasitoposes (which include toposes and therefore many graph categories of interest), and is applicable to non-linear rules. The method is also defined for other frameworks, including SqPO and left-linear DPO, because we have previously shown that they are naturally encodable into PBPO+ in the quasitopos setting.

    An extended version appeared in Logical Methods in Computer Science (2024).

    Bibtex

    @inproceedings{graph:termination:subgraph:counting:2023,
  author = {Overbeek, Roy and Endrullis, J{\"{o}}rg},
  editor = {Fern{\'{a}}ndez, Maribel and Poskitt, Christopher M.},
  title = {Termination of Graph Transformation Systems Using Weighted Subgraph
                    Counting},
  booktitle = {Graph Transformation - 16th International Conference, {ICGT} 2023,
                    Held as Part of {STAF} 2023, Leicester, UK, July 19-20, 2023, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {13961},
  pages = {81--101},
  publisher = {Springer},
  year = {2023},
  url = {https://doi.org/10.1007/978-3-031-36709-0\_5},
  doi = {10.1007/978-3-031-36709-0\_5},
  biburl = {https://dblp.org/rec/conf/gg/OverbeekE23.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  keywords = {rewriting, termination},
  type = {conference}
}

    Digital Object Identifier

    10.1007/978-3-031-36709-0_5

2021

  1. Star Games and Hydras
    Jörg Endrullis, Jan Willem Klop, and Roy Overbeek
    Log. Methods Comput. Sci. , 17 (2) (2021)
    paper

    Summary

    The recursive path ordering is an established and crucial tool in term rewriting to prove termination. We revisit its presentation by means of some simple rules on trees (or corresponding terms) equipped with a 'star' as control symbol, signifying a command to make that tree (or term) smaller in the order being defined. This leads to star games that are very convenient for proving termination of many rewriting tasks. For instance, using already the simplest star game on finite unlabeled trees, we obtain a very direct proof of termination of the famous Hydra battle, direct in the sense that there is not the usual mention of ordinals. We also include an alternative road to setting up the star games, using a proof method of Buchholz, adapted by van Oostrom, resulting in a quantitative version of the star as control symbol. We conclude with a number of questions and future research directions.

    Bibtex

    @article{termination:star:games:2021,
  author = {Endrullis, J{\"{o}}rg and Klop, Jan Willem and Overbeek, Roy},
  title = {Star Games and Hydras},
  journal = {Log. Methods Comput. Sci.},
  volume = {17},
  number = {2},
  year = {2021},
  url = {https://lmcs.episciences.org/7518},
  biburl = {https://dblp.org/rec/journals/lmcs/EndrullisKO21.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  keywords = {rewriting, termination},
  type = {journal}
}

    Digital Object Identifier

  2. From Linear Term Rewriting to Graph Rewriting with Preservation Of Termination
    Roy Overbeek, and Jörg Endrullis
    In: Proceedings Twelfth International Workshop on Graph Computational Models, GCM@STAF 2021, Online, 22nd June 2021 Hoffmann, Berthold and Minas, Mark (eds.) , pp. 19–34 (2021)
    paper

    Summary

    Encodings of term rewriting systems (TRSs) into graph rewriting systems usually lose global termination, meaning the encodings do not terminate on all graphs. A typical encoding of the terminating TRS rule a(b(x)) -> b(a(x)), for example, may be indefinitely applicable along a cycle of a's and b's. Recently, we introduced PBPO+, a graph rewriting formalism in which rules employ a type graph to specify transformations and control rule applicability. In the present paper, we show that PBPO+ allows for a natural encoding of linear TRS rules that preserves termination globally. This result is a step towards modeling other rewriting formalisms, such as lambda calculus and higher order rewriting, using graph rewriting in a way that preserves properties like termination and confluence. We moreover expect that the encoding can serve as a guide for lifting TRS termination methods to PBPO+ rewriting.

    Bibtex

    @inproceedings{graph:termination:linear:2021,
  author = {Overbeek, Roy and Endrullis, J{\"{o}}rg},
  editor = {Hoffmann, Berthold and Minas, Mark},
  title = {From Linear Term Rewriting to Graph Rewriting with Preservation of
                    Termination},
  booktitle = {Proceedings Twelfth International Workshop on Graph Computational
                    Models, GCM@STAF 2021, Online, 22nd June 2021},
  series = {{EPTCS}},
  volume = {350},
  pages = {19--34},
  year = {2021},
  url = {https://doi.org/10.4204/EPTCS.350.2},
  doi = {10.4204/EPTCS.350.2},
  biburl = {https://dblp.org/rec/journals/corr/abs-2106-13826.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  keywords = {rewriting, termination},
  type = {workshop}
}

    Digital Object Identifier

    10.4204/EPTCS.350.2

2015

  1. Proving Non-Termination by Finite Automata
    Jörg Endrullis, and Hans Zantema
    In: Proc. Conf. on Rewriting Techniques and Applications (RTA 2015) , pp. 160–176 , Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)
    paper

    Summary

    We present a new technique to prove non-termination of term rewriting. The basic idea is tofind a non-empty regular language of terms that is weakly closed under rewriting and does not containnormal forms. It is automated by representing the language by a tree automaton with a fixednumber of states, and expressing the mentioned requirements in a SAT formula. Satisfiabilityof this formula implies non-termination. Our approach succeeds for many examples where allearlier techniques fail, for instance for the S-rule from combinatory logic.

    See research for an overview of my research on termination.

    Bibtex

    @inproceedings{termination:automata:2015,
  author = {Endrullis, J\"{o}rg and Zantema, Hans},
  title = {{Proving Non-termination by Finite Automata}},
  booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2015)},
  volume = {36},
  pages = {160--176},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  series = {LIPIcs},
  year = {2015},
  doi = {10.4230/LIPIcs.RTA.2015.160},
  keywords = {rewriting, termination, automata},
  type = {conference}
}

    Digital Object Identifier

    10.4230/LIPIcs.RTA.2015.160

2013

  1. SAT Compilation for Termination Proofs via Semantic Labelling
    Alexander Bau, Jörg Endrullis, and Johannes Waldmann
    In: Proc. Workshop on Termination (WST 2007) (2013)
    paper

    Bibtex

    @inproceedings{termination:sat:compilation:2014,
  author = {Bau, Alexander and Endrullis, J\"{o}rg and Waldmann, Johannes},
  title = {{SAT compilation for Termination Proofs via Semantic Labelling}},
  booktitle = {Proc.\ Workshop on Termination (WST~2007)},
  year = {2013},
  keywords = {rewriting, termination},
  type = {workshop}
}

    Digital Object Identifier

2011

  1. Lazy Productivity via Termination
    Jörg Endrullis, and Dimitri Hendriks
    Theoretical Computer Science , 412 (28) , pp. 3203–3225 (2011)
    paper

    Bibtex

    @article{productivity:termination:2011,
  author = {Endrullis, J\"{o}rg and Hendriks, Dimitri},
  title = {{Lazy Productivity via Termination}},
  journal = {Theoretical Computer Science},
  volume = {412},
  number = {28},
  pages = {3203--3225},
  year = {2011},
  doi = {10.1016/j.tcs.2011.03.024},
  keywords = {rewriting, infinitary rewriting, productivity, termination},
  type = {journal}
}

    Digital Object Identifier

    10.1016/j.tcs.2011.03.024
  2. Levels of Undecidability in Rewriting
    Jörg Endrullis, Herman Geuvers, Jakob Grue Simonsen, and Hans Zantema
    Information and Computation , 209 (2) , pp. 227–245 (2011)
    paper

    Summary

    Undecidability of various properties of first-order term rewriting systems is well-known. An undecidable property can be classified by the complexity of the formula defining it. This classification gives rise to a hierarchy of distinct levels of undecidability, starting from the arithmetical hierarchy classifying properties using first order arithmetical formulas, and continuing into the analytic hierarchy, where quantification over function variables is allowed.

    In this paper we give an overview of how the main properties of first-order term rewriting systems are classified in these hierarchies. We consider properties related to normalization (strong normalization, weak normalization and dependency problems) and properties related to confluence (confluence, local confluence and the unique normal form property). For all of these we distinguish between the single term version and the uniform version. Where appropriate, we also distinguish between ground and open terms.

    Most uniform properties are \( \Pi^0_2 \)-complete. The particular problem of local confluence turns out to be \( \Pi^0_2 \)-complete for ground terms, but only \( \Sigma^0_1 \)-complete (and thereby recursively enumerable) for open terms. The most surprising result concerns dependency pair problems without minimality flag: we prove this problem to be \( \Pi^1_1 \)-complete, hence not in the arithmetical hierarchy, but properly in the analytic hierarchy.

    This paper is an extended version of Degrees of Undecidability in Term Rewriting (CSL 2009).

    Bibtex

    @article{rewriting:undecidability:levels:2011,
  author = {Endrullis, J\"{o}rg and Geuvers, Herman and Simonsen, Jakob Grue and Zantema, Hans},
  title = {{Levels of Undecidability in Rewriting}},
  journal = {Information and Computation},
  volume = {209},
  number = {2},
  pages = {227--245},
  year = {2011},
  doi = {10.1016/j.ic.2010.09.003},
  keywords = {rewriting, undecidability, termination, confluence},
  type = {journal}
}

    Digital Object Identifier

    10.1016/j.ic.2010.09.003

2010

  1. Local Termination: Theory and Practice
    Jörg Endrullis, Roel C. de Vrijer, and Johannes Waldmann
    Logical Methods in Computer Science , 6 (3) (2010)
    paper

    Bibtex

    @article{termination:local:2010,
  author = {Endrullis, J\"{o}rg and de~Vrijer, Roel C. and Waldmann, Johannes},
  title = {{Local Termination: Theory and Practice}},
  journal = {Logical Methods in Computer Science},
  volume = {6},
  number = {3},
  year = {2010},
  doi = {10.2168/LMCS-6(3:20)2010},
  keywords = {rewriting, termination, automata},
  type = {journal}
}

    Digital Object Identifier

    10.2168/LMCS-6(3:20)2010
  2. Transforming Outermost into Context-Sensitive Rewriting
    Jörg Endrullis, and Dimitri Hendriks
    Logical Methods in Computer Science , 6 (2) (2010)
    paper

    Summary

    We define two transformations from term rewriting systems (TRSs) to context-sensitive TRSs in such a way that termination of the target system implies outermost termination of the original system. In the transformation based on `context extension', each outermost rewrite step is modeled by exactly one step in the transformed system. This transformation turns out to be complete for the class of left-linear TRSs. The second transformation is called `dynamic labeling' and results in smaller sized context-sensitive TRSs. Here each modeled step is adjoined with a small number of auxiliary steps. As a result state-of-the-art termination methods for context-sensitive rewriting become available for proving termination of outermost rewriting. Both transformations have been implemented in Jambox, making it the most successful tool in the category of outermost rewriting of the annual termination competition.

    This is an extended version of the paper From Outermost to Context-Sensitive Rewriting (RTA 2009).

    See research for an overview of my research on termination.

    Bibtex

    @article{termination:outermost:2010,
  author = {Endrullis, J\"{o}rg and Hendriks, Dimitri},
  title = {{Transforming Outermost into Context-Sensitive Rewriting}},
  journal = {Logical Methods in Computer Science},
  volume = {6},
  number = {2},
  year = {2010},
  doi = {10.2168/LMCS-6(2:5)2010},
  keywords = {rewriting, termination, automata},
  type = {journal}
}

    Digital Object Identifier

    10.2168/LMCS-6(2:5)2010

2009

  1. From Outermost to Context-Sensitive Rewriting
    Jörg Endrullis, and Dimitri Hendriks
    In: Proc. Conf. on Rewriting Techniques and Applications (RTA 2009) , pp. 305–319 , Springer (2009)
    paper

    Summary

    We define a transformation from term rewriting systems (TRSs) to context-sensitive TRSs in such a way that termination of the target system implies outermost termination of the original system. For the class of left-linear TRSs the transformation is complete. Thereby state-of-the-art termination methods and automated termination provers for context-sensitive rewriting become available for proving termination of outermost rewriting. The translation has been implemented in Jambox, making it the most successful tool in the category of outermost rewriting of the last edition of the annual termination competition.

    An extended version of this paper is available from Transforming Outermost into Context-Sensitive Rewriting (Logical Methods in Computer Science 2010).

    See research for an overview of my research on termination.

    Bibtex

    @inproceedings{termination:outermost:2009,
  author = {Endrullis, J\"{o}rg and Hendriks, Dimitri},
  title = {{From Outermost to Context-Sensitive Rewriting}},
  booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2009)},
  volume = {5595},
  pages = {305--319},
  publisher = {Springer},
  series = {LNCS},
  year = {2009},
  doi = {10.1007/978-3-642-02348-4\_22},
  keywords = {rewriting, termination, automata},
  type = {conference}
}

    Digital Object Identifier

    10.1007/978-3-642-02348-4_22
  2. Local Termination
    Jörg Endrullis, Roel C. de Vrijer, and Johannes Waldmann
    In: Proc. Conf. on Rewriting Techniques and Applications (RTA 2009) , pp. 270–284 , Springer (2009)
    paper

    Bibtex

    @inproceedings{termination:local:2009,
  author = {Endrullis, J\"{o}rg and de~Vrijer, Roel C. and Waldmann, Johannes},
  title = {{Local Termination}},
  booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2009)},
  volume = {5595},
  pages = {270--284},
  publisher = {Springer},
  series = {LNCS},
  year = {2009},
  doi = {10.1007/978-3-642-02348-4\_19},
  keywords = {rewriting, termination, automata},
  type = {conference}
}

    Digital Object Identifier

    10.1007/978-3-642-02348-4_19
  3. Degrees of Undecidability in Term Rewriting
    Jörg Endrullis, Herman Geuvers, and Hans Zantema
    In: Proc. Conf. on Computer Science Logic (CSL 2009) , pp. 255–270 , Springer (2009)
    paper

    Summary

    Undecidability of various properties of first-order term rewriting systems is well-known. An undecidable property can be classified by the complexity of the formula defining it. This classification gives rise to a hierarchy of distinct levels of undecidability, starting from the arithmetical hierarchy classifying properties using first order arithmetical formulas, and continuing into the analytic hierarchy, where quantification over function variables is allowed.

    In this paper we give an overview of how the main properties of first-order term rewriting systems are classified in these hierarchies. We consider properties related to normalization (strong normalization, weak normalization and dependency problems) and properties related to confluence (confluence, local confluence and the unique normal form property). For all of these we distinguish between the single term version and the uniform version. Where appropriate, we also distinguish between ground and open terms.

    Most uniform properties are \( \Pi^0_2 \)-complete. The particular problem of local confluence turns out to be \( \Pi^0_2 \)-complete for ground terms, but only \( \Sigma^0_1 \)-complete (and thereby recursively enumerable) for open terms. The most surprising result concerns dependency pair problems without minimality flag: we prove this problem to be \( \Pi^1_1 \)-complete, hence not in the arithmetical hierarchy, but properly in the analytic hierarchy.

    We refer to Levels of Undecidability in Rewriting (Information and Computation 2011) for an extended journal version of this paper.

    Bibtex

    @inproceedings{rewriting:undecidability:degrees:2009,
  author = {Endrullis, J\"{o}rg and Geuvers, Herman and Zantema, Hans},
  title = {{Degrees of Undecidability in Term Rewriting}},
  booktitle = {Proc.\ Conf.\ on Computer Science Logic (CSL~2009)},
  volume = {5771},
  pages = {255--270},
  publisher = {Springer},
  series = {LNCS},
  year = {2009},
  doi = {10.1007/978-3-642-04027-6\_20},
  keywords = {rewriting, undecidability, termination, confluence},
  type = {conference}
}

    Digital Object Identifier

    10.1007/978-3-642-04027-6_20

2008

  1. Matrix Interpretations for Proving Termination of Term Rewriting
    Jörg Endrullis, Johannes Waldmann, and Hans Zantema
    Journal of Automated Reasoning , 40 (2-3) , pp. 195–220 (2008)
    paper

    Summary

    We present a new method for automatically proving termination of term rewriting using matrix interpretation (weighted automata with natural numbers as weights). It is based on the well-known idea of interpretation of terms where every rewrite step causes a decrease, but instead of the usual natural numbers we use vectors of natural numbers, ordered by a particular nontotal well-founded ordering. Function symbols are interpreted by linear mappings represented by matrices. This method allows us to prove termination and relative termination.

    A modification of the latter, in which strict steps are only allowed at the top, turns out to be helpful in combination with the dependency pair transformation. By bounding the dimension and the matrix coefficients, the search problem becomes finite. Our implementation transforms it to a Boolean satisfiability problem (SAT), to be solved by a state-of-the-art SAT solver.

    This is an extended version of the paper Matrix Interpretations for Proving Termination of Term Rewriting (IJCAR 2006).

    See research for an overview of my research on termination.

    Bibtex

    @article{termination:matrix:2008,
  author = {Endrullis, J\"{o}rg and Waldmann, Johannes and Zantema, Hans},
  title = {{Matrix Interpretations for Proving Termination of Term Rewriting}},
  journal = {Journal of Automated Reasoning},
  volume = {40},
  number = {2-3},
  pages = {195--220},
  year = {2008},
  doi = {10.1007/s10817-007-9087-9},
  keywords = {rewriting, termination},
  type = {journal}
}

    Digital Object Identifier

    10.1007/s10817-007-9087-9

2007

  1. Root Stabilisation Using Dependency Pairs
    Jörg Endrullis, and Jeroen Ketema
    In: Proc. Workshop on Termination (WST 2007) , pp. 17–21 (2007)
    paper

    Bibtex

    @inproceedings{termination:root:2007,
  author = {Endrullis, J\"{o}rg and Ketema, Jeroen},
  title = {{Root Stabilisation Using Dependency Pairs}},
  booktitle = {Proc.\ Workshop on Termination (WST~2007)},
  pages = {17--21},
  year = {2007},
  keywords = {rewriting, infinitary rewriting, termination},
  type = {workshop}
}

    Digital Object Identifier

2006

  1. Matrix Interpretations for Proving Termination of Term Rewriting
    Jörg Endrullis, Johannes Waldmann, and Hans Zantema
    In: Proc. Int. Joint Conf. on Automated Reasoning (IJCAR 2006) , pp. 574–588 , Springer (2006)
    paper

    Summary

    We present a new method for automatically proving termination of term rewriting using matrix interpretation (weighted automata with natural numbers as weights). It is based on the well-known idea of interpretation of terms where every rewrite step causes a decrease, but instead of the usual natural numbers we use vectors of natural numbers, ordered by a particular non-total well-founded ordering. Function symbols are interpreted by linear mappings represented by matrices. This method allows to prove termination and relative termination. A modification of the latter in which strict steps are only allowed at the top, turns out to be helpful in combination with the dependency pair transformation.

    By bounding the dimension and the matrix coefficients, the search problem becomes finite. Our implementation transforms it to a Boolean satisfiability problem (SAT), to be solved by a state-of-the-art SAT solver. Our implementation performs well on the Termination Problem Data Base: better than 5 out of 6 tools that participated in the 2005 termination competition in the category of term rewriting.

    An extended journal version of this paper is available from Matrix Interpretations for Proving Termination of Term Rewriting (Journal of Automated Reasoning 2008).

    See research for an overview of my research on termination.

    Bibtex

    @inproceedings{termination:matrix:2006,
  author = {Endrullis, J\"{o}rg and Waldmann, Johannes and Zantema, Hans},
  title = {{Matrix Interpretations for Proving Termination of Term Rewriting}},
  booktitle = {Proc.\ Int.\ Joint Conf.\ on Automated Reasoning (IJCAR~2006)},
  volume = {4130},
  pages = {574--588},
  publisher = {Springer},
  series = {LNCS},
  year = {2006},
  doi = {10.1007/11814771\_47},
  keywords = {rewriting, termination, automata},
  type = {conference}
}

    Digital Object Identifier

    10.1007/11814771_47
  2. Decomposing Terminating Rewrite Relations
    Jörg Endrullis, Dieter Hofbauer, and Johannes Waldmann
    In: Proc. Workshop on Termination (WST 2006) , pp. 39–43 (2006)
    paper

    Summary

    In this paper we are concerned with automatically proving termination of string rewriting systems (or word rewriting systems). We introduce an efficient technique for constructing automata that serve as certificates of match-boundedness, and thereby termination. Previously constructions have either been inefficient or incomplete:

    • Match-Bounded String Rewriting Systems by Alfons Geser, Dieter Hofbauer and Johannes Waldmann. The construction in this paper is complete but very inefficient.
    • On tree automata that certify termination of left-linear term rewriting systems by Alfons Geser, Dieter Hofbauer, Johannes Waldmann and Hans Zantema. The construction in this paper is efficient but incomplete.
      • We present the first automata construction for matchbounded string rewriting that is both efficient and complete. Here completenss means that the algorithm always terminates if the system is matchbounded.

    See research for an overview of my research on termination.

    Bibtex

    @inproceedings{termination:matchbounds:2006,
  author = {Endrullis, J\"{o}rg and Hofbauer, Dieter and Waldmann, Johannes},
  title = {{Decomposing Terminating Rewrite Relations}},
  booktitle = {Proc.\ Workshop on Termination (WST~2006)},
  pages = {39--43},
  year = {2006},
  keywords = {rewriting, termination, automata},
  type = {workshop}
}

    Digital Object Identifier