Skip to content

This project is a small logic engine and set of example programs that model and solve propositional-logic puzzles.

Notifications You must be signed in to change notification settings

ealbertoav/knowledge

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

2 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Knowledge-Based Logic Puzzles

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.


Purpose

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.


Project Structure

  • logic.py
    Core logic library. Defines the sentence hierarchy (Sentence, Symbol, Not, And, Or, Implication, Biconditional) and the model_check function 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. Uses termcolor to 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 only termcolor for colored terminal output used by clue.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.


Key Components

Core Logic Library (logic.py)

Classes

  • EvaluationException(Exception)
    Custom exception raised when evaluating a Symbol with 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 (a dict mapping symbol names to booleans).
    • formula() – returns a string representation of the sentence (subclasses override this).
    • symbols() – returns a set of symbol names appearing in the sentence (subclasses override this).
    • validate(sentence) – class method that checks an object is a Sentence instance, raising TypeError otherwise.
    • parenthesize(s) – helper that adds parentheses around an expression s when 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) – returns bool(model[name]); raises EvaluationException if 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 that operand is a Sentence and stores it.
    • evaluate(model) – returns logical negation of the operand’s value.
    • formula() – returns "¬" followed by a parenthesized subformula.
    • symbols() – forwards to the operand’s symbols().
  • 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) – returns True only if all conjuncts evaluate to True.
    • 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) – returns True if any disjunct evaluates to True.
    • 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)
    Represents antecedent => 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)
    Represents left <=> right (logical equivalence).

    • __init__(left, right) – validate and store both sides.
    • evaluate(model)True when both sides are true or both are false.
    • formula() – returns "(left) <=> (right)" (using each side’s formula()).
    • symbols() – union of symbols from both sides.

Functions

  • model_check(knowledge, query)
    Given a knowledge base knowledge (a Sentence) and a proposition query (another Sentence), performs exhaustive model checking to decide whether knowledge entails query.

    Behaviour:

    • Collects all symbols appearing in either knowledge or query.
    • Recursively considers every possible truth assignment (model) for those symbols.
    • For every model, if knowledge.evaluate(model) is true, then it requires that query.evaluate(model) is also true; otherwise the entailment fails.
    • Returns True if the entailment condition holds for all models, False otherwise.

Example Puzzles

Each puzzle script imports everything from logic.py (from logic import *) and then:

  1. Defines a set of Symbol objects to represent atomic propositions.
  2. Builds a knowledge base knowledge using And, Or, Not, Implication, and Biconditional.
  3. Uses model_check to determine which symbols are entailed by the knowledge base.

harry.py

A minimal example involving three symbols:

  • rain, hagrid, dumbledore – propositional variables.
  • knowledge – an And of:
    • 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.

puzzle.py (Hogwarts House Puzzle)

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 – an And() initially, then extended with constraints:
    • Each person belongs to some house (an Or over 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:
      • Gilderoy is in Gryffindor or Ravenclaw.
      • Pomona is not in Slytherin.
      • Minerva is definitely in Gryffindor.

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.

clue.py (Mini Clue/Cluedo Puzzle)

Uses characters, rooms, and weapons as symbols, and colors the output:

  • Symbols:
    • Characters: ColMustard, ProfPlum, MsScarlet
    • Rooms: ballroom, kitchen, library
    • Weapons: knife, revolver, wrench
  • check_knowledge(knowledge) – helper function that:
    • Iterates over all symbols.
    • Prints "symbol: YES" in green if model_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.

mastermind.py (Mastermind-style Puzzle)

Encodes a simple Mastermind game with four positions (03) 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 Or of And expressions).
    • 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.


Installation

  1. Clone or download this repository.

  2. Create and activate a virtual environment (recommended):

    python3 -m venv venv
    source venv/bin/activate  # On Windows: venv\\Scripts\\activate
  3. Install dependencies using pip and requirements.txt:

    pip install -r requirements.txt

The only external library currently required is termcolor, used by clue.py for colored terminal output.


Usage

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.

Running the Example Puzzles

Harry/Hagrid puzzle

python harry.py

This prints either True or False, indicating whether the knowledge base entails that it is raining.

Hogwarts house puzzle

python puzzle.py

This prints any person–house symbols that are logically forced by the constraints, for example:

MinervaGryffindor
...

Clue puzzle

python clue.py

This prints lines such as:

ColMustard: MAYBE
ProfPlum: YES
kitchen: MAYBE
...

where : YES entries are printed in green (via termcolor).

Mastermind puzzle

python mastermind.py

This 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.)


Programmatic Usage

You can also import logic.py into your own scripts to model new puzzles.

Basic Example

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

Creating a New Puzzle Script

  1. Import the logic primitives:

    from logic import *
  2. Define your symbols and knowledge base:

    a = Symbol("A")
    b = Symbol("B")
    knowledge = And(
        Implication(a, b),
        a
    )
  3. Use model_check to ask whether certain propositions are entailed:

    print(model_check(knowledge, b))      # True
    print(model_check(knowledge, Not(b))) # False

Features

  • 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).

Requirements

  • Python: 3.8+ (the code uses only standard features; any modern Python 3 version should work).
  • External packages:
    • termcolor (listed in requirements.txt) – only required for clue.py to print colored output.

There are no other non-standard dependencies.


Examples and Further Reading

  • 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.

About

This project is a small logic engine and set of example programs that model and solve propositional-logic puzzles.

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages