Propositional logic as a programming language

October 2009

This project aims to reconstruct the computability concept in terms of propositional algebras. Features of this approach:

The primitive operations, i.e. the whole underlying "virtual machine" is only made of the operations of propositional logic, and this system is effectively implemented [2]. However, it requires a paradigm shift in the reasoning about programming itself. Propositional logic as a whole is a NP-hard problem. And now, we propose our propositional logic system as the primitive base for a more complex programming language. This upside-down perspective has two justifications: our first goal was to show that our propositional machines we want to explore in the formal intelligence project can be run as Turing complete devices. In other words, we just required a mathematical proof that the computability concept is equivalently definable in propositional algebra. The second justification is very pragmatic: just let us see if actual programs run fast enough on a temporary computer system to be practical. Computer power nowadays is so inexpensive, that this practical proof is the only real issue in most cases.

The whole project is only rudimentary realized so far. Many encoding problems are solved and according algorithms are implemented in a Haskell package. But all that is too premature to be published.

Links and footnotes

[home] [blog]