28 citations · 56 across the 20 of their papers we have counts for
5 papers · 1 filter
The Generalized Subterm Criterion in TTT2
Christian Sternagel
We present an SMT encoding of a generalized version of the subterm criterion and evaluate its implementation in TTT2.
A Characterization of Quasi-Decreasingness
Thomas Sternagel, Christian Sternagel
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 t…
Formalized Confluence of Quasi-Decreasing, Strongly Deterministic Conditional TRSs
Thomas Sternagel, Christian Sternagel
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-…
A Short Mechanized Proof of the Church-Rosser Theorem by the Z-property for the -calculus in Nominal Isabelle
Julian Nagele, Vincent van Oostrom, Christian Sternagel
We present a short proof of the Church-Rosser property for the lambda-calculus enjoying two distinguishing features: Firstly, it employs the Z-property, resulting in a short and el…
Level-Confluence of 3-CTRSs in Isabelle/HOL
Christian Sternagel, Thomas Sternagel
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 for…