arXiv subjects
Publications and source records attributed to Thomas Sternagel.
We present three methods to check CTRSs for non-confluence: (1) an ad hoc method for 4-CTRSs, (2) a specialized method for unconditional critical pairs, and finally, (3) a method that employs conditional narrowing to find non-confluence witnesses. We shortly describe our implementation of these methods in ConCon, then look into their certification with CeTA, and finally conclude with experiments on the confluence problems database (Cops).
We propose a notion of complexity for oriented conditional term rewrite systems satisfying certain restrictions. This notion is realistic in the sense that it measures not only successful computations, but also partial computations that result in a failed rule application. A transformation to unconditional context-sensitive rewrite systems is presented which reflects this complexity notion, as well as a technique to derive runtime and derivational complexity bounds for the result of this transformation.
We present an Isabelle/HOL formalization of a characterization of confluence for quasi-reductive strongly deterministic conditional term rewrite systems, due to Avenhaus and Loría-Sáenz.
In 2010 Schernhammer and Gramlich showed that quasi-decreasingness of a DCTRS R is equivalent to μ-termination of its context-sensitive unraveling Ucs(R) on original terms. While the direction that quasi-decreasingness of R implies μ-termination of Ucs(R) on original terms is shown directly; the converse - facilitating the use of context-sensitive termination tools like MU-TERM and VMTL - employs the additional notion of context-sensitive quasi-reductivity of R. In the following, we give a direct proof of the fact that μ-termination of Ucs(R) on original terms implies quasi-decreasingness of R. Moreover, we report our experimental findings on DCTRSs from the confluence problems database (Cops), extending the experiments of Schernhammer and Gramlich.
We present an Isabelle/HOL formalization of an earlier result by Suzuki, Middeldorp, and Ida; namely that a certain class of conditional rewrite systems is level-confluent. Our formalization is basically along the lines of the original proof, from which we deviate mostly in the level of detail as well as concerning some basic definitions.
This paper describes the automatic mode of the new version of the Knuth-Bendix Completion Visualizer. The internally used data structures have been overhauled and the performance was dramatically improved by introducing caching, parallelization, and term- indexing in the computation of critical pairs and simplification. The new version is much faster and can complete three more systems.
When we want to answer/certify whether a given equation is entailed by an equational system we face the following problems: (1) It is hard to find a conversion (but easy to certify a given one). (2) Under the assumption that Knuth-Bendix completion is successful, it is easy to decide the existence of a conversion but hard to certify this decision. In this paper we introduce recording completion, which overcomes both problems.