Propositional Theorem Proving – Inference and Proofs

Propositional theorem proving is the process of using the rules of propositional logic to determine whether a conclusion logically follows from a set of known facts.

This is an important topic because it connects Propositional Logic with AI reasoning.

---

1. What is Theorem Proving?

Definition

Theorem proving is the process of establishing that a proposition or conclusion logically follows from a given set of premises or knowledge base using valid rules of inference.

In AI:

Knowledge Base
      ↓
Facts + Rules
      ↓
Inference / Theorem Proving
      ↓
Logical Conclusion

Simple example

Suppose the AI knows:

1. If it rains, the road is wet.
2. It is raining.

Therefore:

3. The road is wet.

Represented as:\[ P \rightarrow Q \]\[ P \]

Therefore:\[ Q \]

This is a theorem-proving/inference process.

---

2. What is Inference?

Definition

Inference is the process of deriving new information or conclusions from existing facts and rules.

For example:

Fact:
Ravi studies.

Rule:
If a student studies, then the student passes.

Conclusion:
Ravi passes.

In logical form:\[ Studies(Ravi) \]\[ Studies(Ravi)\rightarrow Pass(Ravi) \]

Therefore:\[ Pass(Ravi) \]

---

3. Inference vs Theorem Proving

These terms are closely related but slightly different.

Inference	Theorem Proving
Derives conclusions from knowledge	Establishes that a conclusion logically follows
General reasoning process	More formal proof process
Uses inference rules	Uses formal proof procedures
Example: derive Q from P and P→Q	Prove that KB ⊨ Q

In AI, both are used to enable automated reasoning.

---

4. Knowledge Base

A Knowledge Base (KB) contains facts and rules.

For example:

Fact 1: It is raining.
Fact 2: If it rains, the road is wet.

Represent:\[ P \]\[ P\rightarrow Q \]

The knowledge base is:\[ KB = \{P,\ P\rightarrow Q\} \]

The AI wants to determine whether:\[ Q \]

follows from KB.

---

5. Premises and Conclusion

A logical argument consists of:

Premises

Statements that are assumed to be true.

Conclusion

Statement that we want to prove.

Example:

Premise 1: All humans are mortal.
Premise 2: Socrates is a human.
Conclusion: Socrates is mortal.

In propositional form, a simplified representation could be:\[ P \]\[ P\rightarrow Q \]

Therefore:\[ Q \]

---

6. Entailment

One of the most important concepts in theorem proving is logical entailment.

Symbol:\[ KB \models \alpha \]

Read as:

“Knowledge Base KB entails α.”

It means:

Whenever the knowledge base is true, α must also be true.

Example

Given:\[ P \]

and:\[ P\rightarrow Q \]

we can say:\[ KB\models Q \]

because Q necessarily follows from KB.

---

7. Inference Rule

An inference rule is a logical pattern that allows us to derive a valid conclusion from known statements.

For example:\[ P,\quad P\rightarrow Q \]

Therefore:\[ Q \]

This is Modus Ponens.

Inference rules are the basic building blocks of theorem proving.

---

8. Important Rules of Inference

For your MCA syllabus, you should understand the following rules.

1. Modus Ponens
2. Modus Tollens
3. And-Elimination
4. And-Introduction
5. Or-Introduction
6. Hypothetical Syllogism
7. Resolution

Resolution is particularly important because it is a major automated theorem-proving technique.

---

9. Modus Ponens

This is one of the most important inference rules.

Form

\[ P \]\[ P\rightarrow Q \]

Therefore:\[ \boxed{Q} \]

Example

Premise 1:

It is raining.

\[ P \]

Premise 2:

If it rains, the road is wet.

\[ P\rightarrow Q \]

Conclusion:

The road is wet.

\[ Q \]

Diagram

P is true
   +
P → Q
   ↓
Q is true

---

10. Modus Tollens

Modus Tollens works in the opposite direction.

Form

\[ P\rightarrow Q \]\[ \neg Q \]

Therefore:\[ \boxed{\neg P} \]

Example

If it rains, the road is wet.

\[ P\rightarrow Q \]

The road is not wet.

\[ \neg Q \]

Therefore:

It did not rain.

\[ \neg P \]

---

11. And-Elimination

If we know:\[ P\land Q \]

we can derive either:\[ P \]

or:\[ Q \]

Example

Given:

Ravi is a student AND Ravi is present.

\[ Student(Ravi)\land Present(Ravi) \]

We can conclude:\[ Student(Ravi) \]

and:\[ Present(Ravi) \]

---

12. And-Introduction

If we know:\[ P \]

and:\[ Q \]

we can combine them:\[ \boxed{P\land Q} \]

Example

Given:

Ravi is a student.

and:

Ravi is present.

Therefore:

Ravi is a student AND Ravi is present.

---

13. Or-Introduction

If P is true, then:\[ P\lor Q \]

is also true, regardless of Q.

Example

If:\[ P = True \]

then:\[ P\lor Q = True \]

because at least one part is true.

---

14. Hypothetical Syllogism

Suppose:\[ P\rightarrow Q \]

and:\[ Q\rightarrow R \]

Therefore:\[ \boxed{P\rightarrow R} \]

Example

If it rains → road becomes wet.

If road becomes wet → driving becomes difficult.

Therefore:

If it rains → driving becomes difficult.

Logical form:\[ P\rightarrow Q \]\[ Q\rightarrow R \]

Therefore:\[ P\rightarrow R \]

---

15. Example of a Complete Inference Chain

Suppose the knowledge base contains:\[ P \]\[ P\rightarrow Q \]\[ Q\rightarrow R \]\[ R\rightarrow S \]

Then:

P
↓
Q
↓
R
↓
S

Therefore:\[ KB\models S \]

This type of reasoning is the foundation of rule-based AI systems.

---

16. Proof

A proof is a sequence of logically valid steps that establishes that a conclusion follows from the premises.

Example:

Given

\[ P\rightarrow Q \]\[ P \]

Prove

\[ Q \]

Proof

Step	Statement	Reason
1	\(P\rightarrow Q\)	Given
2	\(P\)	Given
3	\(Q\)	Modus Ponens

Therefore:\[ \boxed{Q} \]

This is a simple propositional proof.

---

17. Direct Proof

In a direct proof, we start with known facts and apply inference rules until we reach the desired conclusion.

Example:

Given:\[ P \]\[ P\rightarrow Q \]\[ Q\rightarrow R \]

Prove:\[ R \]

Proof

1. \(P\) — Given
2. \(P\rightarrow Q\) — Given
3. \(Q\) — Modus Ponens
4. \(Q\rightarrow R\) — Given
5. \(R\) — Modus Ponens

Therefore:\[ \boxed{R} \]

---

18. Proof by Contradiction

Another important proof technique is proof by contradiction.

The basic idea is:

Assume the opposite of what you want to prove. If that assumption leads to a contradiction, the original statement must be true.

Suppose we want to prove:\[ Q \]

We assume:\[ \neg Q \]

If this produces a contradiction, we conclude:\[ Q \]

Structure

Want to prove Q
      ↓
Assume ¬Q
      ↓
Apply logical rules
      ↓
Contradiction
      ↓
Therefore Q

This approach is closely related to proof by refutation, which is important for resolution.

---

19. Model-Based Understanding of Entailment

Suppose:\[ KB = \{P,\ P\rightarrow Q\} \]

There is no possible interpretation in which:

• KB is true
• but Q is false.

Therefore:\[ KB\models Q \]

This gives another way to understand entailment:

If every model that satisfies KB also satisfies Q, then KB entails Q.

---

20. What is a Model?

A model is an assignment of truth values to propositions that makes a logical sentence true.

Suppose:\[ P\rightarrow Q \]

If:

P = True
Q = True

then the expression is true.

That assignment is a model of the expression.

For entailment

\[ KB\models \alpha \]

means:

Every model of KB is also a model of α.

---

21. Truth Table Method of Theorem Proving

One method for determining whether a conclusion follows from premises is to construct a truth table.

Suppose:\[ KB = P\land(P\rightarrow Q) \]

We want to determine whether:\[ Q \]

is entailed.

We can construct:

P	Q	P → Q	P ∧ (P → Q)
T	T	T	T
T	F	F	F
F	T	T	F
F	F	T	F

The only case where KB is true is:

P = T
Q = T

Therefore:\[ KB\models Q \]

---

22. Model Checking

The truth-table method is also called model checking.

The basic idea is:

Generate all possible models
          ↓
Find models where KB is true
          ↓
Check whether conclusion is true
          ↓
If conclusion is true in ALL such models
          ↓
KB entails conclusion

Important limitation

With \(n\) propositional variables, we may need:\[ 2^n \]

models.

Therefore, the number of possibilities grows exponentially.

This is one reason more efficient theorem-proving techniques are important.

---

23. Forward Chaining

Forward chaining starts with known facts and repeatedly applies rules to derive new facts.

Example:

Knowledge:\[ P \]\[ P\rightarrow Q \]\[ Q\rightarrow R \]

Forward chaining:

Known:
P

Apply P → Q
      ↓
Derive Q

Apply Q → R
      ↓
Derive R

Therefore:\[ P\Rightarrow Q\Rightarrow R \]

Direction

Facts → Rules → New Facts → Goal

It is called data-driven reasoning.

---

24. Backward Chaining

Backward chaining starts with the goal and works backward to determine which facts would be required.

Suppose the goal is:\[ R \]

and we have:\[ Q\rightarrow R \]

The system asks:

What do I need to prove R?

Answer:\[ Q \]

Then:\[ P\rightarrow Q \]

So it asks:

What do I need to prove Q?

Answer:\[ P \]

And if P is a known fact, the proof succeeds.

Diagram

Goal: R
  ↑
Q → R
  ↑
P → Q
  ↑
Fact: P

Direction

Goal → Required Conditions → Facts

It is called goal-driven reasoning.

---

25. Forward vs Backward Chaining

Feature	Forward Chaining	Backward Chaining
Direction	Facts → Goal	Goal → Facts
Type	Data-driven	Goal-driven
Starts with	Known facts	Query/goal
Best when	Many facts, need conclusions	Specific goal/query
Example	Expert system	Logic programming
Reasoning	Derives consequences	Finds supporting conditions

---

26. Proof by Resolution

Resolution is another very important theorem-proving technique and is specifically mentioned in your syllabus.

Resolution works by:

1. Converting propositions into a standard form.
2. Negating the conclusion.
3. Combining clauses using the resolution rule.
4. Deriving a contradiction.
5. Therefore proving the original conclusion.

The central idea is:\[ \boxed{\text{Negate the goal and derive contradiction}} \]

We will study this separately in detail as Proof by Resolution.

---

27. Soundness and Completeness

These are very important concepts in theorem proving.

Soundness

An inference procedure is sound if it never derives an invalid conclusion.

In simple terms:

Everything it proves is actually logically correct.

If:\[ KB\vdash Q \]

then:\[ KB\models Q \]

for a sound inference system.

---

Completeness

An inference procedure is complete if it can derive every conclusion that logically follows from the knowledge base.

In simple terms:

If something is logically entailed, the procedure is capable of proving it.

If:\[ KB\models Q \]

then a complete inference system can derive:\[ KB\vdash Q \]

---

28. ⊢ vs ⊨

Students often confuse these two symbols.

\(\models\)

Means semantic entailment.\[ KB\models Q \]

means:

Q is logically true whenever KB is true.

\(\vdash\)

Means syntactic derivation/proof.\[ KB\vdash Q \]

means:

Q can be derived from KB using an allowed inference procedure.

Simple distinction

Symbol	Meaning
\(\models\)	Entails / semantic consequence
\(\vdash\)	Proves / syntactic derivation

For a sound and complete inference system, these correspond appropriately.

---

29. Example: AI Medical Rule System

Consider a simple hypothetical rule-based system.

Facts

\[ Fever \]\[ Cough \]

Rules

\[ Fever\land Cough\rightarrow SuspectedFlu \]

The system can infer:\[ SuspectedFlu \]

Reasoning

Fever
   +
Cough
   ↓
Fever AND Cough
   ↓
Rule:
Fever AND Cough → Suspected Flu
   ↓
Suspected Flu

This illustrates how theorem proving can be used in a rule-based AI system.

Note: In a real medical system, such a logical rule would not by itself establish a medical diagnosis; it is only an illustration of logical inference.

---

30. Example: Student Academic System

Knowledge base:

Studies(Ravi)
Studies(x) → Pass(x)
Pass(x) → EligibleForCertificate(x)

In simple propositional notation for a particular student:\[ P = Studies(Ravi) \]\[ P\rightarrow Q \]\[ Q\rightarrow R \]

Therefore:\[ P\Rightarrow Q\Rightarrow R \]

Conclusion:

Ravi is eligible for the certificate.

This example also shows why First-Order Logic becomes useful: it allows us to express the variable \(x\) and general rules such as:\[ Studies(x)\rightarrow Pass(x) \]

---

31. Important Inference Patterns

For examination, remember these:

Modus Ponens

\[ P,\quad P\rightarrow Q \]\[ \therefore Q \]

Modus Tollens

\[ P\rightarrow Q,\quad \neg Q \]\[ \therefore\neg P \]

And Elimination

\[ P\land Q \]\[ \therefore P \]

And Introduction

\[ P,\quad Q \]\[ \therefore P\land Q \]

Hypothetical Syllogism

\[ P\rightarrow Q,\quad Q\rightarrow R \]\[ \therefore P\rightarrow R \]

Resolution

\[ P\lor Q,\quad \neg P\lor R \]\[ \therefore Q\lor R \]

---

32. Overall Theorem-Proving Process

The complete picture is:

             Knowledge Base
            /              \
         Facts              Rules
           \                /
            \              /
             ↓            ↓
              Inference
                  |
                  ↓
          Derived Statements
                  |
                  ↓
             Goal / Query
                  |
          ┌───────┴────────┐
          ↓                ↓
       Proven            Not Proven

---

33. Relation to Your Next Topics

Your syllabus has:

Propositional Logic
       ↓
Propositional Theorem Proving
       ↓
Inference and Proofs
       ↓
Proof by Resolution
       ↓
Horn Clauses
       ↓
Definite Clauses
       ↓
Forward Chaining
       ↓
Backward Chaining
       ↓
First-Order Logic
       ↓
Inference in First-Order Logic

So the key progression is:

Represent knowledge → infer conclusions → prove conclusions → use efficient theorem-proving methods.

---

34. Exam-Oriented Definition

Propositional theorem proving is the process of proving that a proposition logically follows from a set of premises or a knowledge base using valid inference rules. It involves representing facts and rules in propositional logic and applying techniques such as Modus Ponens, Modus Tollens, truth-table/model checking, forward chaining, backward chaining and resolution to establish logical conclusions.

---

35. Short Exam Answer

If the question is “Explain inference and proofs in propositional logic”, you can write:

Inference is the process of deriving new propositions from known facts and rules. A proof is a sequence of valid inference steps used to establish that a conclusion follows from given premises.

For example:\[ P \]\[ P\rightarrow Q \]

Using Modus Ponens:\[ \therefore Q \]

Important inference techniques include Modus Ponens, Modus Tollens, truth-table/model checking, forward chaining, backward chaining and resolution. The concepts of soundness and completeness are used to evaluate inference procedures.

---

36. Final Revision Diagram

              PROPOSITIONAL LOGIC
                       |
                       ↓
               Knowledge Base
                       |
                ┌──────┴──────┐
                ↓             ↓
              Facts          Rules
                \             /
                 \           /
                  ↓         ↓
                   INFERENCE
                       |
          ┌────────────┼────────────┐
          ↓            ↓            ↓
       Modus         Forward      Backward
       Ponens        Chaining     Chaining
          |                          |
          └────────────┬─────────────┘
                       ↓
                  THEOREM PROVING
                       |
                       ↓
                  Proof / Result
                       |
                       ↓
                Logical Conclusion

One line to remember

Inference derives a conclusion; theorem proving formally establishes that the conclusion follows from the knowledge base.