Logical Expressions
ArboreAbstract_FormaFinala.py:
-converts the logical expression from relaxed syntax to strict syntax
-checks whether the inserted logical expression is valid
-displays the step of building the abstract tree of the logical expression
-shows the truth table of the logical expression
heuristic_algorithm_for_expression_simplification.py:
-converts the logical expression from relaxed syntax to strict syntax
-checks whether the inserted logical expression is valid
-simplifies the logical expression using the laws of reduction, comutativity, associativity, idempotency, anihilation, distributivity and absortion
QuineMcCluskey+Petricksalgorithmforminimizi.py:
-converts the logical expression from relaxed syntax to strict syntax
-checks whether the inserted logical expression is valid
-simplifies the logical expression using the Quine-McCluskey algorithm using Petrick's method
ResolutionMethod.py:
-converts the logical expression from relaxed syntax to strict syntax
-checks whether the inserted logical expression is valid
-converts the logical expression to CNF
-checks its satisfiability using the Resolution Method
DavisPutnam.py:
-converts the logical expression from relaxed syntax to strict syntax
-checks whether the inserted logical expression is valid
-converts the logical expression to CNF
-checks its satisfiability using the Resolution Method with David Putnam's optimisation
DPLL.py:
-converts the logical expression from relaxed syntax to strict syntax
-checks whether the inserted logical expression is valid
-converts the logical expression to CNF
-checks its satisfiability using DPLL