Resolution Algorithm: Proving "If All Drivers Horn, Then All Traffics Are Frustrated"

Step 1: Identify the Facts and Convert to FoPL (First Order Predicate Logic)

Let us define the predicates:

• Traffic(x) : x is a traffic
• Driver(x) : x is a driver
• Horns(x) : x horns
• Smart(x) : x is smart
• Chases(x, y) : x chases y
• Catches(x, y) : x catches y
• Frustrated(x) : x is frustrated

FoPL Knowledge Base

Goal (to prove):

If all drivers horn, then all traffics are frustrated. ∀x ∀y [Driver(y) ∧ Horns(y) ∧ Traffic(x) → Frustrated(x)]

Step 2: Convert All Statements to Conjunctive Normal Form (CNF) / Clause Form

Using the implication elimination rule: A → B ≡ ¬A ∨ B

C1 (from F1):

∀x ∀y [Traffic(x) ∧ Driver(y) → Chases(x, y)]
≡ ¬Traffic(x) ∨ ¬Driver(y) ∨ Chases(x, y)

C2 (from F2):

∀x [Driver(x) ∧ Horns(x) → Smart(x)]
≡ ¬Driver(x) ∨ ¬Horns(x) ∨ Smart(x)

C3 (from F3):

∀x ∀y [Traffic(x) ∧ Smart(y) → ¬Catches(x, y)]
≡ ¬Traffic(x) ∨ ¬Smart(y) ∨ ¬Catches(x, y)

C4 (from F4):

∀x ∀y [Traffic(x) ∧ Driver(y) ∧ Chases(x,y) ∧ ¬Catches(x,y) → Frustrated(x)]
≡ ¬Traffic(x) ∨ ¬Driver(y) ∨ ¬Chases(x,y) ∨ Catches(x,y) ∨ Frustrated(x)

Step 3: Negate the Goal (for Proof by Refutation / Resolution)

The goal to prove:

∀x ∀y [Traffic(x) ∧ Driver(y) ∧ Horns(y) → Frustrated(x)]

Negate the goal:

¬[∀x ∀y (Traffic(x) ∧ Driver(y) ∧ Horns(y) → Frustrated(x))]
≡ ∃x ∃y [Traffic(x) ∧ Driver(y) ∧ Horns(y) ∧ ¬Frustrated(x)]

Using Skolemization (replace existential variables with constants a and b):

C5: Traffic(a)

C6: Driver(b)

C7: Horns(b)

C8: ¬Frustrated(a)

Step 4: Apply Resolution Algorithm

We now have the clause set:

C1: ¬Traffic(x) ∨ ¬Driver(y) ∨ Chases(x, y)
C2: ¬Driver(x) ∨ ¬Horns(x) ∨ Smart(x)
C3: ¬Traffic(x) ∨ ¬Smart(y) ∨ ¬Catches(x, y)
C4: ¬Traffic(x) ∨ ¬Driver(y) ∨ ¬Chases(x,y) ∨ Catches(x,y) ∨ Frustrated(x)
C5: Traffic(a)
C6: Driver(b)
C7: Horns(b)
C8: ¬Frustrated(a)

Resolution Steps:

Step R1: Resolve C2 with C6 and C7

C2 : ¬Driver(x) ∨ ¬Horns(x) ∨ Smart(x)   [x = b]
C6 : Driver(b)
C7 : Horns(b)
----------------------------------------------
R1 : Smart(b)

Step R2: Resolve C1 with C5 and C6

C1 : ¬Traffic(x) ∨ ¬Driver(y) ∨ Chases(x, y)   [x = a, y = b]
C5 : Traffic(a)
C6 : Driver(b)
----------------------------------------------
R2 : Chases(a, b)

Step R3: Resolve C3 with C5 and R1

C3 : ¬Traffic(x) ∨ ¬Smart(y) ∨ ¬Catches(x, y)   [x = a, y = b]
C5 : Traffic(a)
R1 : Smart(b)
----------------------------------------------
R3 : ¬Catches(a, b)

Step R4: Resolve C4 with C5, C6, and R2

C4 : ¬Traffic(x) ∨ ¬Driver(y) ∨ ¬Chases(x,y) ∨ Catches(x,y) ∨ Frustrated(x)   [x = a, y = b]
C5 : Traffic(a)
C6 : Driver(b)
R2 : Chases(a, b)
----------------------------------------------
R4 : Catches(a, b) ∨ Frustrated(a)

Step R5: Resolve R4 with R3

R4 : Catches(a, b) ∨ Frustrated(a)
R3 : ¬Catches(a, b)
----------------------------------------------
R5 : Frustrated(a)

Step R6: Resolve R5 with C8

R5 : Frustrated(a)
C8 : ¬Frustrated(a)
----------------------------------------------
NIL  (Empty Clause -- Contradiction!)

Step 5: Conclusion

Since resolution derives the empty clause (NIL) from the knowledge base together with the negated goal, the negated goal is unsatisfiable together with the facts. By the refutation principle, this proves the original statement:

$$\boxed{\text{If all drivers horn, then all traffics are frustrated.}}$$

Crossover Operation in Genetic Algorithm

Given Data

• Chromosome $C_1 = 01100010$
• Chromosome $C_2 = 10101100$
• Each chromosome has 8 bits.
• Crossover points to be chosen by student.

Position indexing:

C1 = 0 1 1 0 0 0 1 0
C2 = 1 0 1 0 1 1 0 0
     1 2 3 4 5 6 7 8

Definition of Crossover

Crossover (also called recombination) is a genetic operator in a Genetic Algorithm that combines the genetic material of two parent chromosomes to produce one or more offspring. Two parents are selected from the mating pool, one or more crossover points are chosen, and the segments of the parents are exchanged around these points. Crossover is the primary operator responsible for exploring new regions of the search space by recombining good building blocks (schemas) from both parents, thereby helping the population converge toward better solutions.

One-Point Crossover

Chosen crossover point: after position 4.

Split at position 4:

Swap the tails:

C1 = 0110 | 0010
C2 = 1010 | 1100
          ^  (cut after position 4)

O1 = 0110 | 1100  = 01101100
O2 = 1010 | 0010  = 10100010

Offspring: $O_1 = 01101100$, $O_2 = 10100010$.

Verification of bit copy:

• O1 head = C1 head 0110 ✓; O1 tail = C2 tail 1100 ✓
• O2 head = C2 head 1010 ✓; O2 tail = C1 tail 0010 ✓

Two-Point Crossover

Chosen crossover points: after position 2 and after position 6.

Split into three segments:

Check the middle segment of C1 (pos 3-6): C1 = 0 1 1 0 0 0 1 0 → 1000 ✓ Middle segment of C2 (pos 3-6): C2 = 1 0 1 0 1 1 0 0 → 1011 ✓

Swap the middle segment:

C1 = 01 | 1000 | 10
C2 = 10 | 1011 | 00
       ^        ^
  cut after 2   cut after 6

O1 = 01 | 1011 | 10 = 01101110
O2 = 10 | 1000 | 00 = 10100000

Offspring: $O_1 = 01101110$, $O_2 = 10100000$.

Summary Table

Crossover recombines features of both parents to generate new candidate solutions, which is essential for the genetic algorithm to search effectively and converge toward an optimal solution.