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 predicatelogic
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 firstorder 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 32letter
string
uidlamportlogiccalculatorproject.
Please do not put this string in any document that could wind up on
the webincluding email messages and Postscript and Word documents.
You can refer to it in Web documents as "the string obtained by
removing the  from
uidlamportlogiccalculatorproject".