From Abstract Rewriting Systems to Abstract Proof Systems (2009)
Some personal recollections on the introduction of `abstract proof systems' as a framework for formulating syntax-independent, general results about rule derivability and admissibility. With a...
Unique Normal Forms in Infinitary Weakly Orthogonal Term Rewriting (2009)
Endrullis, Joerg, Grabmayer, Clemens, Hendriks, Dimitri, Klop, Jan Willem
The theory of finite and infinitary term rewriting is extensively developed for orthogonal rewrite systems, but to a lesser degree for weakly orthogonal rewrite systems. In this note we present some...
On the termination of Russel's description elimination algorithm (2009)
Grabmayer, Clemens, Leo, Joop, Oostrom, Vincent Van, Visser, Albert
In this paper we study the termination behaviour of Russell’s description elimination rewrite system. We discuss certain claims made by Saul Kripke in his paper.
Complexity of Fractran and Productivity (2009)
Endrullis, Joerg, Grabmayer, Clemens, Hendriks, Dimitri
In functional programming languages the use of infinite structures is common practice. For total correctness of programs dealing with infinite structures one must guarantee that every finite part of...
VRIJE UNIVERSITEIT Relating Proof Systems for Recursive Types (2008)
Typeset L Atexe, Clemens Grabmayer, Academisch Proefschrift, Clemens Armin Grabmayer, Geboren Te Linz
ter verkrijging van de graad van doctor aan de Vrije Universiteit Amsterdam, op gezag van de rector magnificus prof.dr. T. Sminia, in het openbaar te verdedigen ten overstaan van de promotiecommissie...
Productivity of stream definitions (2008)
Endrullis, Jörg, Grabmayer, Clemens, Hendriks, D., Isihara, Ariya, Klop, J.W.
We give an algorithm for deciding productivity of a large and natural class of recursive stream definitions. A stream definition is called ‘productive’ if it can be evaluated continually in such...
Data-Oblivious Stream Productivity (2008)
Endrullis, Joerg, Grabmayer, Clemens, Hendriks, Dimitri
We are concerned with demonstrating productivity of specifications of infinite streams of data, based on orthogonal rewrite rules. In general, this property is undecidable, but for restricted formats...
Using proofs by coinduction to find “traditional” proofs (2008)
Abstract. In the specific situation of formal reasoning concerned with “regular expression equivalence ” we address instances of more general questions such as: how can coinductive argumentation...
Using proofs by coinduction to find “traditional” proofs (2008)
• A finitary coinduction principle for regular expression equivalence. • A coinductively motivated proof system cREG0 for reg.expr.equiv. • An effective proof-theoretic transformation from the...
Some Remarks on Definability of Process Graphs (2008)
Clemens Grabmayer, Jan Willem Klop, Bas Luttik, Cwi Amsterdam
Abstract. We propose the notions of “density ” and “connectivity ” of infinite process graphs and investigate them in the context of the wellknown process algebras BPA and BPP. For a process...
Productivity of Stream Definitions (2007)
Endrullis, Jörg, Grabmayer, Clemens, Hendriks, Dimitri, Isihara, Ariya, Klop, Jan
We give an algorithm for deciding productivity of a large and natural class of recursive stream definitions. A stream definition is called ‘productive’ if it can be evaluated continuously in such...
Productivity of Stream Definitions (2007)
Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Ariya Isihara
We give an algorithm for deciding productivity of a large and natural class of recursive stream definitions. A stream definition is called ‘productive ’ if it can be evaluated continually in such...
Reflections on a Geometry of Processes (2005)
Clemens Grabmayer, Jan Willem, Klop Bas Luttik
In this note we discuss some issues concerning a geometric approach to process algebra. We mainly raise questions and are not yet able to present significant answers. 1 Periodic Processes Our point...
Derivability and Admissibility of Inference Rules in Abstract Hilbert Systems (2003)
Abstract. We give an overview of results, presented in the form of a poster at CSL03/KGC, about a general study of the notions of rule derivability and admissibility in Hilbert-style proof systems....
) Clemens Grabmayer Master's Thesis at the Institute for Logic, Language and Computation (ILLC), Universiteit van Amsterdam, October 1999 This thesis consists of two chapters, the rst of which...