🧠 Knights and Knaves Logic Puzzle Solver

This project solves Knights and Knaves logic puzzles using propositional logic and model checking. Each character in the puzzle is either a knight (always tells the truth) or a knave (always lies). By representing statements with logic expressions and evaluating all possible models, the program deduces who is a knight or a knave.

Overview

Inspired by Raymond Smullyan’s 1978 book “What Is the Name of This Book?”, Knights and Knaves puzzles present a logical challenge:

• Knights always tell the truth.
• Knaves always lie.
• The goal is to determine, using logic, the identity of each character based on what they say.

Example:

A says, “I am both a knight and a knave.”
This is a contradiction, so A must be a knave.

🧩 Puzzles Implemented

Four logic puzzles are defined in puzzle.py, each using a custom knowledge base:

🔹 Puzzle 0

• A says: “I am both a knight and a knave.”

🔹 Puzzle 1

• A says: “We are both knaves.”

• B says nothing.

🔹 Puzzle 2

• A says: “We are the same kind.”

• B says: “We are of different kinds.”

🔹 Puzzle 3

• A says either: “I am a knight.” or “I am a knave.” (you don’t know which)

• B says: “A said ‘I am a knave.’”

• B also says: “C is a knave.”

• C says: “A is a knight.”

Each puzzle tests a different aspect of propositional reasoning and the model-checking engine.

🛠 How It Works

The project includes:

• logic.py – Propositional logic engine for building and evaluating logical expressions.
• puzzle.py – Contains the puzzle definitions and logic to solve them.
• model_check – Recursive model checker to determine if a query is entailed by the knowledge base.

The knowledge bases are constructed using symbols like:

AKnight, AKnave, BKnight, BKnave, CKnight, CKnave

With logical operations such as:

And, Or, Not, Implication, Biconditional

▶️ Running

From the project directory, run:

python puzzle.py

The program will evaluate each puzzle and print out logical conclusions for who is a knight and who is a knave.

Example Output

🧩 Extend the Logic

You can add your own puzzles by defining additional knowledge bases in puzzle.py. Use propositional logic to model characters' statements and apply model_check.