Project is inspired by book "Automatyczne dowodzenie twierdzeń" authored by Polish mathematician Zdzisław Pawlak. More about main conjunction you can find here: Klasyczny rachunek zdań.
How formula element's value is calculated:
F(x_<sub>1</sub>) = 0.F(x_<sub>i+1</sub>) = F(x_<sub>i</sub>) + 1whenF(x_<sub>i</sub>) IN {"(" "a" "b" "c" ...}.F(x_<sub>i+1</sub>) = F(x_<sub>i</sub>) - 1whenF(x_<sub>i</sub>) IN {")" "OR" "AND" "IMPL" "IFF"}.F(x_<sub>i+1</sub>) = F(x_<sub>i</sub>)whenF(x_<sub>i</sub>) IN {"NOT"}.
Main conjunction (except first and last bracket) has value 0.
Let f be the formula: ( p AND ( q OR r ) )
We can present formula f as a tree:
( p AND ( q OR r ) )
/ \
p ( q OR r )
/ \
q r
In this example main conjunction is AND (3 index in formula). The calculated values for the formula is: [0 1 0 1 2 1 2 1 0].
Let f be the formula: ( ( NOT ( p OR q ) OR q ) AND ( p AND NOT r ) )
Table presents calculated values:
| ( | ( | NOT | ( | p | OR | q | ) | OR | q | ) | AND | ( | p | AND | NOT | r | ) | ) | |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 | 16 | 17 | 18 | 19 | |
| 0 | 1 | 1 | 2 | 3 | 2 | 3 | 2 | 1 | 2 | 1 | 0 | 1 | 2 | 1 | 1 | 2 | 1 | 0 |
In this example main conjunction is also AND (12 index in formula).