Propositional logic deals with the connectives
`¬`

(negation),
`∧`

(conjunction),
`∨`

(disjunction),
`⇒`

(implication),
and `⇔`

(equivalence).

The language of propositional logic contains the following symbols:

- infinitely many variables,
- the connectives
`¬`

,`∧`

,`∨`

,`⇒`

,`⇔`

, and - parentheses
`(`

,`)`

.

The set of propositional logic formulas, F, is the smallest one satisfying

- for all
`X`

such that`X`

is a variable then`X`

∈ F, - for all
`φ`

and`ψ`

, if`φ`

and`ψ`

∈ F, then`¬φ`

∈ F,`φ∧ψ`

∈ F,`φ∨ψ`

∈ F,`φ⇒ψ`

∈ F, and`φ⇔ψ`

∈ F, - for all
`φ`

such that`φ`

∈ F then`(φ)`

∈ F.

We can also use the constants `t`

, or `⊤`

, for true, and
`f`

, or `⊥`

, for false and have these as propositional formulas but
not all authors use them.

The meaning of a connective is given by its truth table.
These truth tables in combination with a
truth assignment allow us to assign a truth value (`t`

or `f`

)
to a formula.

A truth assignment, `γ`

*satisfies* a formula `φ`

,
written `γ⊨φ`

, if `φ`

evaluates to `t`

using `γ`

.
A formula `φ`

is *satisfiable* if there is some truth assignment `γ`

such that `γ⊨φ`

.

A truth assignment, `γ`

*satisfies* a set of formulas `Γ`

,
written `γ⊨Γ`

,
if `γ`

satisfies every member of `Γ`

.

A formula `φ`

is *logically valid*, written `⊨φ`

, if `φ`

is satisfied by every truth assignment.

A formula `φ`

is a *logical consequence* of the set of formulas `Γ`

,
written `Γ⊨φ`

,
if `φ`

is satisfied by every truth assignment that satisfies `Γ`

.

The formulas `φ`

and `ψ`

are *equivalent*,
written `φ≡ψ`

if they are satisfied by the same
assignments.

The following is a Prolog implementation of the semantics of propositional logic. The code is specific to Barry's Prolog but should work on other Prolog implementations which provide association lists.

` ````
:- ensure_loaded(runtime(assoc)). % A library that supplies get_assoc/3
%%%
%%% The syntax of propositional logic
%%%
%%% I use the built in parser and change/augment the Prolog operators to handle
%%% propositional logic.
%%%
:-op(200, fy, ~). % Negation
:-op(0, yfx, (/\)).
:-op(400, xfy, (/\)). % Conjunction (not ISO associativity which is yfx)
:-op(0, yfx, (\/)).
:-op(500, xfy, (\/)). % Disjunction (not ISO associativity which is yfx)
:-op(600, xfy, ==>). % Implication
:-op(700, xfy, <=>). % Equivalence
%%%
%%% pl_eval_not(P, NotP).
%%%
%%% The samantics of the propositional logic negation connective.
%%%
pl_eval_not(true, false).
pl_eval_not(false, true).
%%%
%%% pl_eval_and(C1, C2, Conjunction)
%%%
%%% The semantics of the propositional logic conjunction.
%%%
pl_eval_and(true, true, X) :- !, X = true.
pl_eval_and(_, _, false).
%%%
%%% pl_eval_or(C1, C2, Disjunction)
%%%
%%% The semantics of the propositional logic disjunction.
%%%
pl_eval_or(false, false, X) :- !, X = false.
pl_eval_or(_, _, true).
%%%
%%% pl_eval(F, V, Answer)
%%%
%%% Using the valuation (truth assignment) V we evaluate the formula F to Answer (true, false).
%%% This is the mathematical definition of the semantics of propositional logic.
%%% An association list is used to implement the truth assignment.
%%%
%%% assoc_to_list(V, [p-true, q-false, r-true]), pl_eval((p /\ q ==> q \/ r), V, Answer).
%%% assoc_to_list(V, [p-true, q-true, r-false]), pl_eval((p /\ q ==> q /\ r), V, Answer).
%%%
pl_eval(false, _, false).
pl_eval(true, _, true).
pl_eval(Atom, V, Answer) :-
atom(Atom),
!,
get_assoc(Atom, V, Answer).
pl_eval(~Phi, V, Answer) :-
pl_eval(Phi, V, Temp),
pl_eval_not(Temp, Answer).
pl_eval(Phi /\ Psi, V, Answer) :-
pl_eval(Phi, V, T1),
pl_eval(Psi, V, T2),
pl_eval_and(T1, T2, Answer).
pl_eval(Phi \/ Psi, V, Answer) :-
pl_eval(Phi, V, T1),
pl_eval(Psi, V, T2),
pl_eval_or(T1, T2, Answer).
pl_eval(Phi ==> Psi, V, Answer) :-
pl_eval(~Phi \/ Psi, V, Answer).
pl_eval(Phi <=> Psi, V, true) :-
pl_eval(Phi, V, T1),
pl_eval(Psi, V, T2),
T1 == T2,
!.
pl_eval(_ <=> _, _, false).
```

Doets, Kees. *From Logic to Logic Programming.* MIT Press, 1994.

Harrison, John. *Handbook of Practical Logic and Automated Reasoning.* Cambridge, 2009.

Copyright © 2014, 2015 Barry Watson. All rights reserved.