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

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