Bliksem

Bliksem is a first-order, resolution based theorem prover, which is written in C. It has grown out of a series of benchmark tests that I carried out in december 1998. The benchmark tests compared various datastructures for representating terms, using the operations of unification and matching. The main outcome of these tests was that the most common datastructure (deep terms with arguments lists which are used in E, Spass and Otter) can sometimes be dramatically slower (app. 5 times) than flatterms. Flatterms are not harder to implement than deep terms with argument lists and use less memory. In that time, there existed only one prover using flatterms (Waldmeister), and this prover could handle only unit equality. Therefore it seemed a good idea to implement a full first-order prover using flatterms.

If you are still using bliksem

then you are probably a linguist. I recently found out that linguists are still using Bliksem, mainly due to the book 'Representation and Inference for Natural Language' by Patrick Blackburn and Johan Bos. Probably I will make some updates of Bliksem, and remove its most obvious demerits.

Downloading Bliksem

Download the sources here .
Read the manual here .
Read the log here .
The picture of bliksem attacking a problem is still there .

In order to compile bliksem, type 'make' and hold your breath. (on my computer, it takes only 10 seconds to compile) If make starts complaining about maphoon, type 'touch inoutput.c', and try again.

The Benchmark Tests

If you intend to implement a theorem prover, it is still a good idea to have a look at the banchmarks.

View the benchmarks in pdf or ps.gz .

Total Proofs

Proofs from Bliksem can be converted into typetheory and checked by Coq. See the details here .