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 CNF conversion, and validates logical formulas.
Key Features: Support for multi-character variables, efficient tree construction, CNF conversion with parse tree generation, and tautology detection.
Implementation Statistics
7
Core Tasks
O(n)
Average Complexity
1000+
Variables Supported
16MB
Stack Size
Task Analysis
Task 1
Infix to Prefix Conversion
Converts propositional logic expressions from infix to prefix notation using a modified
Shunting Yard algorithm.
Time: O(N)
Space: O(N)
Time: O(N)
Space: O(N)
Task 2
Parse Tree Construction
Builds a rooted binary parse tree from prefix expressions with support for multi-character
variables.
Time: O(T)
Space: O(T)
Time: O(T)
Space: O(T)
Task 3
Infix Reconstruction
Traverses the parse tree using in-order traversal to reconstruct the original infix
expression.
Time: O(M)
Space: O(H)
Time: O(M)
Space: O(H)
Task 4
Tree Height Computation
Calculates the height of the parse tree using recursive depth-first traversal.
Time: O(M)
Space: O(H)
Time: O(M)
Space: O(H)
Task 5
Truth Value Evaluation
Evaluates propositional formulas given truth assignments using bottom-up tree
traversal.
Time: O(M)
Space: O(H+V)
Time: O(M)
Space: O(H+V)
Task 6
CNF Conversion
Converts any propositional formula to Conjunctive Normal Form using IMPL_FREE, NNF, and
distribution.
Time: Exponential
Space: Exponential
Time: Exponential
Space: Exponential
Task 7
CNF Validity Check
Validates CNF formulas and identifies tautological clauses by checking for complementary
literals.
Time: O(M)
Space: O(M)
Time: O(M)
Space: O(M)
Docs
Doxygen Documentation
Auto-generated documentation for all C++ source files, including call graphs and file structures.
Time Complexity Analysis
Tasks 1-5, 7: Linear O(n)
Efficient single-pass or tree traversal algorithms with linear time complexity
Task 6: Exponential
CNF conversion requires exponential time due to distribution operations in worst case