Implementation of Beyond Lisp

Currently I am trying to implement the idea that I have which is outlined at Beyond-lisp-notes . Basically I will add the mu special form to the scheme language. This will take a formal logic expression and see if it holds true for a computer program. The syntax we will use is an automated theorm prover in first order logic. I am also thinking of adding mu-let which would take a set of mu statements and prove if they hold true given a set of data.

Requirements

The software package will require gandalf to be compiled on your unix machine. There is a windows binary that I will make available for windows computers. It will also require scsh because I am programing the program in that scheme environment. The Gandalf package is independant of implementation since it creates its own binaries.

Scsh
Gandalf