Propositional logic (or propositional calculus) is, according to Wikipedia, “a branch of mathematical logic concerned with the study of propositions (whether they are true or false) that are formed by other propositions with the use of logical connectives, and how their value depends on the truth value of their components.”

I was introduced to this topic during my third-year of college in a course titled Introduction to Formal Logic. I did not have high expectations going in (my primary motivation was avoiding more writing-intensive electives), but it turned out to be one of my favorite courses. One aspect that I found particularly intriguing about the course was that much of the material seemed to lend itself nicely to automation—whether it be the construction of truth tables or even the analysis of proofs. Indeed, there are a number of existing online tools such as:

• The Logic Daemon by Texas A&M University, which “checks proofs and can provide hints for students attempting to construct proofs in a natural deduction system for sentential (propositional) and first-order predicate (quantifier) logic”;

• truth table generators by Michael Rieppel, Jamie Wong or Lawrence Turner (among others); and

• the various utilities developed by Logictools.

I intend to re-implement (and, where possible, try to improve upon) much of the functionality mentioned above with the goals of gaining a more thorough understanding of the topic and releasing a full-featured, open-source library named Tombstone.js (if you’re wondering why I chose the name “Tombstone,” it was inspired by the typographical symbol).

## Evaluating Well-Formed Formulas#

The first step was to implement the ability to evaluate arbitrary well-formed formulas (WFFs). This requires a definition of our vocabulary, which consists of sentence variables ($\{A,B, \dots, Z\}$), parentheses and connectives.

Logical Connectives (descending order of precedence)
SymbolNameExample
~negation~P ("not P")
&conjunctionP & Q ("P and Q")
||disjunctionP || Q ("P or Q")
->implicationP -> Q ("If P, then Q")
<->equivalenceP <-> Q ("P if and only if Q")

A formula is considered well-formed according to the following conditions:

1. All sentence variables are WFFs.

2. If $\phi$ is a WFF, then ~$\phi$ is also a WFF.

3. If $\phi$ and $\psi$ are WFFs, then ($\phi$ & $\psi$), ($\phi$ || $\psi$), ($\phi$ -> $\psi$) and ($\phi$ <-> $\psi$) are WFFs.

4. Nothing else is a WFF.

From here, I decided to use the shunting-yard algorithm to convert WFFs to Reverse Polish notation (RPN) for evaluation. In RPN, every operator follows its operands—for example, P & Q becomes P Q &. This parsing strategy is more commonly associated with mathematical expressions but it seems to work well for logic too. You can see the algorithm in action below.

Once in RPN, we can easily evaluate the expression or construct a graphical representation of the formula’s structure (known as a parse tree) as seen below.

## Truth Tables#

Now that we can evaluate arbitrary WFFs, generating truth tables is just a matter of evaluating an expression at all of its variable combinations.

## Conclusion#

While Tombstone.js is still in its early stages of development, I think this is a promising start. An approximate roadmap for future development is as follows.

• Extend truth table generation to allow for copying in HTML, Markdown, $\LaTeX$, reStructuredText or plain text;

• add the ability to analyze proofs; and

• create a website to showcase Tombstone.js.

I am also considering re-writing the project (that is, the two files it currently contains) in TypeScript. This seems like it would offer a number of interesting features without sacrificing browser support, which is something I would like to keep as high as possible.

## References#

• Allen, Colin and Michael Hand. Logic Primer. Cambridge, Mass.: MIT Press, 2001. Print.