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.
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.
Download the sources
Read the manual
Read the log
The picture of bliksem attacking a problem is
still there .
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
Proofs from Bliksem can be converted into typetheory
and checked by Coq.
See the details