This project is a small logic engine and set of example programs that model and solve propositional-logic puzzles.
It provides a minimal library (logic.py) for building sentences in propositional logic and several scripts that
encode classic puzzles (Harry/Hagrid, Hogwarts house placement, Clue, and Mastermind) as knowledge bases and then
query what must be true.
The code is deliberately compact and readable, making it useful as a teaching example for knowledge-based agents and model checking.
The main goal of this project is to demonstrate how propositional logic and model checking can be used to reason about worlds described by rules and facts. The library lets you:
- Declare propositional symbols (e.g.
rain,GilderoyGryffindor) - Build complex formulas using logical connectives (
Not,And,Or,Implication,Biconditional) - Encode a knowledge base of constraints about a puzzle
- Ask whether a given proposition is entailed by the knowledge base via exhaustive model checking
The example scripts show how to use these tools to solve small, self-contained puzzles.
-
logic.py
Core logic library. Defines the sentence hierarchy (Sentence,Symbol,Not,And,Or,Implication,Biconditional) and themodel_checkfunction used by all puzzle scripts. -
harry.py
Simple example puzzle about whether it is raining, involving the characters Hagrid and Dumbledore. Demonstrates building a small knowledge base inline and querying a single symbol (rain). -
puzzle.py
Hogwarts house-placement puzzle. Encodes constraints about which of four people are in which of four houses and prints any assignments that are logically forced by the knowledge base. -
clue.py
Mini Clue/Cluedo-style puzzle. Usestermcolorto print colored output indicating which suspect/room/weapon must be true, might be true, or is not entailed by the knowledge base. -
mastermind.py
Mastermind-style puzzle involving colored pegs in four positions. The script builds a knowledge base from the game constraints and prints any color–position assignments that are logically entailed. -
requirements.txt
Python dependency list for this project (currently onlytermcolorfor colored terminal output used byclue.py). -
lecture.pdf
A PDF document presumably containing lecture slides or notes that accompany this code. It is not required to run the code but may provide additional context about the logic and puzzles.
Classes
-
EvaluationException(Exception)
Custom exception raised when evaluating aSymbolwith respect to a model that does not define a value for that symbol. -
Sentence(base class)
Abstract base class for all propositional formulas. Provides:evaluate(model)– abstract; subclasses must implement the truth evaluation of the sentence under a given model (adictmapping symbol names to booleans).formula()– returns a string representation of the sentence (subclasses override this).symbols()– returns asetof symbol names appearing in the sentence (subclasses override this).validate(sentence)– class method that checks an object is aSentenceinstance, raisingTypeErrorotherwise.parenthesize(s)– helper that adds parentheses around an expressionswhen needed, taking care to respect existing balanced parentheses.
-
Symbol(Sentence)
Represents an atomic propositional symbol (e.g."rain","GilderoyGryffindor").__init__(name)– store the symbol name.evaluate(model)– returnsbool(model[name]); raisesEvaluationExceptionif the symbol is not present in the provided model.formula()– returns the symbol name.symbols()– returns{name}.
-
Not(Sentence)
Logical negation of a single operand.__init__(operand)– validates thatoperandis aSentenceand stores it.evaluate(model)– returns logical negation of the operand’s value.formula()– returns"¬"followed by a parenthesized subformula.symbols()– forwards to the operand’ssymbols().
-
And(Sentence)
Logical conjunction of one or more conjuncts.__init__(*conjuncts)– validates and stores a list of conjunct sentences.add(conjunct)– validate and append another conjunct.evaluate(model)– returnsTrueonly if all conjuncts evaluate toTrue.formula()– joins conjunct formulas with" ∧ ", using parentheses where needed.symbols()– returns the union of all symbol sets from the conjuncts (empty set if there are none).
-
Or(Sentence)
Logical disjunction of one or more disjuncts.__init__(*disjuncts)– validates and stores disjunct sentences.evaluate(model)– returnsTrueif any disjunct evaluates toTrue.formula()– joins disjunct formulas with" ∨ ", using parentheses where needed.symbols()– union of symbol sets from all disjuncts (empty set if there are none).
-
Implication(Sentence)
Representsantecedent => consequent.__init__(antecedent, consequent)– validate and store sub-sentences.evaluate(model)– implements material implication:not antecedent or consequent.formula()– returns"(antecedent) => (consequent)"with appropriate parentheses.symbols()– union of symbols from antecedent and consequent.
-
Biconditional(Sentence)
Representsleft <=> right(logical equivalence).__init__(left, right)– validate and store both sides.evaluate(model)–Truewhen both sides are true or both are false.formula()– returns"(left) <=> (right)"(using each side’sformula()).symbols()– union of symbols from both sides.
Functions
-
model_check(knowledge, query)
Given a knowledge baseknowledge(aSentence) and a propositionquery(anotherSentence), performs exhaustive model checking to decide whetherknowledgeentailsquery.Behaviour:
- Collects all symbols appearing in either
knowledgeorquery. - Recursively considers every possible truth assignment (model) for those symbols.
- For every model, if
knowledge.evaluate(model)is true, then it requires thatquery.evaluate(model)is also true; otherwise the entailment fails. - Returns
Trueif the entailment condition holds for all models,Falseotherwise.
- Collects all symbols appearing in either
Each puzzle script imports everything from logic.py (from logic import *) and then:
- Defines a set of
Symbolobjects to represent atomic propositions. - Builds a knowledge base
knowledgeusingAnd,Or,Not,Implication, andBiconditional. - Uses
model_checkto determine which symbols are entailed by the knowledge base.
A minimal example involving three symbols:
rain,hagrid,dumbledore– propositional variables.knowledge– anAndof:Implication(Not(rain), hagrid)– if it is not raining, Hagrid visits.Or(hagrid, dumbledore)– either Hagrid or Dumbledore will visit.Not(And(hagrid, dumbledore))– not both visit at once.dumbledore– Dumbledore does visit.
The script prints the result of model_check(knowledge, rain), answering whether it must be raining given these
constraints.
Models four people and four Hogwarts houses using symbols like "GilderoyGryffindor".
people = ["Gilderoy", "Pomona", "Minerva", "Horace"]houses = ["Gryffindor", "Hufflepuff", "Ravenclaw", "Slytherin"]symbols– all combinations of person–house symbols.knowledge– anAnd()initially, then extended with constraints:- Each person belongs to some house (an
Orover four house symbols per person). - Only one house per person (implications that prevent a person from being in two houses at once).
- Only one person per house (implications that prevent two people from sharing a house).
- Additional clues:
Gilderoyis inGryffindororRavenclaw.Pomonais not inSlytherin.Minervais definitely inGryffindor.
- Each person belongs to some house (an
Finally, the script loops over all symbols and prints those for which model_check(knowledge, symbol) is true—
these represent assignments that are logically forced by the knowledge base.
Uses characters, rooms, and weapons as symbols, and colors the output:
- Symbols:
- Characters:
ColMustard,ProfPlum,MsScarlet - Rooms:
ballroom,kitchen,library - Weapons:
knife,revolver,wrench
- Characters:
check_knowledge(knowledge)– helper function that:- Iterates over all symbols.
- Prints
"symbol: YES"in green ifmodel_check(knowledge, symbol)is true (entailed by the knowledge). - Prints
"symbol: MAYBE"if neither the symbol nor its negation is entailed.
The knowledge base encodes:
- There must be exactly one character, one room, and one weapon.
- Some initial cards that are known not to be in the solution.
- Additional constraints about unknown and known cards.
Running the script prints the logical status (YES/MAYBE) of each candidate solution component.
Encodes a simple Mastermind game with four positions (0–3) and four colors (red, blue, green, yellow).
- Symbols like
"red0","blue1", etc., represent a specific color in a specific position. - Knowledge base includes:
- Each color has exactly one position.
- Each position has exactly one color.
- Complex constraints representing feedback from previous guesses (encoded as large
OrofAndexpressions). - Additional constraints excluding certain color–position pairs.
The script prints any color-position symbols that are entailed by the knowledge base, revealing which colors
must be in which positions.
-
Clone or download this repository.
-
Create and activate a virtual environment (recommended):
python3 -m venv venv source venv/bin/activate # On Windows: venv\\Scripts\\activate
-
Install dependencies using
pipandrequirements.txt:pip install -r requirements.txt
The only external library currently required is termcolor, used by clue.py for colored terminal output.
All scripts are simple command-line programs that can be run directly with Python. Make sure you are in the project directory and that your virtual environment (if any) is activated.
Harry/Hagrid puzzle
python harry.pyThis prints either True or False, indicating whether the knowledge base entails that it is raining.
Hogwarts house puzzle
python puzzle.pyThis prints any person–house symbols that are logically forced by the constraints, for example:
MinervaGryffindor
...
Clue puzzle
python clue.pyThis prints lines such as:
ColMustard: MAYBE
ProfPlum: YES
kitchen: MAYBE
...
where : YES entries are printed in green (via termcolor).
Mastermind puzzle
python mastermind.pyThis prints color–position assignments that must be true given the encoded Mastermind constraints, for example:
red0
blue1
green2
yellow3
(Actual output depends on the encoded constraints.)
You can also import logic.py into your own scripts to model new puzzles.
from logic import Symbol, And, Or, Not, Implication, model_check
# Define symbols
rain = Symbol("rain")
sprinkler = Symbol("sprinkler")
wet = Symbol("wet")
# Knowledge base: if it rains or the sprinkler is on, then it is wet
knowledge = And(
Implication(Or(rain, sprinkler), wet),
rain # we know it is raining
)
# Query: does the knowledge base entail that it is wet?
print(model_check(knowledge, wet)) # True-
Import the logic primitives:
from logic import *
-
Define your symbols and knowledge base:
a = Symbol("A") b = Symbol("B") knowledge = And( Implication(a, b), a )
-
Use
model_checkto ask whether certain propositions are entailed:print(model_check(knowledge, b)) # True print(model_check(knowledge, Not(b))) # False
- Minimal, self-contained propositional logic library.
- Support for standard logical connectives: NOT, AND, OR, IMPLIES, IFF.
- Exhaustive model checking to determine entailment of a query from a knowledge base.
- Helper utilities to:
- Generate readable formulas.
- Collect symbol sets from complex sentences.
- Multiple example scripts demonstrating:
- A small reasoning example (
harry.py). - A house-assignment puzzle (
puzzle.py). - A Clue-style deduction puzzle with colored output (
clue.py). - A Mastermind-style puzzle (
mastermind.py).
- A small reasoning example (
- Python: 3.8+ (the code uses only standard features; any modern Python 3 version should work).
- External packages:
termcolor(listed inrequirements.txt) – only required forclue.pyto print colored output.
There are no other non-standard dependencies.
- Example puzzle scripts:
harry.py– minimal entailment example.puzzle.py– house-assignment puzzle.clue.py– Clue/Cluedo logic puzzle with colored output.mastermind.py– Mastermind-style puzzle.
- Slides/notes:
lecture.pdf(if provided with the repository) likely explains the underlying concepts of propositional logic and model checking used in this project.
To explore further, you can extend these scripts or create new ones that encode your own logic puzzles using the
logic.py primitives.