Propositional Logic Parser and Checker

Version: 1.0.0

A C++ library and tool for parsing and analyzing logical formulas.

Project Overview

This project implements a comprehensive propositional logic parser and analyzer capable of handling complex logical formulas. The system converts infix expressions to prefix notation, builds parse trees, performs Conjunctive Normal Form (CNF) conversion, and validates logical formulas.

Key Features

• Support for multi-character variables.

• Efficient parse tree construction from prefix expressions.

• Conversion of any propositional formula to CNF.

• Tautology detection and CNF validity checking.

Project Documentation

A live website containing a detailed analysis of the project's tasks and the complete Doxygen-generated documentation can be found at the following link:

Project Analysis and Documentation Website

Core Tasks Implemented

1. Infix to Prefix Conversion: Converts standard logical expressions into prefix (Polish) notation.

2. Parse Tree Construction: Builds a binary tree representation from a prefix expression.

3. Infix Reconstruction: Reconstructs the original infix expression from the parse tree.

4. Tree Height Computation: Calculates the height of the generated parse tree.

5. Truth Value Evaluation: Evaluates a formula's truth value given an assignment for its variables.

6. CNF Conversion: Transforms any formula into its equivalent Conjunctive Normal Form.

7. CNF Validity Check: Validates CNF formulas and identifies tautological (trivial) clauses.

Authors

• Bhavya Shah (2024A7PS0139H)

• Prathamesh Patil (2024A7PS0052H)

• Sahitya Sharma (2024A7PS0096H)

• Krish Vasa (2024A7PS0106H)