The Intelligent Logic Verification and Automated Reasoning Toolkit is a software application designed to automatically solve and verify problems in propositional and predicate logic.
The project is being developed as part of the CE 474 – Logic of Computer Science Group Project 2 at the University of Mines and Technology (UMaT).
The toolkit focuses on practical implementation of logic-solving algorithms and formal verification techniques. It aims to provide users with an easy-to-use interface for entering logical expressions, performing automated reasoning, and understanding the results.
The main objective of this project is to develop a web-based application capable of automatically solving propositional and predicate logic problems.
The system will provide tools for:
- Generating truth tables
- Checking logical equivalence
- Converting formulas into Conjunctive Normal Form (CNF)
- Performing resolution-based reasoning
- Checking satisfiability of logical formulas
- Translating simple English statements into predicate logic
- Supporting different proof strategies
- Providing a user-friendly graphical interface
Accepts a propositional logic formula and automatically generates its complete truth table.
Example:
(P → Q) ∧ (Q → R)
The system generates all possible truth assignments and evaluates the formula.
Determines whether two logical expressions are logically equivalent by comparing their truth values under all possible interpretations.
Example:
P → Q
¬P ∨ Q
The system determines whether both expressions have identical truth values.
Converts logical expressions into an equivalent Conjunctive Normal Form (CNF).
Example:
(P → Q)
The system transforms the expression into its equivalent CNF representation.
Accepts premises and a conclusion and uses resolution-based reasoning to determine whether the conclusion is:
- Valid
- Invalid
- Unsatisfiable
Determines whether a given logical formula is satisfiable.
The implementation may use a custom SAT-solving algorithm or optionally integrate an external SAT engine.
Translates simple English statements into predicate logic representations.
Example:
Every student passed Logic.
Can be represented as:
∀x (Student(x) → Passed(x, Logic))
Supports different proof strategies, including:
- Direct Proof
- Proof by Contradiction
- Proof by Contrapositive
- Natural Deduction (optional)
The application will provide a graphical interface with:
- Logical expression input
- Syntax highlighting
- Error detection
- Clear output presentation
- Result explanations
- User-friendly interaction
The proposed system will follow a flow similar to:
┌──────────────────┐
│ User Input │
└────────┬─────────┘
│
▼
┌──────────────────┐
│ Parser │
└────────┬─────────┘
│
▼
┌──────────────────────────────┐
│ Internal Formula Representation│
└──────────────┬───────────────┘
│
▼
┌──────────────────┐
│ Reasoning Engine │
└────────┬─────────┘
│
┌──────────────┼──────────────┐
▼ ▼ ▼
Truth Table CNF/SAT Resolution/
Solver Solver Proof Engine
│ │ │
└──────────────┼──────────────┘
▼
┌──────────────────┐
│ Output Display │
└──────────────────┘
The project may be implemented using one or more of the permitted programming languages:
- Python
- Java
- C#
- JavaScript
- C++
Possible supporting tools include:
- Visual Studio Code
- GitHub
- SWI-Prolog
- Graphviz
- MiniSAT
- Z3 SMT Solver (Bonus)
- Prover9 (Bonus)
intelligent-logic-verification-toolkit/
│
├── src/
│ ├── parser/
│ ├── truth_table/
│ ├── cnf_converter/
│ ├── resolution/
│ ├── sat_solver/
│ ├── predicate_logic/
│ ├── proof_assistant/
│ └── gui/
│
├── tests/
│
├── docs/
│ ├── architecture/
│ ├── technical_report/
│ └── installation_guide/
│
├── README.md
├── requirements.txt
└── .gitignore
| Role | Responsibility |
|---|---|
| Project Manager | Coordinates the team, manages milestones and oversees project progress |
| GUI Developer | Designs and implements the graphical user interface |
| Truth Table Developer | Develops the truth table generation module |
| CNF Converter Developer | Implements CNF conversion algorithms |
| Resolution Developer | Develops the resolution theorem prover |
| SAT Solver Developer | Implements the SAT-solving functionality |
| Predicate Logic Developer | Develops the predicate logic translation module |
| Testing Lead | Designs and manages system testing |
| Documentation Lead | Maintains technical documentation and reports |
| Presentation & Integration Lead | Coordinates integration and prepares the final presentation |
To keep development organized, team members should avoid making changes directly to the main branch.
Each major feature should have its own branch.
Example:
main
│
└── develop
├── feature/truth-table
├── feature/cnf-converter
├── feature/resolution
├── feature/sat-solver
├── feature/predicate-logic
└── feature/gui
- Clone the repository.
- Create or switch to your assigned feature branch.
- Implement your changes.
- Test your changes.
- Commit your work with a clear commit message.
- Push the branch to GitHub.
- Create a Pull Request.
- Request a review before merging into
develop.
git clone <repository-url>
git checkout develop
git checkout -b feature/truth-table
git add .
git commit -m "Implement truth table generator"
git push origin feature/truth-tableTesting will be carried out throughout development to ensure that:
- Logical expressions are parsed correctly.
- Algorithms produce correct results.
- Invalid or malformed formulas are handled appropriately.
- Individual modules work as expected.
- Modules work correctly after integration.
- The graphical interface responds correctly to user input.
| Milestone | Status |
|---|---|
| Project planning | 🟡 In Progress |
| System architecture | ⬜ Pending |
| Parser development | ⬜ Pending |
| Truth table module | ⬜ Pending |
| CNF converter | ⬜ Pending |
| Resolution module | ⬜ Pending |
| SAT solver | ⬜ Pending |
| Predicate logic module | ⬜ Pending |
| Proof assistant | ⬜ Pending |
| GUI development | ⬜ Pending |
| Module integration | ⬜ Pending |
| System testing | ⬜ Pending |
| Documentation | ⬜ Pending |
| Final presentation & demonstration | ⬜ Pending |
The project will produce:
- Source code
- Executable application
- GitHub repository
- Technical report
- Installation guide
- Testing report
- Presentation slides
- Live demonstration
According to the project brief, all group deliverables are to be placed in a single folder named after the group, compressed into a ZIP archive, and submitted to the class/group representative on or before 14 August 2026.
Course: CE 474 – Logic of Computer Science Project: Group Project 2 Project Title: Intelligent Logic Verification and Automated Reasoning Toolkit Institution: University of Mines and Technology (UMaT) Department: Computer Science & Engineering
Add the names and GitHub usernames of all team members below:
| # | Name | Role | GitHub |
|---|---|---|---|
| 1 | [Your Name] | Project Manager | @username |
| 2 | [Member Name] | GUI Developer | @username |
| 3 | [Member Name] | Truth Table Developer | @username |
| 4 | [Member Name] | CNF Converter Developer | @username |
| 5 | [Member Name] | Resolution Developer | @username |
| 6 | [Member Name] | SAT Solver Developer | @username |
| 7 | [Member Name] | Predicate Logic Developer | @username |
| 8 | [Member Name] | Testing Lead | @username |
| 9 | [Member Name] | Documentation Lead | @username |
| 10 | [Member Name] | Presentation & Integration Lead | @username |
This repository is maintained as part of the CE 474 Logic of Computer Science Group Project 2 and will contain the source code, documentation, testing materials, and other project deliverables.
Built with teamwork, logic, and a little bit of debugging pain. 😅💻