A Theorem Prover for First-Order Logic (Predicate Calculus)

What follows is a Java applet that allows you to enter a logical “theory” (a set of axioms, definitions, and theorems) in a first-order logic language that supports types and other goodies. You then ask the applet to prove the theorems. It will fail to prove them if there is no proof, or one cannot be found. Read the information below the applet window to learn more about the logic language used.

Information about the logic language used

The text that you enter in the large black rectangle on the left side of the applet must be written in this theorem prover’s language. The language allows you to express a logical theory in 1st-order logic (predicate calculus). The best way to learn about the features of the language is to open one by one the sample files shown in a list when you click on the “open file” button (). The files document through their comments which features are included in the language. For a brief overview of such features, please take a look at the following list:

The language supports full first-order logic expressions (“well-formed formulas”), including universal and existential quantifiers. The keyboard characters used for representing logical symbols are the following:

~ : “not”
&: “and”
v : “or”
-> : “implies”
<--> : “if and only if”
@ : “for all” (universal quantifier)
#  : “there exists” (existential quantifier)

The language supports types for logical objects, such as variables, constants, and functions (or “functors” as they are often called in logic). Thus, for instance, when a variable x is declared, it can be optionally given a type, as follows:

Types

person;

Variables

x : person;

Types allow for the simplification of the expressed logical theory, without losing in derivational power. Without types, the previous type “person” would have to be expressed though a predicate, such as person(x). With types, such predicates of a single parameter become redundant, thus simplifying logical formulas.

The language supports a hierarchy of types, in which one type can be a subtype of another type. For example:

Types

person < mammal < living_being;
chimp < mammal;
plant < living_being;

Thus, an entire hierarchy tree can be specified. All types are assumed to be subtypes of the special and known type Entity, which needs no declaration. When objects of given types are unified, the object of a subtype can substitute a variable of any of its supertypes, but not vice-versa. For example, IsRunning(x) can be unified with IsRunning(John) if IsRunning has been declared as a predicate expecting parameters of type mammal (see the previous hierarchy of types), and John is a constant of type person. In the unification, John will substitute x, because person < mammal. However, an object of type plant cannot substitute the variable x of IsRunning, because plant is not a subtype of mammal.

The special predicate is (x, type) is provided for use with types, where x is any well-formed expression, and type is one of the declared types. This predicate evaluates to true if and only if the type of x is either type, or it is a subtype of type.

Types are of course optional. They are included only for the user’s convenience.

The overall syntax of the language allows an initial declaration of Types, Constants, Variables, Functions, and Predicates (in that order, but each is optional), followed by any sections of Axioms, Definitions, and Theorems (in any order). More Axioms may then follow the Theorems, followed by further sets of Axioms, Definitions, and Theorems, in any order, without limitation. The applet includes buttons on its tool-bar at the top that allow the user to step through the theory either:

one theorem at a time (button ), or
an entire set of theorems at a time (button ), or
proving all theorems up to the end (button ).

The user can interrupt the proving process at any time (button ), modify the theory by editing it, or start over (button ).

The syntax allows the user to choose extreme simplification, ending up with expressions of Propositional Calculus form (such as P -> Q, etc), or full adherence to the declared types, in which case type-checking is strict and enforced. It is up to the user to choose either strict or free syntactic conventions.

Information about features of the theorem prover

The theorem prover can be used to examine the consistency of the given axioms (and/or definitions) instead of proving any theorem. It does this if the last section(s) of the theory include only axioms and/or definitions, but no theorems to be proved. As it follows from the theory of first-order logic, if the theory is consistent, the search for inconsistency might not terminate. If, however, the theory is incosistent, the inconsistency will be found and shown in the output (blue) window, on the right.

As it follows from the theory of first-order logic, if a theorem has a proof, the proof will be found by this theorem prover, and shown on the output (blue) window, on the right. But if a theorem has no proof, then the theorem prover might enter a search without end, in which case the user should interrupt the prover by using the stop button (). In that case, neither the user nor the theorem prover know if a proof really does not exist, or a proof would be found if only the prover were allowed to continue searching a bit more. But note that for many of the simple theories the prover can conclude that there is no proof after searching the proof-space exhaustively. In that case, it will terminate and announce the lack of proof.

Internally, the theorem prover converts all propositions of axioms and/or definitions into “disjunctive normal form” (applying elimination of universal quantifiers and Skolemization of existential quantifiers), and places all the resultant clauses in a “search space”. It also converts the negation of the theorem to be proved into disjunctive normal form, and adds it to the search space. Subsequently, it applies the resolution method, using the following heuristics:

the “set of support” strategy (the restriction that at least one of the resolved clauses must come from the negated theorem or its derivative clauses; it can be proven that this restriction is complete, i.e., does not miss any proof),
the “unit preference” heuristic (the heuristic according to which proofs are found faster if, in selecting which clauses to resolve, preference is given to clauses with a single literal (if any),
and the “smaller clauses preference” heuristic (sorting the clauses in search space in ascending order of length), which is a generalization of the previous heuristic.

The logic language used in this theorem prover is one that was proposed in the author’s Master’s thesis, back in 1985–1987, at which time it contained most of the features shown here, including the hierarchical type scheme. Back then, the idea of logic languages with types was novel. (There was the untyped logic language Prolog, and the strongly typed — but general programming language — Pascal.) The author’s M.S. thesis project was converted into this applet in May–August 2010, purely for fun.

Some computer screens are quite compact. If the applet rectangle shown at the top of this page doesn’t fit in your screen, you have two options. One is to see if the smaller (shorter) rectangle, below, still fits. And another is to set your browser in full-screen mode. In Internet Explorer this is done as follows: if you don’t already see the menu bar at the top (saying File, Edit, View, Favorites, Tools, Help), you can make it appear by hitting the Alt key on PC’s. Then click on View, and then on Full Screen (at the bottom of the list). (The same effect can be achieved by hitting the F11 key.) Then the entire screen is used for the contents of your window. You may exit the full-screen mode by moving the cursor near the top of the screen; a bar will appear at the top-portion of the screen, on which you can click the “restore” button, on the upper-right corner.

Here is the applet in a shorter window:

While calculus is used in many fields including economics and statistics, it would not be required study for an accounting position at a loan company like Titlemax. Lower math operations and algebra are necessary for a Titlemax accounting job but calculus is not required.