TY - RPRT

T1 - Geometric Operators on Boolean Functions

AU - Frisvad, Jeppe Revall

AU - Falster, Peter

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

KW - array-based logic, Boolean functions, geometric operators, inference, propositional reasoning.

M3 - Report

T3 - D T U Compute. Technical Report

BT - Geometric Operators on Boolean Functions

PB - Informatics and Mathematical Modelling, Technical University of Denmark, DTU

CY - Richard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby

ER -