Algebraic approach to logical inference implementation

Algebraic Approach to Logical Inference Implementation

1319

B · N

M −1

given that every intersection is nonempty. This estimate is evidently

greater than the one for a problem of CNF satisfiability.

Transformation of D-systems into C-systems is of most interest for implemen-

tation of logical inference, since in NTA a D-system is isomorphic to a CNF and

a C-system can be considered a set of satisfying substitutions for this CNF. Hence

for this transformation we need to solve a problem of CNF satisfiability, one of the

most popular problems in applications of logical inference theory and computational

complexity theory. This solution is clearly redundant as it gives all elementary n-

tuples or C-tuples contained in the D-system, while it would be enough to find only

one of them to declare the D-system is not empty; but the solution is acceptable

when some analysis of satisfying substitutions is needed beside determining of the

CNF satisfiability.

In practice, a CNF satisfiability (D-system emptiness) check is the initial stage

of any algorithm for transformation of a D-system into a C-system since the trans-

formation makes sense only if the initial D-system is not empty. This stage can be

the only one if no analysis of satisfying substitutions is required. A CNF satisfiabi-

lity check is also performed during enclosure checks for NTA objects; moreover, it

is the main source of complexity in this case.

The material stated above lets us conclude that in NTA, as well as in many

other logical systems, a laboriousness decrease for the problem of CNF satisfiability

allows to shorten not only certain steps of logical inference algorithms, but also the

whole inference procedure, if it can be reduced to the said problem.

In NTA, a decrease in laboriousness and sometimes in computational complexity

as well, is mostly realized by using matrix properties of NTA objects; we are now

going to describe these properties below.

5.2 Matrix Properties of NTA Objects (Case Study: CNF Satisfiability)

In artificial intelligence systems, CNF satisfiability is an important problem for the

following reasons:

1. In complexity theory, CNF satisfiability is the basic NP-complete problem. It

has been proven that, using rational coding, any NP-class problem can be rep-

resented as a CNF, and that converting any NP-class problem to CNF takes

polynomial time.

2. Based on Theorem 17, the resolution principle was stated for both propositional

and predicate calculus; this principle is now widely used in machine implemen-

tations of artificial intelligence systems. According to this principle, the formula

F

1

∧ . . . ∧ F

n

∧ ¬G is converted to CNF, and logical inference is narrowed down

to solving a CNF satisfiability problem.

Thus, it is important to find new CNF classes with a polynomially recognizable

satisfiability property.

---

1320

B. Kulik, A. Fridman, A. Zuenko

NTA structures (n-tuples and systems of n-tuples) look like matrices. Although

operations on NTA objects are substantially different from matrix-algebra opera-

tions, the former have many properties of matrix structures, which can be used to

reduce laboriousness in many NTA operations, e.g. in solving the problem of CNF

satisfiability/emptiness of a D-system.

Let an arbitrary D-n-tuple = ]s

1

s

2

. . . s

n

[ be given. If the set of its compo-

nents can be divided into R nonempty nonintersecting subsets that make up D-n-

tuples D

j

, then

D =

R

j=1

D

j

.

For example, if a D-n-tuple ]s

1

s

2

s

3

s

4

s

5

s

6

s

7

[ is split into three D-n-tuples ]s

2

s

4

s

6

[,

]s

1

s

3

s

5

[ and ]s

7

[, reducing these to the same relation diagram transforms them into

D-n-tuples ]Øs

2

Øs

4

Øs

6

Ø[, ]s

1

Øs

3

Øs

5

ØØ[ and ]ØØØØØØs

7

[. Union of these rela-

tions equals the initial D-n-tuple.

Similarly, under the same splitting conditions, for C-n-tuples C, C

i

it is true

that

C =

R

j=1

C

j

.

Let T be a D-system represented as a matrix of components whose dimensions

are M × N (M rows and N columns). Let us divide this D-system into R vertical

blocks R (j = 1, 2, . . . , R) by vertical lines. Let D

i

(i = 1, 2, . . . , M ) be a D-n-tuple

that is represented by the i

th

row of the matrix T , then T =

M

i=1

D

i

. Let D

ij

denote the D-n-tuple represented by a subrow of the i

th

row from the j

th

block in

the matrix T . Then, D

i

=

R

j=1

D

ij

, and T =

M

i=1

R

j=1

D

ij

. By removing the

brackets in the last equation, we get the relation stated in the following theorem.

Theorem 18. If a D-system matrix T with dimensions M × N is divided into R

vertical blocks (R < N ), the following is true:

T =

S

j=1

M

i=1

D

ij

,

where S = R

M

.

One of the corollaries to the Theorem 18 is that a D-system is nonempty if at

least one D-system

M

i=1

D

ij

is nonempty, whatever the division into vertical blocks

is. For example, D-system

t

11

t

12

t

13

t

14

t

21

t

22

t

23

t

24

is divided into two vertical blocks.

In accordance with the theorem, it can be represented as a union of four D-systems

t

11

Ø

Ø

Ø

∪

Ø

t

12

t

13

t

14

∩

t

21

Ø

Ø

Ø

∪

Ø

t

22

t

23

t

24

---