This project has been created as part of the 42 curriculum by iberegsz, ajovanov.
A backward-chaining inference engine for propositional calculus, implementing a complete expert system that can reason about logical rules and facts.
This repository implements a backward-chaining expert system for propositional calculus. Its goal is to parse a small propositional-language, perform logical inference (backward-chaining) over user-supplied rules and facts, and answer queries about fact truth values. The implementation supports standard Boolean operators, parentheses, operator precedence, and detects syntax errors, contradictions and cycles.
The system is intended for educational purposes (42 curriculum) and provides: parsing, reasoning, debugging support and optional visualization of reasoning paths.
This is a 42 School project that implements an expert system capable of:
- Backward-chaining inference: Determining if queries are true, false, or undetermined based on given rules and facts
- Full propositional logic: Supporting AND, OR, XOR, NOT, IMPLIES, and biconditional (IFF) operators
- Complex expressions: Handling parentheses and operator precedence
- Error detection: Identifying contradictions, circular dependencies, and syntax errors
Summary: The goal of this project is to create an expert system for propositional calculus.
Version: 3.3
- Data Structure: Global knowledge graph with explicit fact nodes and rule nodes
- O(1) lookup for rules concluding/using facts
- Bidirectional edges for efficient traversal
- Foundation for proof visualization and dependency analysis
- AND conditions:
A + B => C(if A and B then C) - OR conditions:
A | B => C(if A or B then C) - XOR conditions:
A ^ B => C(if A xor B then C) - exclusive OR - Negation:
!A(NOT A),A + !B => C(if A and not B then C) - Multiple rules with same conclusion: Multiple rules can conclude the same fact
- AND in conclusions:
A => B + C(if A then B and C) - Parentheses:
(A + B) | C => Dfor grouping expressions - Biconditional rules:
A <=> B(if and only if) - Backward-chaining inference: Efficient reasoning from queries back to facts
- Error handling: Syntax errors, contradictions, and cycle detection
- Interactive Fact Validation: Change facts interactively without modifying files
- Reasoning Visualization: Detailed explanations with formal logic notation
- OR/XOR in Conclusions: Support for
A => B | CandA => B ^ C - Biconditional Rules: Full
<=>operator support (if and only if) - Statistics Analyzer: Comprehensive metrics and complexity analysis
- Graph Exporter: Export reasoning paths as graphs (DOT/Graphviz)
- Debug Tool: Display parsed rules and AST structure
- Trace Tool: Basic trace of evaluation steps for debugging
- Comprehensive Test Suite: 12+ test files covering all features and edge cases
- EBNF Grammar Specification: Complete formal grammar with railroad diagrams in BottleCaps-compatible format
The system is built with three main components:
- Lexer (
lexer.py): Tokenizes input according to the language specification - Parser (
parser.py): Builds an Abstract Syntax Tree (AST) respecting operator precedence - Inference Engine (
inference_engine.py): Performs backward-chaining inference to evaluate queries
The expert system language follows a formal EBNF grammar specification.
Grammar summary:
Start = Line*Line = Initials | Queries | RuleRule = Expression ('=>' | '<=>' ) ExpressionExpression = Iff(with full precedence chain)- Facts are single uppercase letters:
IDENT = /[A-Z]/
Operators are listed in order of decreasing priority (highest to lowest):
()- Parentheses (grouping)!- NOT (negation)+- AND (conjunction)|- OR (disjunction)^- XOR (exclusive OR)=>- IMPLIES (implication)<=>- IFF (biconditional, if and only if)
- AND (
A + B): True if both A and B are true - OR (
A | B): True if at least one of A or B is true - XOR (
A ^ B): True if exactly one of A or B is true (not both) - NOT (
!A): True if A is false, false if A is true - IMPLIES (
A => B): False only when A is true and B is false - IFF (
A <=> B): True when both have the same truth value
The engine can determine three possible truth values:
- TRUE: The fact is provably true
- FALSE: The fact is provably false (default for unknown facts)
- UNDETERMINED: Cannot determine due to insufficient information
Run the main program with an input file containing rules, initial facts and queries:
python3 expert_system.py <input_file>python3 interactive_mode.py <input_file>
# Commands: +A (add), -A (remove), ?A (query), facts, reset, quitpython3 reasoning_visualizer.py <input_file>
# Shows detailed step-by-step reasoning with formal logicpython3 statistics_analyzer.py <input_file>
# Provides complexity metrics and rule analysisThe input file contains three sections:
- Rules: Logical rules using operators (one per line)
- Initial Facts: Facts that are known to be true (line starting with
=) - Queries: Facts to evaluate (line starting with
?)
Example:
# This is a comment
C => E # C implies E
A + B + C => D # A and B and C implies D
A | B => C # A or B implies C
A + !B => F # A and not B implies F
V ^ W => X # V xor W implies X
A + B => Y + Z # A and B implies Y and Z
A + B <=> C # A and B if and only if C
=ABG # Initial facts: A, B, and G are true
?GVX # Queries: What are G, V, and X?
Output:
============================================================
EXPERT SYSTEM - PROPOSITIONAL CALCULUS
============================================================
Loaded 7 rule(s)
Initial facts: A, B, G
============================================================
QUERY RESULTS
============================================================
G: ✓ TRUE
V: ✗ FALSE
X: ✗ FALSE
Comments start with # and continue to the end of the line. They can appear anywhere in the file.
Facts must be single uppercase letters (A-Z). Each fact can be:
- In the initial facts (explicitly true)
- Concluded by one or more rules
- False by default if not proven true
# Simple implication chain
A => B
B => C
C => D
=A
?D
Output: D: ✓ TRUE
A + B => C
A + B + C => D
=AB
?CD
Output: C: ✓ TRUE, D: ✓ TRUE
A ^ B => C # C is true only if exactly one of A or B is true
=A # Only A is true (not B)
?C
Output: C: ✓ TRUE
A => B
!B => C # If NOT B, then C
=A
?BC
Output: B: ✓ TRUE, C: ✗ FALSE
A <=> B # A if and only if B (they're equivalent)
B => C
=A
?ABC
Output: A: ✓ TRUE, B: ✓ TRUE, C: ✓ TRUE
(A + B) | C => D
A + (B | C) => E
=AC
?DE
Output: Both D and E will be TRUE
The project includes 12 comprehensive test files located in the test/ directory:
test/test1.txt- Complex example from subject (all features)test/test2.txt- Simple implication chainstest/test3.txt- AND conditionstest/test4.txt- OR conditions and undetermined statestest/test5.txt- XOR (exclusive OR)test/test6.txt- Negationtest/test7.txt- Parenthesestest/test8.txt- Multiple rules with same conclusiontest/test9.txt- Biconditional (if and only if)test/test10.txt- Complex example with all operatorstest/test11.txt- No initial factstest/test12.txt- AND in conclusions
Run all tests:
for i in {1..12}; do
echo "=== Test $i ==="
python3 expert_system.py test/test$i.txt
echo
doneThe inference engine uses backward chaining:
- Start with query: Begin with the fact we want to prove
- Check initial facts: If it's in the initial facts, return TRUE
- Search for rules: Find rules that can conclude this fact
- Evaluate conditions: Recursively evaluate the conditions of those rules
- Apply rules: If a condition is true, the conclusion follows
- Cache results: Memoize to avoid redundant computation
- Detect cycles: Track facts being evaluated to prevent infinite loops
This approach is efficient for queries because it only explores relevant rules rather than forward-chaining through all possible deductions.
The system detects and reports:
- Syntax errors: Invalid operators, malformed expressions
- Contradictions: Facts that are proven both true and false
- Circular dependencies: Rules that reference themselves
- Invalid facts: Facts that aren't single uppercase letters
Python was chosen for this implementation because:
- Clear syntax: Easy to express logical operations
- Rich data structures: Sets, dicts, and lists work well for logic systems
- Development speed: Rapid prototyping and testing
- Debugging: Excellent tools for tracing logical inference
- Pattern matching: Modern Python supports sophisticated pattern matching
While not the fastest language, Python provides excellent clarity and correctness for a logic system.
- Python 3.10 or higher (uses modern type hints and pattern matching features)
- No external dependencies (pure Python standard library)
- BottleCaps Railroad Diagram Generator: https://www.bottlecaps.de/rr/ui
- Official EBNF specification and reference materials (W3C / ISO resources)
- Propositional logic overview: https://en.wikipedia.org/wiki/Propositional_calculus
- Project subject and examples: docs/EXAMPLES.md and docs/QUICKSTART.md
AI assistance
-
Documentation and content edits were performed with the help of an AI assistant to speed up formatting and consistency tasks. The AI was used specifically for:
- Converting embedded railroad/mermaid diagrams into compact ASCII diagrams
- Removing embedded base64 image blobs and normalizing in-file diagrams
- Updating and unifying README and docs references (filenames, links)
- Minor copy edits and organization of documentation sections
The implementation code (lexer, parser, inference engine) and core algorithmic logic were authored and reviewed manually; AI was used only as an editorial/formatting aide.
The codebase follows:
- Type hints: All functions are fully typed
- Docstrings: Comprehensive documentation
- Clean code: Following PEP 8 style guidelines
- Modular design: Clear separation of concerns
Run individual tests:
python3 expert_system.py test/test1.txt
python3 expert_system.py test/test2.txt
# ... etc