Boolean Expressions (Cboolexp)

THEOREM PROVER

Description

This is a simple propositional logic theorem prover build using tableaux method. Theorem is inserted using the customizable set of notations as follows.

AND: ^

OR : +

NOT: ~

IMPLY: >

EQUAL: =

NECESSITY : #

POSSIBLITY: @

Boolean Expressions (CBoolExp)

Boolean expressions are stored in CBoolExp class. The expression is stored using tree of nodes.

Ex :-#(A+B) ^ (C>D)

When the expression is stored like this, it is easy to make inference rules.

Input expression from the user is inserted as a string. Then the string is converted to postfix. The postfix expression is then converted to the expression tree.

(i.e. CBoolExp::setStr()).

Inference are applied using infer function. The tree is split from the operator and two expressions are created. Then the two expressions are added to the solution tree.

The inference is special to the Necessity and Possibility. They take i, j as inputs. The world stores the i value of the expression. Finding irj is not a part of the CBoolExp class. They are found through the CSolution class.

When inferring, NOT is considered with relative to the next operator after next. So it is dissolved in two steps. First step dissolves NOT and second step dissolves the next operator.

Solution (CSolution)

Solution is stored at CSolution class. First the expressions are added to the solution. Then the theorem is solved by inferring expressions and adding to the ends of the left and right branches.

Boolean expressions to be solved are stored in a queue. So the one by one expression to be inferred gets simplified.

The solution is also stored as a tree. Each expression inferred is added to the end of the tree (each branch). This tree also hosts a parent pointer to point to the upper node.

CSolution class has a queue called open queue which stores expressions to be inferred. The function solve in CSolution take each expression in open queue and infers them and then stores the results in the tree.

The inferring part is done by the CBoolExp class. The results are added by the CSolution class.

This class has two functions findirj and findirjup to find irj kind of node. When inferring Necessity or Possibility these two functions are used.

Displaying the solution tree is also done by this class using draw and drawNode function. The draw function uses drawNode draw each type of expression one by one.

GUI (CTProverView)

The complexity of the GUI is covered by designing program modularly. The only function to be considered is CTPrverView::OnFileNew(). All the work is done by this function with the aid of CSolution and CBoolExp.

Expressions can be added by typing in textbox and pressing Alt+A.