A Relative Dependency Pair Framework
In this paper we generalize the DP framework to a relative DP framework, where a so called split is possible.
Researcher profile
René Thiemann
René Thiemann contributes to research discovery and scholarly infrastructure.
ResearcherAffiliation not importedOpen to collaborate
Trust snapshot
Quick read
Trust 21 - EmergingVerification L1Unclaimed author
7works
0followers
3topics
4close collaborators
Actions
Decide how to stay connected
Identity and collaboration
How to connect with this researcher
Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.
Log in to claimDirect collaboration
Open a focused conversation when the fit is right
Claim this author entity first to unlock direct invitations.
Research graph
See the researcher in context
Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.
Building this graph slice
BZPEER is loading the nearby papers, people, topics and institutions for this page.
Published work
7 published item(s)
preprint2012arXiv
Certification extends Termination Techniques
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.
0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv
CeTA - A Tool for Certified Termination Analysis
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.
0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv
Recording Completion for Finding and Certifying Proofs in Equational Logic
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.
0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv
Towards the Certification of Complexity Proofs
We report on our formalization of matrix-interpretation in Isabelle/HOL. Matrices are required to certify termination proofs and we wish to utilize them for complexity proofs, too. For the latter aim, only basic methods have already been integrated, and we discuss some upcoming problems which arise when formalizing more complicated results on matrix-interpretations, which are based on Cayley-Hamilton's theorem or joint-spectral radius theory.
0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv
Automated Termination Analysis for Logic Programs with Cut
Termination is an important and well-studied property for logic programs. However, almost all approaches for automated termination analysis focus on definite logic programs, whereas real-world Prolog programs typically use the cut operator. We introduce a novel pre-processing method which automatically transforms Prolog programs into logic programs without cuts, where termination of the cut-free program implies termination of the original program. Hence after this pre-processing, any technique for proving termination of definite logic programs can be applied. We implemented this pre-processing in our termination prover AProVE and evaluated it successfully with extensive experiments.
0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv
Loops under Strategies ... Continued
While there are many approaches for automatically proving termination of term rewrite systems, up to now there exist only few techniques to disprove their termination automatically. Almost all of these techniques try to find loops, where the existence of a loop implies non-termination of the rewrite system. However, most programming languages use specific evaluation strategies, whereas loop detection techniques usually do not take strategies into account. So even if a rewrite system has a loop, it may still be terminating under certain strategies. Therefore, our goal is to develop decision procedures which can determine whether a given loop is also a loop under the respective evaluation strategy. In earlier work, such procedures were presented for the strategies of innermost, outermost, and context-sensitive evaluation. In the current paper, we build upon this work and develop such decision procedures for important strategies like leftmost-innermost, leftmost-outermost, (max-)parallel-innermost, (max-)parallel-outermost, and forbidden patterns (which generalize innermost, outermost, and context-sensitive strategies). In this way, we obtain the first approach to disprove termination under these strategies automatically.
0 citations0 reviewsNo code linkedOpen access