Extensionality of Simply Typed Logic Programs (1999)
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
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...
Diagram Techniques for Confluence (1996)
Bezem, M.A., Klop, J.W., Oostrom, V. Van
We develop diagram techniques for proving confluence in abstract reductions systems. The underlying theory gives a systematic and uniform framework in which a number of known results, widely...
Generalizing Hamming distance to finite sets (1996)
We propose a distance measure to compare objects that have heterogeneous sets of characteristics, such as encountered in, for example, medical diagnosis and genetic programming.
On the computational content of the Axiom of Choice (1994)
Berardi, S., Bezem, M.A., Coquand, T.
We present a possible computational content of the negative translation of classical analysis with the Axiom of Choice. Our interpretation seems computationally more direct than the one based on...
Proving a graph well founded using resolution (1994)
Using the resolution theorem prover OTTER we prove that a certain directed graph has no infinite path. We argue that this technique complements the well known combinatorial algorithms in cases in...
A Correctness Proof of a One-bit Sliding Window Protocol in μCRL (1994)
ION The most substantial step in the correctness proof of the one-bit sliding window protocol is provided by the following lemma. It states, roughly, that the partial abstraction ø føc ;ø c 2 ;ø...
A Correctness Proof of a One-bit Sliding Window Protocol in {micro}CRL (1994)
We model a one-bit sliding window protocol and prove that its external behaviour is a bi-directional buffer of capacity 2. The proof is given in μCRL, which is a process algebra extended with data....
A Correctness Proof of a One-bit Sliding Window Protocol in μCRL (1993)
We model a one-bit sliding window protocol and prove that its external behaviour is a bi-directional buffer of capacity 2. The proof is given in μCRL, which is a process algebra extended with data....
Invariants in Process Algebra with Data (1993)
We provide rules for calculating with invariants in process algebra with data, and illustrate these with examples. The new rules turn out to be equivalent to the well known Recursive Specification...
A Formal Verification of the Alternating Bit Protocol in the Calculus of Constructions (1993)
We report on a formal verification of the Alternating Bit Protocol (ABP) in the Calculus of Constructions. We outline a semi-formal correctness proof of the ABP with sufficient detail to be...
Bar recursion versus polymorphism (1992)
By constructing a counter, model we show that a certain appealing equation E has no solution in Girard's [1972] second order lambdacalculus (the so-called polymorphic, lambda calculus). The equation...
Ramsey's theorem and the pigeonhole principle in intuitionistic mathematics (1992)
At first sight, the argument which F.P. Ramsey gave for (the infinite case of) his famous theorem from 1927, is hopelessly unconstructive. If suitably reformulated, the theorem is true...
Strong Termination of Logic Programs (1991)
We study a powerful class of logic programs which terminate for a large class of goals. Both classes are characterized in a natural way in terms of mappings from variable-free atoms to natural...