Chapter II Propositional Logic

Dr. Abdelhakim ZEROUAL

University of Batna 2
Faculty of Mathematics and Computer Science
Computer Engineering Common Core
Email : [Link]@univ-batna2.dz1
1.0 2025

Dr. Abdelhakim ZEROUAL

Attribution - NonCommercial : [Link]

Table of contents

Objectives 4
Introduction 5
I - Propositional Language 6
1. The alphabet ..............................................................................................................6
2. Propositional Formulas .............................................................................................6
3. Syntax Trees ...............................................................................................................7
4. Formalization .............................................................................................................7
II - Semantic 9
1. Interpretation ............................................................................................................9
2. Satisfiability .............................................................................................................11
3. Satisfiability of a set of formulas.............................................................................12
4. Tautology .................................................................................................................12
5. Logical consequence ...............................................................................................13
6. Substitution theorem ..............................................................................................14
7. Replacement theorem.............................................................................................14
8. Sematic Equivalence ...............................................................................................14
9. Complete set of connectives ...................................................................................15
10. Conjunctive and Disjunctive Normal Form ..........................................................15
III - The Deductive System (¬, ∧ )
18
1. Deduction.................................................................................................................18
2. Rules of Deduction...................................................................................................19
3. Strategy ....................................................................................................................20
4. Other deductive systems.........................................................................................21
IV - DEMONSTRATION THEORY 22
1. Resolution Principle ................................................................................................22
2. Resolution Algorithm...............................................................................................23
3. Strategies of Resolution ..........................................................................................24
Conclusion 25

2 Dr. Abdelhakim ZEROUAL

 Table of contents

Bibliography 26

1. [Link]

Dr. Abdelhakim ZEROUAL 3

Objectives

Understand the syntax and semantics of propositional logic:

Learn how formulas are constructed using logical symbols and how truth values are
assigned through interpretation.
Apply logical reasoning techniques:
Use truth tables, tautologies, and logical consequences to evaluate and manipulate logical
statements.
Master deductive systems and resolution methods:
Explore Gentzen's Natural Deduction rules, proof strategies, and the resolution algorithm for
validating logical formulas.
Translate natural language into formal logic:
Practice formalization to express real-world statements as logical formulas for analysis and
inference.

4 Dr. Abdelhakim ZEROUAL

Introduction

Chapter II introduces propositional logic as a foundational element of formal logic and mathematical
reasoning. It provides a systematic study of propositions, their syntactic structure, semantic
interpretation, and the process of formal deduction. The chapter progresses from defining the basic
components of propositional language to establishing logical equivalence, deduction systems, and
resolution methods for automated reasoning.

Dr. Abdelhakim ZEROUAL 5

Propositional Language I

1. Introduction
The propositional language is composed of formulas representing propositions. Like other languages, the
language of propositional logic is characterized by its syntax and semantics.

2. The alphabet

Definition

The alphabet is composed of the symbols of language. It includes:

A countable set of propositional variables. The letters of the Latin alphabet (a, b, c ...) should be
used, possibly indexed.
Logical connectors(¬, ∧, ∨, →, ↔). This list is not complete, it may change from one teacher to
another or from one university to another.
Auxiliary symbols.

3. Propositional Formulas
The writing rules specify how the symbols of the alphabet are assembled to form well-formed
expressions (or formulas) of the propositional language:
1. Any propositional variable is a formula.
2. If 𝛼 is a formula, ¬𝛼 or 𝑎 is a formula.
3. If 𝛼 and 𝛽 are formulas, (𝛼∧𝛽), (𝛼 ⋁ 𝛽), (𝛼⟶𝛽) and (𝛼↔𝛽) are also formulas.
4. An expression is only a formula if it is written according to rules 1, 2 and 3.

Example

1. p, q, r are propositional variables, therefore formulas.

2. (𝑝 ∧ 𝑞) is a formula.
3. 𝑝 → (𝑞 𝑟) isn’t a formula.

Connector priority
The connectors are applied in the following order:
(¬, ⋀, ⋁, →, ⟷)

6 Dr. Abdelhakim ZEROUAL

 Propositional Language

Example

1. ¬𝑝 ⋀ 𝑞 is read as (¬ 𝑝 ) ⋀ 𝑞
2. 𝑝 ⋀ 𝑞 ⟶ 𝑟 is read as ( 𝑝 ⋀ 𝑞 ) ⟶ 𝑟
3. 𝑝 ⋁ 𝑞 ⋀ 𝑟 is read as 𝑝 ⋁ ( 𝑞 ⋀ 𝑟 )
4. 𝑝 ⋁ 𝑞 ∨ 𝑟 is read as (𝑝 ⋁ 𝑞 ) ∨ 𝑟

4. Syntax Trees

Definition

A syntax tree is a graphical representation that illustrates the hierarchical structure of a formula.

Structure of a Syntax Tree

Root: Represents the main logical connective of the formula.
Internal Nodes: Represent the applied logical connectives.
Leaves: Represent the propositional variables (atomic propositions).

Example

For the formula (p ∧ (¬q)):

The root is the connective ∧.
The left subtree is the leaf p.
The right subtree consists of the connective ¬, with q as its leaf.

5. Formalization

Definition

Formalization is the process of translating a statement from natural language into a formula of
propositional logic.

Steps for Formalization

1. Identification of Propositions:
Identify the different atomic propositions present in the statement.
2. Assignment of Symbols:
Associate each atomic proposition with a variable (e.g., p, q, etc.).

Dr. Abdelhakim ZEROUAL 7

Propositional Language

3. Selection of Connectives:
Determine the logical relationships (such as implication, conjunction, etc.) and represent
them using the appropriate logical connectives.

Example

Statement: "If the sky is blue, then the weather is nice."

Formalization:
Let p represent "The sky is blue."
Let q represent "The weather is nice."
The formula becomes: p → q

8 Dr. Abdelhakim ZEROUAL

Semantic II

1. Interpretation
The semantic study of a language for the calculation of propositions aims to give a truth value to the
formulas of the language. It is also called model theory.
The semantics associates a valuation function.
V : vp → (1, 0)

(Where vp is the set of propositional variables, 1 means true and 0 means false) unique to each of the
logical connectors.
This function is described by a graph called truth table. Each formula α with n propositional variables
has a unique truth function. The graph of this function is defined by a truth table with 2n lines
representing the truth value of a corresponding to each combination of truth values of the n variables
(also called distribution of truth values of the variables).1 p.26

The negation
The negation of a proposition a noted ¬a or ā is defined as follows:
If the proposition a is true, then ā is false.
If the proposition a is false, then ā is true.
The truth table of negation:

a ā

1 0

0 0

The conjunction
The conjunction of two propositions a and b noted symbolically by a ∧ b and read (a and b) is true if
and only if both propositions a and b are true simultaneously.
The truth table of the conjunction:

a b a ∧ b

1 1 1

1 0 0

0 1 0

0 0 0

Dr. Abdelhakim ZEROUAL 9

Semantic

The disjunction
The disjunction of two propositions a and b noted symbolically by a ∨ b and reads (a or b) is false if
and only if both propositions a and b are false simultaneously.
The truth table of the disjunction:

a b a ∨ b

1 1 1

1 0 1

0 1 1

0 0 0

Conditional
The proposition a → b is false in the case where a is true and b is false. It is defined by the following
table:

a b a → b

1 1 1

1 0 0

0 1 1

0 0 1

Let a and b be two propositions, in the formula , a is called the antecedent and b the
a → b

consequence.
With conditional situations, we also have the following:
The original conditional is “if a, then b” a → b

The converse is “if b, then a” b → a

The inverse is “if not a, then not b” ā → b̄

The contrapositive is “if not b, then not a” b̄ → ā

Biconditional
The proposition a ↔ b is true in the case where a and b have the same truth value. It is defined by the
following table:

a b a ↔ b

1 1 1

1 0 0

0 1 0

0 0 0

10 Dr. Abdelhakim ZEROUAL

 Semantic

Example

Let α be the formula:

p ∨ q → r

The truth table of this formula as follow:

p q r p ∨ q α

1 1 1 1 1

1 1 0 1 0

1 0 1 1 1

1 0 0 1 0

0 1 1 1 1

0 1 0 1 0

0 0 1 0 1

0 0 0 0 1

2. Satisfiability

Definition

A formula α is said to be satisfiable if and only if its truth table contains at least one row where the truth
value of α is true (or V (α) = 1).

α is said to be unsatisfiable if it is false on all rows of its truth table.1 p.26

Example

The formula α of the previous example is satisfiable.

Example

¯
Let β be the formula (p ∧ q) ∧ (p ↔ q)

¯
p q p ∧ q (p ↔ q) β

1 1 1 0 0

1 0 0 1 0

0 1 0 1 0

0 0 0 0 0

Hence β is unsatisfiable.

Dr. Abdelhakim ZEROUAL 11

Semantic

3. Satisfiability of a set of formulas

The notion of satisfiability is generalized to a set of formulas:
Let L = {α1,α2, … , αn} be a set of formulas. L is said to be satisfiable if and only if given the truth table of
all the formulas α1,α2, … , αn there exists at least one row where all these formulas are simultaneously
true.

Example

The set {p ∧ q, p ∨ q, p → q } is satisfiable.

The set {p ∧ q, p ∨ q, q̄ } is unsatisfiable.

4. Tautology

Definition

A formula αis a tautology (note ⊨ ), if and only if α is true on all lines of its truth table.
α

Example

A formula a ∧ b → b is a tautology

a b a ∧ b a ∧ b → b

1 1 1 1

1 0 0 1

0 1 0 1

0 0 0 1

Note

If ⊨ α → β , we say that α logically implies β.

If ⊨ α ↔ β , we say that α logically equivalent to β and we note α ≡ β .

Lemma
A formula α is a tautology if and only if ᾱis unsatisfiable.

Demonstration Method

Suppose that ⊨ α but ᾱ is satisfiable. Therefore, there is at least one row in the truth table
where ᾱ is true. For this line, α is false but ⊨ α. Then α is unsatisfiable.
Now suppose that α is unsatisfiable, but α is not a tautology. Therefore, there is at least one line
in the truth table where α is false. For this line, ᾱ must be true which contradicts the fact that ᾱis
unsatisfiable.

12 Dr. Abdelhakim ZEROUAL

 Semantic

Theorem
If ⊨ α and ⊨ α → β, then ⊨ β.

Demonstration Method

Let's proceed by absurdity.

Suppose ⊨ α and ⊨ α → β, but ⊭ β. Therefore, there is at least one line where β is false. For
this line, α → β is false because ⊨ β. Contradiction with the fact that ⊨ α → β.

5. Logical consequence
In propositional language, a formula 𝛽 is a logical consequence of a formula 𝛼 (and we note 𝛼 ⊨ 𝛽 ), if
and only if given the truth table of 𝛼 and 𝛽, the truth value of 𝛽 is true on all lines where the truth value
of 𝛼 is true.
In general, a formula 𝛽 is a logical consequence of a set of formulas Γ = {𝛼1,𝛼2, … ,𝛼n } (and we note Γ ⊨
𝛽 or 𝛼1,𝛼2, … ,𝛼n ⊨ 𝛽) if and only if, given the truth table of the formulas 𝛼1, 𝛼2, … , 𝛼n, 𝛽, the truth
value of 𝛽 is true on all the lines in which the formulas 𝛼1, 𝛼2, … , 𝛼n, are true simultaneously.

Example

,
p → q q̄ ⊨ p̄

p q p → q q̄ p̄

1 1 1 0 0

1 0 0 1 0

0 1 1 0 1

0 0 1 1 1

Note

1. {𝛼1, … ,𝛼n } ⊨ 𝛼 if and only if ⊨ 𝛼1 ⋀ … ⋀ 𝛼n → 𝛼.

2. Let E be a set of formulas and A ⊆ E. Then, if E is satisfiable, A is satisfiable.
3. The empty set is satisfiable.
4. The set of all formulas is unsatisfiable.
5. Let E be a set of formulas and A ⊆ E. Then, if A is unsatisfiable so E is unsatisfiable.
6. Every tautology is a logical consequence of any set of formulas, in particular of an empty set.

Dr. Abdelhakim ZEROUAL 13

Semantic

6. Substitution theorem

Definition

(see Substitution_Theorem.pdf)
Let β be a formula containing the propositional variable x, and let β be the formula obtained from β by
′

substituting for x, in all its occurrences, a formula α.

If ⊨ β, then ⊨ β ′

Example

Let β ≡ x → ((y → z) → x) . We can check that t ⊨ β. And let

β≡ (a ∧ b) → ((y → z) → (a ∧ b)) obtained by substituting in β, (a ∧ b)for x. Then, ⊨ β.

7. Replacement theorem

Definition

(see Replacement_Therorem.pdf)
Let α be a formula in which the formula β appears in one or more occurrences and let α be the formula
′

obtained from α by replacing β in one or more of its occurrences by the formula β'.
If β ≡ β , then α
′
≡ α ′

Note

Letα ≡ x ∨ (x → y) ↔ (z ∨ (z → y) . We can verify that z → y ≡ z̄ ∨ y .

Let α be the formula obtained from α by replacing z by z̄ .
′
→ y ∨ y

α ′
≡ x ∨ (x → y) ↔ (z ∨ ( z̄ ∨ y)) We can easily verify that α ≡ α. ′

8. Sematic Equivalence

Definition

Two well formed formulas F and G are equivalent, if and only if, the truth values of F and G are the
same.

Let A, B, and well-formed formulas:

Equivalence Name

A → B ≡ ¬A ∨ B Implication

A ⟷ B ≡ (A → B) ∧ (B → A) Equivalence

A ∨ B ≡ B ∨ A Commutative
A ∧ B ≡ B ∧ A laws

14 Dr. Abdelhakim ZEROUAL

 Semantic

Equivalence Name

(A ∨ B) ∨ C ≡ A ∨ (B ∨ C) Associative
(A ∧ B) ∧ C ≡ A ∧ (B ∧ C) laws

A ∨ (B ∧ C) ≡ (A ∨ B) ∧ (A ∨ C) Distributive
A ∧ (B ∨ C) ≡ (A ∧ B) ∨ (A ∧ C) laws

A ∧ T ≡ A Identity
A ∨ F ≡ A laws

A ∨ T ≡ A Domination
A ∧ F ≡ F laws

A ∨ ¬A ≡ T negation
A ∧ ¬A ≡ F laws

¬(A ∨ B) ≡ (¬A ∧ ¬B) De Morgan's

¬(A ∧ B) ≡ (¬A ∨ ¬B) laws

A ∧ A ≡ A Idempotent
A ∨ A ≡ A laws

Logical Equivalences

9. Complete set of connectives

A set S of logical connectives is said to be complete if, given any arbitrary formula A, there exists a
formula B that uses only the connectives from S such that A ≡ B.

Example

Showing that the set {¬, ∨} forms a complete system.

1. ¬P : Already in the set.
2. P ∧ R : ¬(¬P ∨ ¬R) .
3. P ∨ R : Already in the set.
4. P → R : ¬P ∨ R.
5. P ↔ R : ¬(¬(¬P ∨ R)∨¬(¬R ∨ P)).

10. Conjunctive and Disjunctive Normal Form

Atom, Literal, Clause, Conjunctive Normal Form Definition

An atom or atomic formula is a formula with only one propositional variable (no connectives).
A literal is an atomic formula or the negation of an atomic formula.
A conjunctive monomial is a conjunction of literals.

Dr. Abdelhakim ZEROUAL 15

Semantic

A clause is a disjunction of literals.

A formula is in conjunctive normal form if it is a conjunction of clauses.
A formula is in disjunctive normal form if it is a disjunction of monomials.

Conjunctive Normal Form (CNF) Definition

A formula is in Conjunctive Normal Form (CNF) if it is a conjunction (AND, ∧) of one or more clauses,
where each clause is a disjunction (OR, ∨) of literals (a literal is a variable or its negation, e.g., P or ¬P).
•In other words, CNF is an AND of ORs.

General Form
C1 ∧ C 2 ∧ ⋯ ∧ Cn
where each Ci​is a clause of the form:
L1 ∨ L 2 ∨ ⋯ ∨ L m
and each Lj​ is a literal.

Example of CNF Example

The formula: •(P ∨ ¬Q) ∧ (¬P ∨ R) ∧ (Q ∨ ¬R) is in CNF because it is a conjunction of three clauses:
1. P ∨ ¬Q
2. ¬P ∨ R
3. Q ∨ ¬R

Disjunctive Normal Form (DNF) Definition

A formula is in Disjunctive Normal Form (DNF) if it is a disjunction (OR, ∨) of one or more terms, where
each term is a conjunction (AND, ∧) of literals. In other words, DNF is an OR of ANDs.

General Form
T1 ∨ T 2 ∨ ⋯ ∨ T n
​where each Ti​is a term of the form:
L1 ∧ L 2 ∧ ⋯ ∧ L m
and each Lj​is a literal.

Example of DNF Example

The formula:
(P ∧ ¬Q) ∨ (¬P ∧ R) ∨ (Q ∧ ¬R) is in DNF because it is a disjunction of three terms:
1. P ∧ ¬Q
2. ¬P ∧ R
3. Q ∧ ¬R

16 Dr. Abdelhakim ZEROUAL

 Semantic

Converting a Formula to CNF or DNF

1. Remove the connectors → and ↔ using implication and equivalence theorems.
2. Develop the ¬ using Morgan’s Law and remove ¬¬ by involution theorem.
3. Group the ∨ (respectively ∧) by distributivity theorem.

Example

(A ∧ ¬(B ∨ ¬C)) → (¬B → (A ∧ B))

≡ ¬((A ∧ ¬(B ∨ ¬C)) ∨ (B ∨ (A ∧ B))

≡ ¬((A ∧ (¬B ∧ C)) ∨ (B ∨ (A ∧ B))

≡ ((¬A ∨ (B ∨ ¬C)) ∨ (B ∨ (A ∧ B))

≡ ¬A ∨ B ∨ ¬C ∨ B ∨ (A ∧ B)

≡ (A ∨ ¬A ∨ B ∨ ¬C ∨ B) ∧ (B ∨ ¬A ∨ B ∨ ¬C ∨ B)

We obtain a CN F equivalent to the first well formed formula.

Dr. Abdelhakim ZEROUAL 17

The Deductive System (¬, ∧) III

1. Introduction
The deductive system is a formal method that allows us to derive a new formula β from a set of initial
formulas, called premises or hypotheses {α1,…,αn}, by using predefined syntactic transformation rules
(form transformation).

The rules of the deductive system (¬, ∧) allow for the construction of a new formula.
They are generally of the form:

The formulas α1, α2 are the conditions of the rule

The formula β is the conclusion of the rule
(R) is the name of the deduction rule
Deduction will be represented in the form of a tree:

2. Deduction

Definition

A deduction in the deductive system (¬, ∧) is a finite tree that uses the rules (I ∧), (E ∧), (I ¬), and (E ¬),
called Gentzen's Natural Deduction Rules. The leaves of the tree are the initial premises (hypotheses),
and the root is the conclusion.

18 Dr. Abdelhakim ZEROUAL

 The Deductive System (¬, ∧)

Notations
Let Γ be a set of formulas and β a formula. We denote:
Γ ⊢ β: If there exists a deduction D with conclusion β, and all non-eliminated premises
(hypotheses) of D are in Γ.
We say that D is a deduction of β from Γ.
⊢ β: If there exists a deduction D with conclusion β, and all premises (hypotheses) have been
eliminated.
In this case (Γ = ∅), we say that β is a theorem of Lp(¬, ∧).
If Γ is a set of formulas, and β, α, α₁, …, αₙ are formulas, then we write:
α₁, …, αₙ ⊢ β instead of {α₁, …, αₙ} ⊢ β.
Γ, α ⊢ β instead of Γ ∪ {α} ⊢ β.

3. Rules of Deduction
For each of the connectives ¬ and ∧, we associate two rules (Gentzen's Natural Deduction Rules):
1. An introduction rule for the connective, which allows us to derive a compound formula using
this connective.
2. An elimination rule for the connective, which is used to derive a simpler formula by
eliminating this connective.

Rules for the Connective ∧

Introduction rule for ∧, denoted as: (I ∧):
This rule expresses the fact that:

"If we have the formula α and if we also have the formula β, then we can derive the formula α ∧ β."
Elimination rule for ∧, denoted as: (E ∧) It has two (02) forms:

This rule expresses the fact that:

"If we have the formula α ∧ β, then we can derive either the formula α (first form) or the formula β
(second form), depending on what we wish to obtain."

Rules for the Connective ¬

Elimination rule for ¬, denoted as: (E ¬)

This rule expresses the fact that:

"If we have the formula ¬¬α, then we can derive the formula α."
"This rule eliminates two ¬ connectives at once, not just one!!"
Introduction Rule for ¬, denoted as: (I ¬)

Dr. Abdelhakim ZEROUAL 19

The Deductive System (¬, ∧)

"This rule states that:

'If, starting from the assumed hypothesis α (and others), we can derive both a formula and its negation
(β and ¬β) (called a contradiction, denoted as ⊥),
then we can derive the formula ¬α (the negation of α) by removing α.'"

4. Strategy
To prove that: 𝛼1,…,𝛼𝑛 ⊢ 𝛽?
To construct 𝛽, we often assume, in addition to the initial hypotheses, ¬𝛽 (the negation of the
conclusion). This follows a proof by contradiction.

Example 01 Example

Show that we can derive α ∨ β from α: α⊢α∨β?

Since we are working within the deductive system of Lp (¬,∧), we must replace ∨ with its definition: α ∨
β ≡ ¬(¬α ∧ ¬β)
Thus, the proof reduces to showing: α ⊢ ¬(¬α ∧ ¬β)

Example 02 Example

Prove the deduction ⊢ α ∨ ¬α, which can also be interpreted as showing that α ∨ ¬α is a theorem of Lp ?
Remark: There are no initial hypotheses (i.e., Γ = ∅).
Since we are working within the deductive system of Lp (¬, ∧), we replace ∨ with its definition. Thus, the
proof reduces to showing ⊢ ¬(¬α ∧ ¬¬α)

20 Dr. Abdelhakim ZEROUAL

 The Deductive System (¬, ∧)

Example 03 Example

Prove the following deduction: α → β, α ⊢ β

Since we are working within the deductive system of Lp (¬, ∧), we must replace → with its definition: α
→ β ≡ ¬(α ∧ ¬β)
Thus, the proof reduces to showing: ¬(α ∧ ¬β), α ⊢β

5. Other deductive systems

Other deductive systems can be defined in the language Lp of propositional logic.

The Deductive System (¬, →)

Rules for the connective →:
1. (E →): Elimination rule for →
2. (I →): Introduction rule for →

The Deductive System (¬, ∨)

Rules for the connective ∨:
1. (E ∨): Elimination rule for ∨
2. (I ∨): Introduction rule for ∨

Dr. Abdelhakim ZEROUAL 21

DEMONSTRATION THEORY IV

1. Resolution Principle
The resolution principle is an automatic method used to prove the validity of a logical formula.
Before diving into resolution, two key concepts must be understood: clauses and resolvents.

Clause Concept
A clause is a well-formed formula that consists of a disjunction of literals (e.g., A ∨ B ∨ C ∨ D).
To obtain a set of clauses from a well-formed formula:
1. Convert the formula into its conjunctive normal form (CNF).
2. Eliminate the "∧" connectors, resulting in a set S of clauses

Resolving Clause
If C1 and C2 are clauses, and there is a literal L1 in C1 that is the negation of a literal L2 in C2 (i.e.,
L1=¬L2), you can resolve these clauses.
• The resolvent clause C is formed by removing L1 and L2 from C1 and C2 and taking the disjunction
(logical OR) of the remaining literals.
• This process is called resolution, and the resulting clause C is denoted as Resolvent(C1,C2).

Example 01 Example

Let C1 = E1 ∨ E2 and C2 = ¬E2 ∨ E3.

• Here, E2 and ¬E2 are complementary literals, so they can be resolved.
• The resolvent C is E1 ∨ E3, which is formed by removing E2 and ¬E2 and combining the remaining
literals.

Example 02 Example

Let C1 = P and C2 = ¬P.

Since P and ¬P are complementary literals, resolving them results in the empty clause ∅.
The empty clause represents a contradiction, indicating that the original set of clauses is unsatisfiable.

22 Dr. Abdelhakim ZEROUAL

 DEMONSTRATION THEORY

2. Resolution Algorithm
Let R1 = R ∨ Q and R2 = ¬R.
Resolving R1 and R2 gives Q (since R and ¬R cancel out).
This process continues until the empty clause is derived (if possible).
If the empty clause ∅ is derived from a set of clauses S, then S is unsatisfiable (i.e., there is no
assignment of truth values that makes all clauses in S true).
The process of deriving the empty clause is called a refutation.

To prove that a well-formed formula F is valid, you can:

1. Show that ¬F is inconsistent (i.e., unsatisfiable).
2. Use the resolution algorithm to derive the empty clause from the set of clauses representing ¬F.
If the empty clause is derived, then ¬F is inconsistent, and F must be valid (Satisfiable).

Resolution Algorithm Steps

1. Write the negation of F.
2. Convert ¬F into a set of clauses.
3. While the empty clause is not found and there are reducible pairs:
Search for resolvent clauses.
Add the resolvent to the list of clauses.
4. If the empty clause is found, F is valid.
5. If the empty clause is not found, F is invalid.

Example 01 Example

Let S = {¬P ∨ ¬Q ∨ R, ¬R, P, ¬T ∨ Q, T}.

The clauses are:
C1 = ¬P ∨ ¬Q ∨ R
C2 = ¬R
C3 = P
C4 = ¬T∨Q
C5 = T
This set represents the negation of a well-formed formula F.
Resolving
C1 and C2 gives
C6=¬P∨¬Q.
Resolving C6 and C3 gives C7=¬Q.
Resolving C7 and C4 gives C8=¬T.
Resolving C8 and C5 gives C9=∅ (the empty clause).
Since the empty clause is derived, ¬F is inconsistent, and F is valid (Satisfiable)

Dr. Abdelhakim ZEROUAL 23

DEMONSTRATION THEORY

Example 02 Example

Let S = {P ∨ Q, ¬Q ∨ T, ¬T ∨ R, ¬R, ¬P ∨ R, Q ∨ S, P ∨ S}.

This is another set of clauses to which the resolution algorithm can be applied.

Important Remarks
A clause can be used multiple times in the resolution process.
Clauses cannot be used to directly deduce the empty clause; the empty clause is derived through a
series of resolutions.
Only one resolution is performed at a time.
For example, if C1 = P ∨ Q and C2 = ¬P ∨ ¬Q:
Resolving C1 and C2 can give P ∨ ¬P (eliminating Q and ¬Q).
Alternatively, it can give Q ∨ ¬Q (eliminating P and ¬P).
However, it cannot directly give the empty clause ∅.

3. Strategies of Resolution
The resolution rule is an inference rule that states:
If you have {X ∨ A, ¬X ∨ B}, you can derive A ∨ B.
This can be interpreted as:
(¬X ∨ B) = (X → B)
(A ∨ X) = (¬A → X)
Combining these gives ¬A → B = A ∨ B.

Example

Let C1 = P ∨ Q ∨ R, C2 = ¬P ∨ Q ∨ R, and C3 = ¬Q ∨ R.
Resolving C1 and C2 gives C4 = Q ∨ R.
Resolving C4 and C3 gives R.
Thus, R is a logical consequence of the set {P ∨ Q ∨ R, ¬P ∨ Q ∨ R, ¬Q ∨ R}.

Resolution + Refutation Definition

To prove a proposition, start with a set of clauses that includes the negation of the proposition.
Apply the resolution rule repeatedly, adding new resolvents to the set.
If the empty clause ∅ is derived, the original proposition is valid (since its negation leads to a
contradiction).

24 Dr. Abdelhakim ZEROUAL

Conclusion

This chapter equips learners with essential tools to analyze and construct logical arguments using
propositional logic. By mastering syntax, semantics, and deduction systems, students gain the ability to
formalize problems, verify logical validity, and apply automated reasoning techniques like resolution.
These skills lay the groundwork for deeper study in formal logic, computer science, and mathematical
proof systems.

Dr. Abdelhakim ZEROUAL 25

Bibliography

[1] [Link]

26 Dr. Abdelhakim ZEROUAL