D. Hendriks

Publication List Details

Period

1998 - 2009

Number

8

Co-Authors

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...

Proof reflection in Coq (2001)

Hendriks, D.

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...

Clausification in Coq (1998)

Bezem, M.A., Hendriks, D.

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...