Many problems in propositional logic can be solved by evaluating the logical sentences — via truth tables, or a more efficient approach. Doing so on paper is a tedious and boring process, therefore, it would be very useful to use a computer to help solve these problems. Many tools for doing so are available on the Internet, but building one for ourselves is not difficult, and a very interesting project. Prolog is very well suited to this problem for two reasons: (1) it is a logic programming language, thus, logical statements can easily be expressed in it; (2) it has excellent support for metaprogramming, thus, the language can be extended to provide the notation we expect in mathematics. This article will describe the implementation of such a system — a literate program of sorts. For running the program, the complete code is provided on Github.
The program in this article is written in Prolog. You will need to install and set up a Prolog interpreter or compiler before proceeding. Because Prolog is defined by an ISO standard, any properly implemented Prolog will work. I recommend SWI-Prolog (Download), which is available for most platforms.
If you save your program in a file called
decider.pl, you can run it by typing
swipl -l decider.pl. This will open an interactive Prolog REPL, which will allow you to make queries to the program you're writing. Make sure to end all statements in Prolog with a dot (
halt. to quit Prolog.
Expressing Logical Connectives
Prolog's syntax is different from the usual mathematical notation:
, represents conjunction and
; disjunction. We define a few predicates to provide a more expected syntax. We do not need to define one for NOT because Prolog already has
and(P,Q) :- P, Q, !. or(P,Q) :- (P; Q), !.
! represents cut. Basically, it tells Prolog not to backtrack and look for alternative solutions to the goal (e.g.
and(t,t)). In Prolog, predicates are referred to as
arity, arity being the number of arguments to the predicate. For example,
not/1. I will use this notation in the rest of the article.
Now, we are able to express logical sentences, using function notation. For example,
True and False
It would be useful to be able to use TRUE and FALSE in our logical sentences. In Prolog,
fail are predicates that can perform these functions. For the sake of convenience, we provide
f as shorter alternatives.
t. f :- fail.
When a Prolog predicate is missing a body, it is assumed that the predicate is a fact — a statement of something that is true.
- Now, we are ready to test our program. Try typing
and(t,or(t,f)).. What do you get?
Tagged True and False values
For word problems, it is often useful to indicate what TRUE and FALSE represent. For example P being true may represent A is a knight. We provide some syntactical sugar for this, in the form of
t('A is a knight') or
f('Peter does not have a drivers license').
t(_). f(_) :- fail.
_ is used as a variable in Prolog, it denotes the anonymous variable. It means that we do not care what its value is — the statement is true regardless. You may have noticed that in Prolog you may define multiple predicates with the same name, but with different arities.
If you were to define two predicates with the same name and arity, you would actually be defining multiple clauses of the same predicate. Prolog will try each matching clause until one that is true for the input is found.
Using Prolog more efficiently
If you have correctly configured SWI-Prolog, powerful tools are available to you for editing, debugging and modelling Prolog programs. To edit the currently loaded file, you can simply type
edit.. A text editor will be opened, and the program will be reloaded once you are finished. You can jump to the definition of a specific predicate by typing
You can start the debugger by typing
gtrace. (GUI debugger) or
trace. (CLI debugger). As soon as you enter a statement, the debugger will open and you can analyze your program and see what steps it is taking.
- Try tracing
or(and(t,not(f)),f).to see how Prolog evaluates this expression.
Enabling infix syntax for logical connectives
It is rather awkward to write
and(t,or(t,f)). Instead, it would be much better if infix notation could be used instead, like
t and (t or f). Doing so in Prolog is very simple. All we must do is declare our logical connectives as new operators.
:- op(400,xf,not). :- op(500,xfx,and). :- op(500,xfx,or). :- op(600,xfx,implies). :- op(600,xfx,equiv).
op/3 directive has three arguments: the precedence, the behaviour and the name of the predicate to be made an operator. The precedence is straightforward: the operator with the smallest precedence value is evaluated first. The behaviour describes how the operator acts in relation to other terms.
f represents position of the functor (our operator) and
y are the other terms in the expression. The SWI-Prolog manual gives the formal definitions for
yshould be interpreted as "on this position a term with precedence lower or equal to the precedence of the functor should occur". For
xthe precedence of the argument must be strictly lower.
A complete description of the
op/3 directive and a listing of the operators built in to Prolog can be obtained by consulting the built-in help system, by typing
- Now, we can write expressions such as
f or not f.Try it.
- You will notice that I have chosen the behaviour for the operators poorly. What happens when you type
t and t and f? How could this be fixed?
- Interestingly, you will notice that the logical operators
/\are already listed in Prolog's operator table. What happens when you try to use them?
Defining logical operators for the connectives
Although Prolog reserves,
/\ to represent the logical connectives, it does not provide their definitions. While we could define predicates for these operators, I chose to use
^ instead to save typing. (This does produce a conflict with Prolog's built in
^ operator in some cases, unfortunately.) First, let's declare our new operators.
:- op(400,xf,~). :- op(500,xfx,^). :- op(500,xfx,v). :- op(600,xfx,=>). :- op(600,xfx,<=>).
So long as the
op/3 directive precedes the definition of the predicates, we can use infix notation in our definitions. Thus, to make these new operators aliases of the connectives we defined earlier, the following will work:
~P :- not P. P ^ Q :- P and Q. P v Q :- P or Q. P => Q :- P implies Q. P <=> Q :- P equiv Q.
- Try using the new operators to evaluate a logical sentence. Does it work?
Providing connectives for implication and equivalence
Up until now, we have not defined implication and equivalence. We can easily do so in terms of the other connectives:
P implies Q :- not P or Q. P equiv Q :- (P and Q) or (not P and not Q).
- Verify the function of implication operator by trying each possible value for
Notes on using the program we have so far
You can use Prolog's
, operator to combine multiple statements, either in Prolog syntax or in our logical notation. For example, you might want to do something like
P = t('A is a knight'), Q = t('B is a knight'), P <=> ~P ^ Q.