Search

Completion is one of the most studied techniques in term rewriting and fundamental to automated reasoning with equalities. In this paper we present new correctness proofs of abstract completion, both for finite and infinite runs. For the special case of ground completion we present a new proof based on random descent. We moreover extend the results to ordered completion, an important extension of completion that aims to produce ground-complete presentations of the initial equations. We present new proofs concerning the completeness of ordered completion for two settings. Moreover, we revisit and extend results of M\'etivier concerning canonicity of rewrite systems. All proofs presented in the paper have been formalized in Isabelle/HOL., Logical Methods in Computer Science ; Volume 15, Issue 3 ; 1860-5974

This is an introduction to the remote_build tool for transparent remote session builds. The intended workflow for a user is to locally issue a build command for some session heap images and then continue working, while the actual build runs on a remote machine and the resulting heap images are synchronized incrementally as soon as they are available., Accepted at Isabelle Workshop 2018

On the one hand, ordered completion is a fundamental technique in equational theorem proving that is employed by automated tools. On the other hand, their complexity makes such tools inherently error prone. As a remedy to this situation we give an Isabelle/HOL formalization of ordered rewriting and completion that comes with a formally verified certifier for ordered completion proofs. By validating generated proof certificates, our certifier increases the reliability of ordered completion tools., Comment: accepted at 7th International Workshop on Confluence 2018

On the one hand, checking specific termination proofs by hand, say using a particular collection of matrix interpretations, can be an arduous and error-prone task. On the other hand, automation of such checks would save time and help to establish correctness of exam solutions, examples in lecture notes etc. To this end, we introduce a template mechanism for the termination tool TTT2 that allows us to restrict parameters of certain termination methods. In the extreme, when all parameters are fixed, such restrictions result in checks for specific proofs., Comment: Accepted at the International Workshop on Termination 2018

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)., Comment: 5 pages

We present an SMT encoding of a generalized version of the subterm criterion and evaluate its implementation in TTT2., In Proceedings of 15th International Workshop on Termination (WST 2016)

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\'ia-S\'aenz., Comment: IWC 2016

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., In Proceedings of the 4th International Workshop on Confluence (IWC 2015)

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 elegant proof; and secondly, it is formalized in the nominal higher-order logic available for the proof assistant Isabelle/HOL., 5th International Workshop on Confluence

We present a Haskell library for first-order term rewriting covering basic operations on positions, terms, contexts, substitutions and rewrite rules. This effort is motivated by the increasing number of term rewriting tools that are written in Haskell., 1st International Workshop on Haskell And Rewriting Techniques, HART 2013, 6 pages

We present the HOLCF-Prelude, a formalization of a large part of Haskell's standard prelude in Isabelle/HOLCF. Applying this formalization to the hints suggested by HLint allows us to certify them formally., 1st International Workshop on Haskell And Rewriting Techniques, HART 2013, 5 pages

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., pages 6, International Workshop on Confluence 2012

Since the first termination competition in 2004 it is of great interest, whether a proof that has been automatically generated by a termination tool, is indeed correct. The increasing number of termination proving techniques as well as the increasing complexity of generated proofs (e.g., combinations of several techniques, exhaustive labelings, tree automata, etc.), make certifying (i.e., checking the correctness of) such proofs more and more tedious for humans. Hence the interest in automated certification of termination proofs. This led to the general approach of using proof assistants (like Coq and Isabelle) for certification. We present the latest developments for IsaFoR/CeTA (version 1.03) which is the certifier CeTA, based on the Isabelle/HOL formalization of rewriting IsaFoR., 4 pages, International Workshop on Termination 2009

We present a locale that abstracts over the necessary ingredients for constructing a minimal bad sequence, as required in classical proofs of Higman's lemma and Kruskal's tree theorem., 7 pages, Isabelle Users Workshop 2012

In this paper we generalize the DP framework to a relative DP framework, where a so called split is possible., 5 pages, International Workshop on Termination 2012

There are termination proofs that are produced by termination tools for which certifiers are not powerful enough. However, a similar situation also occurs in the other direction. We have formalized termination techniques in a more general setting as they have been introduced. Hence, we can certify proofs using techniques that no termination tool supports so far. In this paper we shortly present two of these formalizations: Polynomial orders with negative constants and Arctic termination., 5 pages, International Workshop on Termination 2010

This is a beginner-oriented introduction to Isabelle/jEdit, the main user interface for the proof assistant Isabelle., Comment: 5 pages, Isabelle Users Workshop 2012 (updated in 2019)