Logic Calculators

What is a Logic Calculator?

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

• ptl: propositional temporal logic (PTL) tautology checker

  This is a very nice logic calculator for propositional linear-time temporal logic. All it lacks is a good, concise description of how to use it.

• STeP's propositional temporal validity checker

  This isn't exactly a logic calculator. (For one thing, it requires variable declarations, something you don't have to do on your typical pocket calculator.) It can check propositional formulas in Manna-Pnueli logic--a rich linear-time temporal logic described in

  Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Volume 1 (Specification). Springer-Verlag. 1992. ISBN 0-387-97664-7.

  Unfortunately, this page is not maintained and no longer works.

Related Work

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