Lambda the Ultimate

A very short paper having pretty narrow applicability, but somehow it is exactly what I needed today for my programming. Go figure.

The concept of a propositional logic, PL, will be defined and a method, to be referred to as the Kleene Search Procedure, will be used to determine the validity of formulas of PL. This method utilizes a set of sequent rules which are derived in a purely mechanical fashion from the truth tables which are the intended interpretations of the connectives of PL. The results are then used to show how a formal system, GPL, which is a sequent calculus can be constructed with very simple axioms and these sequent rules to yield the valid formulas of PL

Note that there are two "mechanical" algorithms here - one deriving sequent rules from truth tables, and another deriving either a proof ar a refutation of a sequent.

I wonder just how deeply this is related to both Qi and the map coloring theorem proof (didn't read any of those threads carefully yet).