Logic Calculators

Last modified 3 February 2014


What is a Logic Calculator?

Symbolic logic lies at the heart of reasoning about systems. It is to specification and verification what arithmetic is to most fields of science and engineering. Engineers do arithmetic with the help of calculators, but we don't provide them with any comparable tools for logic.

I would like to remedy this lack. My goal is a collection of web pages that provide simple logic calculators. The user types a formula into the calculator, presses a button, and is told if the formula is valid. If it isn't valid, the calculator provides a counterexample.

A logic calculator is not a theorem prover. It is a tool that is as easy to use as an ordinary pocket calculator. Complete directions for using a calculator should be just a few lines long.

A logic calculator should work reasonably fast on simple formulas. If the logic is undecidable, the calculator should work on most simple formulas. There should be a "Stop" button to terminate computations that take too long.

If you would like to implement a logic calculator, please send email to Leslie Lamport.


Existing Logic Calculators

Logic calculators are disappearing faster than I learn about them. The only ones I know of that still work are:
ProB Logic Calculator
This provides a convenient calculator for propositional logic. It can also check formulas of predicate logic and some other fields of math such as set theory, but only on explicit finite examples. It does not satisfy my criteria for a predicate-logic calculator.

somerby.net/mack/logic
Handles propositional and (somewhat restricted) predicate logic.

Related Work

The TLA+ Toolbox.
The Toolbox does not fit the definition of a calculator because it is not as easy to use as a pocket calculator. However, once you learn how to use it, it provides a general mathematics calculator that will evaluate any mathematical formula that can be naively evaluated in a finite number of steps. (For example, it can't evaluate quantification over an infinite set or unbounded quantification.)

SVC Demo Page
SVC ( The Stanford Validity Checker) claims to be "a research tool to check the validity of formulas expressed in a subset of first-order logic." However, the page describing its syntax doesn't mention quantifiers. Moreover, the syntax is not something that a human being would want to read or write. But, you can use it over the web.



This page can be found by searching the Web for the 32-letter string uidlamportlogiccalculatorproject. Please do not put this string in any document that could wind up on the web--including email messages and Postscript and Word documents. You can refer to it in Web documents as "the string obtained by removing the - from uid-lamportlogiccalculatorproject".