Resolution Refutation Theorem Prover

Command-line theorem prover for propositional logic using the resolution-refutation algorithm.

The project checks whether a knowledge base entails a query by adding the negated query to the clause set and repeatedly applying resolution. If the empty clause is derived, the query is entailed by the knowledge base.

Overview

The implementation supports propositional clauses in conjunctive normal form using:

• | for disjunction
• ! for negation
• one clause per input line

It prints each resolution step followed by the final entailment result:

• 1 if the knowledge base entails the query
• 0 otherwise

Repository Structure

.
├── resolution_refutation.py
├── input.txt
├── requirements.txt
├── .gitignore
└── README.md

Method

Resolution refutation proves entailment by contradiction:

KB entails Q iff KB ∧ ¬Q is unsatisfiable

The prover:

1. Reads the knowledge base clauses.
2. Negates the query clause and adds the resulting unit clauses to the clause set.
3. Resolves pairs of clauses containing complementary literals.
4. Returns success when the empty clause is derived.
5. Returns failure when no new clauses can be generated.

Input Format

n
clause_1
clause_2
...
clause_n
query

Where:

• n is the number of knowledge base clauses.
• Each knowledge base line is a disjunction of literals.
• The final line is the query clause to prove.

Example

Input:

2
A|B
!B
A

Run:

python resolution_refutation.py input.txt

Example output:

1: RESOLVE (A | B) and (!B) => A
2: RESOLVE (A | B) and (!A) => B
3: RESOLVE (!B) and (B) => {}
1

Quiet Mode

To print only the final result:

python resolution_refutation.py input.txt --quiet

Requirements

The implementation uses only the Python standard library.

Recommended runtime:

Python 3.9+