^{1} Image Analysis and Computer Graphics, Department of Informatics and Mathematical Modeling, Technical University of Denmark^{2} Department of Informatics and Mathematical Modeling, Technical University of Denmark^{3} Computer Science and Engineering, Department of Informatics and Mathematical Modeling, Technical University of Denmark^{4} Department of Applied Mathematics and Computer Science, Technical University of Denmark

Abstract:

In truth-functional propositional logic, any propositional formula represents a Boolean function (according to some valuation of the formula). We describe operators based on Decartes' concept of constructing coordinate systems, for translation of a propositional formula to the image of a Boolean function. With this image of a Boolean function corresponding to a propositional formula, we prove that the orthogonal projection operator leads to a theorem describing all rules of inference in propositional reasoning. In other words, we can capture all kinds of inference in propositional logic by means of a few geometric operators working on the images of Boolean functions. The operators we describe, arise from the niche area of array-based logic and have previously been tightly bound to an array-based representation of Boolean functions. We redefine the operators in an abstract form to make them independent of representation such that we no longer need to be much concerned with the form of the Boolean functions. Knowing that the operators can easily be implemented (as they have been in array-based logic), shows the advantage they give with respect to automated reasoning.