Geo
Geo
is a theorem prover, based on geometric resolution. The calculus
is described in a joint IJCAR 2006 paper with Jia Meng. You can also
download it here
here
under 2006.
(I am working on a new version,
that uses 3valued logic.
Checker for Partical Classical Logic
A
simple checker
,
which checks reasoning rules and equivalences for the two sequent
calculi for PCL. It works by exhaustively enumerating all possible
truth assignments.
Simple Proof Checker
The proof checker is able to check natural deduction proofs using
an arbitrary firstorder theorem prover. The theorem prover can
be selected through the first parameter. The proof to be checked is given
in the second parameter. For each step in the proof, the proof checker
creates an input file (in TPTP), and sends it to the theorem prover.
The tool supports a weak form of higherorder logic.
The program can be downloaded from
Piotr Witkowski's homepage
.
Parser Generation
Maphoon is an LALRparser
generator that I wrote in 1989 when I was a student.
The parser of Bliksem is generated by Maphoon.
(But Bliksem can also be compiled without it.)
This version of Maphoon obsolete and there is no reason to download it,
unless you still use Bliksem.
This is maphoon2008b.
It is a parser generator written in C++. It generates a
bottom up (LALR) parser in C++.
It features are:

True support of C++ and objectoriented programming style.
Since nearly every C program is also
a C++ program, every parser generator that can generate C programs,
can also generate C++ programs.
But in this way, the advantages of C++ cannot be used in the
parser. Maphoon treats tokens as true C++objects. The
user does not have to worry about allocation and deallocation
of objects, and there is no need to deal with polymorphism
through pointer casts.
The parser is generated in a namespace that the user can
specify. This may be useful in big projects that need several
parsers.

Run time definition of operators. If one wants to be able
to define infix/postfix/binary operators at run time,
one needs a mechanism for deciding shift/reduce conflicts at run time.
In maphoon, this mechanism is provided by allowing reductions to
refuse. If there is a shift/reduce conflict, the parser will first
try to reduce. If the reduction refuses, the parser will shift.
The reduction can look at the table of defined operators and their
priorities, when making its decision.
In this way, operators can be defined at run time.
The package contains C++ sources, a few examples, and a .pdf manual.
(Feb 2010)
Bliksem
Bliksem
is a resolutionbased theorem prover, written in C.
It was mostly written in 19981999. By now it has become pretty
outdated, but it seems that people are still using it,
so it stays on the web.
Encryption with Rijndael
An implementation of the Rijndaelencryption
scheme in C++. The user interface is primitive.
The program asks whether you want to decrypt or encrypt, after
that it asks for a key.
If you want to encrypt it reasks for the key.
Finally, it asks for an inputfile and an outputfile.
It encrypts about 1Mbyte/second on an 800Mhz Pentium.
Note that
Rijndael is a block cypher. As a consequence, repetitions in the input,
may cause repetitions in the output. If you don't want that, you could
compress the input before encrypting.
WARNING! If you encrypt a file and forget the key, then
the file is gone.
The algorithm is based on the description of
Rijndael in Joan Daemen, Vincent Rijmen, The Design of Rijndael, Springer
Verlag, 2002.
Compute SunsetSunrise Times
Here is a Cprogram that computes sunset/sunrise times.
The interface is primitive, but the times are accurate up to the minute.
Download.