Let's Make a Difference! (2009)
Endrullis, Joerg, Hendriks, Dimitri, Klop, Jan Willem
We study the behaviour of iterations of the difference operator delta on streams over {0,1}. In particular, we show that a stream sigma is eventually periodic if and only if the sequence of...
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...
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...
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...
Automated Proof Construction in Type Theory using Resolution † (2008)
Jean Marie, Guillaume Gérard Nivelle, Sonstige Wissenschaftliche Arbeiten, Marc Bezem, Dimitri Hendriks
Dieser Band enthält die sonstigen wissenschaftliche Arbeiten, die ich zusammen mit meiner Habilitationsschrift einreiche. Die ersten vier Arbeiten beschäftigen sich mit Beweiserzeugung durch...
On the Mechanization of the Proof of Hessenberg’s Theorem in Coherent Logic (2007)
Bezem, Marc, Hendriks, Dimitri
We propose to combine interactive proof construction with proof automation for a fragment of first-order logic called Coherent Logic (CL). CL allows enough existential quantification to make...
Clausification is an essential step in the so-called resolution method, one of the most successful procedures for automated theorem proving. Anticipating the use of resolution in proof construction...
Nieuwsbrief van de Nederlandse Vereniging voor Theoretische Informatica (2007)
Mieke Brune, Jan Willem Klop, Jan Rutten (eds.), Van De Redactie, Samenstelling Bestuur, ...
s van voordrachten On Notions of bisimulation and associated logics Prof.dr. M. Nielsen BRICS, Computer Science Department, University of Aarhus Recently, there have been several attempts of abstract...
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...
Automated Proof Construction in Type Theory using Resolution (2002)
Bezem,Marc, Hendriks,Dimitri, De Nivelle,Hans
We provide techniques to integrate resolution logic with equality in type theory. The results may be rendered as follows: {\bf (1)}. A clausification procedure in type theory, equipped with a...
Automated Proof Construction in Type Theory using Resolution (2002)
Bezem, Marc, Hendriks, Dimitri, De Nivelle, Hans
We provide techniques to integrate resolution logic with equality in type theory. The results may be rendered as follows: {\bf (1)}. A clausification procedure in type theory, equipped with a...
Nivelle. Automated proof construction in type theory using resolution (2002)
Abstract. We provide techniques to integrate resolution logic with equality in type theory. The results may be rendered as follows. − A clausification procedure in type theory, equipped with a...
Proof reflection in Coq (2002)
Abstract. We formalise natural deduction for first-order logic in the proof assistant Coq, using de Bruijn indices for variable binding. The main judgement we model is of the form Γ ⊢ d [:] φ,...
Nivelle. Automated proof construction in type theory using resolution (2002)
Marc Bezem, Dimitri Hendriks, Hans De Nivelle
Abstract. We provide techniques to integrate resolution logic with equality in type theory. The results may be rendered as follows. { A clausication procedure in type theory, equipped with a...
Proof reflection in Coq (2002)
We formalise natural deduction for first-order logic in the proof assistant Coq, using De Bruijn indices for variable binding. The main judgement we model is of the form Γ ⊢ d [:] φ, stating that...
Proof reflection in Coq (2002)
We formalise natural deduction for first-order logic in the proof assistant Coq, using De Bruijn indices for variable binding. The main judgement we model is of the form Γ ⊢ d [:] φ, stating that...
Proof reflection in Coq (2002)
We formalise natural deduction for first-order logic in the proof assistant Coq, using De Bruijn indices for variable binding. The main judgement we model is of the form # d [:] #, stating that d is...