This repository contains the implementation of a Forward Search (Forward Chaining) algorithm designed to solve propositional logic problems. The system takes a knowledge base (a set of known facts and implication rules) and a query, then iteratively infers new knowledge to prove or disprove the query.
This project was completed as part of the SE_14 Artificial Intelligence Basics module assessment.
The codebase is organized into the following components:
-
main.py: The entry point of the application. It defines several logic test problems (knowledge bases + queries) and compares the performance of the custom Forward Search algorithm against a reference Model Checker. -
solvers/: Contains the core algorithms.-
forward_search.py: My implementation of the Forward Search algorithm. -
model_check.py: The reference model checking algorithm used for verification and performance comparison.
-
-
logic/: Contains the classes representing propositional logic components.-
symbol.py: Represents atomic logical symbols (e.g., A, B). -
sentence.py: Base class for logical sentences. -
implication.py,biconditional.py,conjunction.py,disjunction.py,negation.py: Implementations of logical connectives.
-
- Python 3.x: This project relies on the Python standard library. No external dependencies (like
numpyorpandas) are required.
-
Open your terminal or command prompt.
-
Navigate to the root directory of this repository (where
main.pyis located). -
Execute the main script:
python main.py
The script will run 5 test problems sequentially. For each problem, it will:
-
Run the Model Checking algorithm (Reference).
-
Run the Forward Search algorithm (My Implementation).
-
Display the result (
True,False, orNone) and the execution time for both.
Example Output:
Testing Problem 2
... running model checking
... running forward search
... done.
- result - model checking: True
- result - forward search: True
- time for model checking 25720500 ns
- time for forward search 0 ns
The Forward Search algorithm (solvers/forward_search.py) utilizes a data-driven approach:
-
It repeatedly scans the knowledge base for
ImplicationandBiconditionalrules. -
If the premises of a rule are satisfied by currently known facts, the conclusion is inferred and added to the knowledge base.
-
This process repeats until the query is proven, disproven, or no further inferences can be made.