main-conjunction

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ń.

Main conjunction

How formula element's value is calculated:

1. F(x_<sub>1</sub>) = 0.
2. F(x_<sub>i+1</sub>) = F(x_<sub>i</sub>) + 1 when F(x_<sub>i</sub>) IN {"(" "a" "b" "c" ...}.
3. F(x_<sub>i+1</sub>) = F(x_<sub>i</sub>) - 1 when F(x_<sub>i</sub>) IN {")" "OR" "AND" "IMPL" "IFF"}.
4. F(x_<sub>i+1</sub>) = F(x_<sub>i</sub>) when F(x_<sub>i</sub>) IN {"NOT"}.

Main conjunction (except first and last bracket) has value 0.

Examples

Example 1.

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].

Example 2.

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).