In logic programming, partial evaluation performs unfolding rules of a program in advance to reduce the cost of inferencing steps. Recently, partial evaluation of logic programs has been implemented in vector spaces by computing the powers of matrix representations. It has been reported that linear algebraic partial evaluation substantially enhances the practical performance of linear algebraic methods for logic programming. However, most recent research has focused exclusively on -rules, assuming that their dependency graph is acyclic. In this paper, we introduce cycle-resolving techniques to ensure that linear algebraic partial evaluation works efectively even with cycles in the program. Additionally, we demonstrate that linear algebraic partial evaluation can also be extended to accommodate -rules. Moreover, we propose using eigendecomposition and Jordan normal form to conduct the partial evaluation in vector spaces. We compare the proposed techniques on a set of acyclic and cyclic logic programs to evaluate their efectiveness. It is shown that the iteration method for partial evaluation, especially with sparse format, is the most eficient one in general cases. However, the decomposition method has the potential for future research to leverage eigenvalues and eigenvectors of program matrices for reasoning with logic programming.
Recent research has explored using linear algebraic
methods as a compelling alternative to symbolic methods for
logical inference [
Linear algebraic approaches have also been extended to
Partial Evaluation (PE) in Logic Programming (LP) [
In this work, we focus on extending the capability of linear algebraic PE. First, we propose to separate the matrix representation of a logic program into two parts: one for -rules and the other for -rules. In short, an -rule is a rule that has a conjunction of literals in its body, the head is True only if all its body literals are True. On the other hand, an -rule has a disjunction of literals in its body, the head is True if at least one of its body literals is True. Each part (-rules or -rules) of a logic program has diferent logical meanings but can be treated equally in terms of PE computation which is basically computing powers of a square matrix. We also propose a solution to resolve cycles in the dependency graph of the program to extend the capability of linear algebraic PE to the cyclic case. Moreover, we introduce a novel way to realize PE in vector spaces by leveraging the eigenvalues and eigenvectors.
The rest of this paper is organized as follows: Section 2 reviews background knowledge of LP and dependency graphs; Section 4 presents the iteration method for PE and cycleresolving techniques; Section 5 demonstrates linear algebraic PE using eigendecomposition and Jordan normal form; Section 6 illustrates comparison of the proposed PE methods; finally Section 7 concludes the paper.
In this paper, we focus on propositional logic programs over a finite (nonempty) set of atoms . A program P is called a normal logic program if every rule ∈ P follows the form: ℎ ← 1 ∧ 2 ∧ ... ∧ ∧ ¬+1 ∧ ... ∧ ¬ (1) ( ≥ ≥ 0) where ℎ and are atoms in .
For short, we write ℎ() and () to denote the set of literals in the head and body of a rule , respectively. Additionally, () can be partitioned into +() = {1, 2, ..., } and − () = {¬+1, ¬+2, ..., ¬} which refers to the and literals in ().
A normal rule is called a fact if () = ∅, a constraint if ℎ() = ∅. A fact or a constraint can also be written respectively as ℎ() ← ⊤ and ⊥ ← (), where ⊤ and ⊥ are special symbols representing True and False. In case − () = ∅, the rule is called a definite rule . A normal program P is a definite program if − () = ∅ for every rule ∈ P.
A normal logic program can be transformed into a definite
program as mentioned in [
Accordingly, Π can be seen as a finite set of rules of the form -rules (3) and -rules (4), and there are no two rules with the same head (SD condition): ℎ ← ℎ ← 1 ∧ 2 ∧ ... ∧ 1 ∨ 2 ∨ ... ∨ ( ≥ 0) ( ≥ 2) (3) (4) For simplicity, we still use the notation ¬ in a standardized program Π but, without ambiguity, imply that ¬ and are two “distinct” variables with a “special” relation. Example 1. Given a logic program P1 = { ← ∧ , ← , ← ¬ ℎ, ← ∧ , ← , ← ¬ , ← ¬ , ← , ← , ← , ← , ← , ← ¬ , ℎ ← ¬, ← ∧ ℎ, ← ∧ }.
Standardized logic program: Π 1 = { ← 1 ∨ ∨ ¬ℎ, ←
∧ , ← ∨ ¬ ∨ ¬, ← , ← , ← ∨ , ←
∨ ¬, ℎ ← ¬ , 1 ← ∧ , ← ∧ ℎ, ← ∧ }.
Here in Example 1, note that we do not need to introduce
new variables for each body atom in ← , ← and
(a) MΠ1∧ (b) MΠ1∨
a b c d e f g h x1 1¬a1¬c1¬d1¬g1¬h a b c d e f g h x1 ¬a ¬c ¬d ¬g ¬h ⊥⊥ 1/a21/b21/c2 d e f g 1/h2 x1 ¬a ¬c ¬d ¬g ¬h
(c) vn⊤eg(Π1)
(d) vΠ⊤
1
(e) MΠ
1
← , ← ¬ , because these rules have single-literal
bodies. In case the rule body has more than one atom, we
need to introduce a new variable for each body atom and
rewrite the rule as a disjunction of these new variables.
Further details about the standardization method can be
found in [
We follow a similar program matrix definition as [
Definition 1 (Matrix of And-rules/Or-rules). Let Π = ⟨Π ∧, Π ∨, Π , Π ⟩ be a standardized program. Then the matrix of And-rules MΠ∧ ( Or-rules MΠ∨ ), where MΠ∧ ∈ RΠ× Π (MΠ∨ ∈ RΠ× Π , Π is the number of atoms in Π ), are defined as follows:
1 ∙ MΠ{_} [, ] = if there is a rule in Π {_} ( either in the form of (3) or (4) respectively if Π {_} is Π ∧ or Π ∨) where = |()| ̸= 0, ∙ MΠ{_} [, ] = 0 otherwise.
We define vector of negations as a column vector v such that v[] = 1 if the corresponding atom at index is a negation. Similarly, vector of facts is defined as a column vector v such that v[] = 1 if the corresponding atom at index is a fact. Figure 1 demonstrates the visualization of matrix/vector representations of Π 1 in Example 1. By definitions, non-zero elements of MΠ∧ , MΠ∨ , and MΠ are normalized by the number of atoms in the body of the corresponding rule. It is possible to define the matrix without normalization as long as being consistent. In the context of logic inferencing, we follow the normalized representation as it is more convenient to define True as 1 and False as 0.
We shall show the connection between this matrix
representation and the one defined in [
{︃1 if ≥ 1 {︃1 if > 0
, and ⇑() = 0 otherwise 0 otherwise where is a scalar and can be extended to a vector, or a matrix in an element-wise way.
The program matrix MΠ can be constructed as follows:
MΠ = MΠ∧ + ⇑(︀ MΠ∨ )︀ + diag(vΠ ⊕ ⇓ vneg(Π)) (5)
where ⊕ ⇓ is vector add with ⇓-thresholding, diag turns
an input vector into a diagonal matrix. The reason for ⊕ ⇓
is that there might be a chance where atoms (known to be
False are included as facts) and negations are overlapping.
Program matrix MΠ in (5) is equivalent to the one defined
in [
In order to illustrate the relationship between program
completion [
Definition 3 (Dependency graph). Given a normal logic program P. The dependency graph of P is a directed graph GP = (VP, EP) where VP is the set of atoms in P and EP is determined as follows: • There is a positive edge (, ) in EP if there is a rule ∈ P such that = ℎ() and ∈ +(). • There is a negative edge (, ) in EP if there is a rule ∈ P such that = ℎ() and ∈ − ().
Note that the direction of an edge (, ) does not matter
unless we are consistent. However, in our paper, we persist
in the direction of edges toward the head atom of a rule. In
many studies, the definition of positive dependency graph is
usually preferred over the general dependency graph [
GP where GP is the dependency graph of P such
tight program if GP+ is acyclic [
Dependency graphs are suficient to illustrate the relationship between literals in a normal logic program. However, it is dificult to capture how to “interpret” a rule in a dependency graph. For example, in Figure 2a, we can see that depends on , , , and ¬ℎ, however, it is not clear to see that all of them are required to deduce or which combination is suficient. A similar argument holds for the case of the positive dependency graph in Figure 2b.
To capture the “actual meaning” of a rule, we introduce the concept of - dependency graph which is defined over a standardized program Π . As mentioned, Π = ⟨Π ∧, Π ∨, Π , Π ⟩. We consider to define the dependency graph of Π only over Π ∧ (-rules) and Π ∨ (-rules). Regardless of a rule in Π ∧ or Π ∨ may difer as a conjunction or disjunction, we can always define the dependency graph of Π ∧ and Π ∨ separately using Definition 3, denoted as GΠ∧ and GΠ∨ respectively. Note that Π ∧ and Π ∨ do not contain any negation by definition, therefore, GΠ∧ and GΠ∨ are also positive dependency graphs. To distinguish edges of GΠ∧ and GΠ∨ from each other, we use solid and dash lines respectively.
Definition 4 (- dependency graph). Given a normal logic program P, its standardized program is Π . The - dependency graph of Π is a directed graph GΠ such that GΠ = GΠ∧ ∪ GΠ∨ .
As can be seen in Figure 2d and Figure 2e, each graph GΠ∧ or GΠ∨ only contains edges of the same type, either solid or dash lines. However, in the - dependency graph GΠ in Figure 2c, both types of edges are presented. It is easy to construct GΠ from GΠ∧ and GΠ∨ by merging the two graphs without any conflict. The following important properties of GΠ can be observed: • A node in GΠ is called an -node if it has only incoming solid edges. Similarly, a node in GΠ is an -node if it has only incoming dash edges. • A node cannot have both types of incoming edges (it is not the case for outgoing edges). In other words, a node can only be either an -node or an node. • From GΠ, we can interpret that an -node is True if all original nodes of its incoming edges are True. Similarly, an -node is True if at least one of the original nodes of its incoming edges is True. By definition, the - dependency graph can capture the semantical meaning of the original Π ∧ and Π ∨. More importantly, a program Π ∧ and its dependency graph GΠ∧ (similar to the case of Π ∨ and GΠ∨ ) are related directly because the program matrix and the adjacency matrix of the dependency graph are equivalent. Note that if all nonzero elements are 1, the program matrix MΠ∧ is exactly the adjacency matrix of the dependency graph GΠ∧ . However, to be consistent with the choice of normalizing rule body to define truth values in the previous section, we denote the adjacency matrix of GΠ∧ by ⇑(MΠ∧ ). Similarly, we denote ⇑(MΠ∨ ) as the adjacency matrix of GΠ∨ .
Sakama et al. first proposed the idea of PE for computing
least models of logic programs using linear algebra [
− −
1
+
+
+
+
−
+
(a) GP1
MΠ - Definition 4 in [
Definition 5 (Partial evaluation of And-rules). Given a normal logic program P, its standardized program is Π . The partial evaluated matrix of Π w.r.t. -rules, denoted as peval(Π ∧), is defined as follows: M̂︁Π∧ = MΠ∧ + diag(vΠ ⊕ ⇓ vneg(Π) ⊕ ⇓ vhead(Π∨)) M0 = M̂︁Π∧ M = M− 1 · M− 1
( ≥ 1) where vhead(Π∨) is a column vector such that vhead(Π∨)[] = 1 if the corresponding atom at index is a head of an rule.
Definition 6 (Partial evaluation of Or-rules). Given a normal logic program P, its standardized program is Π . The partial evaluated matrix of Π w.r.t. -rules, denoted as peval(Π ∨), is defined as follows: M̂︁Π∨ = MΠ∨ + diag(vΠ ⊕ ⇓ vneg(Π) ⊕ ⇓ vhead(Π∧)) M0 = M̂︁Π∨ M = M− 1 · M− 1
( ≥ 1) where vhead(Π∧) is a column vector such that vhead(Π∧)[] = 1 if the corresponding atom at index is a head of an rule.
Both Definition 5 and Definition 6 are almost identical
except for the starting point with diferent matrices MΠ∧
and MΠ∨ respectively. We say (6) and (7) reach a fixed point
at a step ( ≥ 1) if M = M− 1. Because the matrix
multiplication performs unfolding rules [
For the case of acyclic programs, it is guaranteed that the
ifxed point is reached after a finite step of iterations [
Proposition 1. For any program P with MΠ∧ (and MΠ∨ ) of the size × such that the corresponding dependency graph GΠ∧ (and GΠ∧ ) is acyclic, the suficient number of PE steps to reach a fixed point is = ⌈2()⌉.
Proof. Consider the case with a program P2 = {1 ← 2, 2 ← 3, . . . , − 1 ← , }. Obviously, this program has the longest dependency chain we can create from atoms. Indeed, unfolding P2 at the first step we have {1 ← 3, 2 ← 4, 3 ← 5, . . . , − 1 ← }, at the second step we have {1 ← 5, 2 ← 6, 3 ← 7 . . . , − 1 ← }, and so on. According to the pattern, if we perform the PE for steps, then the condition of the fixed point is reached when 2 ≥ ⇔ ≥ 2(). is an integer, so we have = ⌈2()⌉. The proof is identical for the case of Π ∨.
At a fixed point, we can also compute M = (M̂︁Π∧ )2 ( ≥ 1) (or M = (M̂︁Π∨ )2 ( ≥ 1) for the case of -rules) that is basically computing powers of a matrix. Then, we define peval(Π ∧) = unpack((M̂︁Π∧ )2 ) is the partially evaluated program of Π ∧, where unpack((M̂︁Π∧ )2 ) is a series of actions including: (s1) reversing the efect of appending vΠ ⊕ ⇓ vneg(Π) ⊕ ⇓ vhead(Π∨) to the diagonal, (s2) removing all row if the sum of non-zero elements on that row in (M̂︁Π∧ )2 is less than 1, and (s3) normalizing non-zero elements of (M̂︁Π∧ )2 to satisfy Definition 1. Step (s2) is important as an -node is True only if all its body atoms are True. Similarly, we define peval(Π ∨) = unpack((M̂︁Π∨ )2 ) is the partially evaluated program of Π ∨, where unpack((M̂︁Π∨ )2 ) is a series of actions including: (s1) reversing the efect of appending vΠ ⊕ ⇓ vneg(Π) ⊕ ⇓ vhead(Π∧) to the diagonal, and (s2) normalizing non-zero elements of (M̂︁Π∨ )2 to satisfy Definition 1. peval(Π ∧) and peval(Π ∨) are introduced to simplify the notation in the following sections.
We have presented the basic idea of linear algebraic PE of logic programs through iteratively compute powers of matrix (M̂︁Π∧ and M̂︁Π∨ ) until a fixed point is reached. However, a fixed point is not guaranteed in case there is a cycle in the corresponding dependency graph (GΠ∧ or GΠ∨ respectively). For example, consider the visualization of P1 in Figure 2 where GΠ∧ has a cycle {, } while GΠ∨ has 1 1 two cycles {, } and {, , }. In this example, (6) and (7) cannot reach a fixed point, consequently peval(Π 1∧) and peval(Π 1∨) cannot be computed. In the next section, we will introduce cycle-resolving techniques to ensure that this method also works even with cycles in GΠ∧ and GΠ∨ .
First, we define the local cycle in GΠ∧ and GΠ∨ . Definition 7 (Local cycle in GΠ∧ and GΠ∨ ). Given a normal logic program P, its standardized program is Π . A set of atoms is called a local cycle in GΠ∧ (or GΠ∨ ) if is strongly connected in GΠ∧ (or GΠ∨ ).
The term local cycle is used to distinguish from the general
concept of a cycle in GΠ. For example in Figure 2, there
are cycles mixing both solid and dash edges at the same time
such as {, , 1}. These are not (yet) the target of our
cycle-resolving techniques in this paper. Our main focus
is to resolve the local cycles in GΠ∧ and GΠ∨ such as
{, } in GΠ∧ ; and {, }, {, , } in GΠ∨ . We can easily
1 1
identify the local cycles in GΠ∧ and GΠ∨ by identifying
every Strongly Connected Component (SCC) in GΠ∧ and
GΠ∨ respectively. This can be done in polynomial time by
applying the Tarjan’s algorithm [
After identifying the local cycles, let us consider how to resolve them. The main idea is to translate a cycle into a set of rules preserving the same logical meaning but does not create cyclic computation in Definition 5 and Definition 6. This should be done diferently for -rules and -rules. For a cycle in GΠ∧ , obviously, there is no way to make an -node in become True other than the cycle itself. On the other hand, for a cycle in GΠ∨ , we can make an -node in become True if there is any body literal (outside from the cycle ) of that rule which is True. Accordingly, we propose the following cycle-resolving techniques for -rules and -rules respectively. Algorithm 1: Cycle-resolving for -rules 1: Identify all SCCs in GΠ∧ . 2: for each SCC in GΠ∧ do 3: for each rule ∈ Π ∧ such that ℎ() ∈ do 4: Remove (by setting the corresponding entries of in MΠ∧ to 0). 1GraphBLAS is an open-source API specification which defines standard building blocks for graph algorithms in the language of linear algebra. Algorithm 2: Cycle-resolving for -rules 1: Identify all SCCs in GΠ∨ . 2: for each SCC in GΠ∨ do 3: Let = ∅ 4: for each rule ∈ Π ∨ such that ℎ() ∈ do 5: = ∪ (() ∖ ) 6: for each rule ∈ Π ∨ such that ℎ() ∈ do 7: Replace by ℎ() ← ⋁︁ . ∈ After resolving the cycles, we can apply the linear algebraic PE of -rules and -rules as described in Definition 5 and Definition 6 respectively. Now we can prove that the computation has a fixed point.
Proposition 2. Given a resolved matrix resolve(MΠ∧ ) (or resolve(MΠ∨ )) as input for the linear algebraic PE of rules (or -rules), the fixed point is guaranteed to be reached after a finite number of iterations.
For the case of -rules, all cycles in GΠ∧ are removed. Hence, this case is identical to the case of acyclic programs in that the computation in Definition 5 reaches a fixed point after a finite number of iterations.
For the case of -rules, cycles still exist in GΠ∨ but all -rules such that their head nodes are in the cycle are updated in a way that they have incoming edges from all body literals related to a cycle but excluding the cycle itself. This ensures that all possible ways to make an -node in a cycle become True are considered, so no new cases are created during the computation in Definition 6. Thus, a ifxed point is guaranteed. when computing (resolve(M̂︁Π∧ ))2 to obtain peval(Π 1∧). 1 Figure 4a visualizes the dependency graph of peval(Π 1∧). For the case of -rules, there are 2 cycles {, } and {, , }. They all belong to a single SCC. Hence, we only need to resolve {, , } corresponding to three -rules: ← 1 ∨ ∨ ¬ℎ, ← ∨ , ← ∨ ¬. Following Algorithm 2, we find = {¬, ¬ℎ, 1}. Next, we reset all -rules corresponding to , , and with the new body {¬, ¬ℎ, 1}. The resulting matrix resolve(MΠ∨ ) is illus1 trated in Figure 3e. Unlike the case of -rules where we remove the cycle, here we find all possibilities to make the cycle become True then update the rules accordingly. After all cycles are resolved, we can apply the iteration method described in Definition 6 to compute peval(Π 1∨). Figure 4b visualizes the dependency graph of peval(Π 1∨). Combining peval(MΠ∧ ) and peval(MΠ∨ ) To sum up, we have presented the basic idea of linear algebraic PE. We have also introduced cycle-resolving techniques to ensure that this method also works efectively even with cycles in GΠ∧ and GΠ∨ . Finally, we can construct the partially (a) resolve(MΠ∧ ) 1 (b) resolve(M̂︁Π1∧ ).
(c) (resolve(M̂︁Π1∧ ))2
(d) peval(MΠ∧ )
1
a b c d e f g h x1 ¬a ¬c ¬d ¬g ¬h
a 1
b 1/2 1/2
c 1
d
e
f 1
g 1
h 1
x1 1/2 1/2
¬a 1
¬c 1
¬d 1
¬g 1
¬h
evaluated program matrix for logic inferencing in vector
spaces by combining peval(MΠ∧ ) and peval(MΠ∨ ):
peval(MΠ) =
peval(Π ∧) + ⇑(︀ peval(Π ∨))︀
+diag(vΠ ⊕ ⇓ vneg(Π))
(8)
peval(MΠ) can be used for the fixpoint computation in
the same way as MΠ. A few modifications may be needed
to apply the idea to Horn abduction in [
As we have seen in the previous sections, the main idea of
PE is to compute the powers of a program matrix. While
in linear algebra, it is known that powers of a matrix M
can be computed eficiently using its eigendecomposition
M = Q · A · Q− 1, where A is a diagonal matrix of
eigenvalues and Q is a matrix of eigenvectors [
In this section, we will show how to apply eigendecomposition to realize PE in LP. Let us consider an example: Example 2. Given a logic program P3 = { ← ∧ , ← ∧ , ← }. Standardized logic program (no change): Π 3 = P3.
There is no -rule in Π 3, so we only need to consider ⎛ 1/2 1/2 ⎞ MΠ3∧ = ⎝ 1/2 1/2 ⎠. For computing the eigen 1 values, it is more numerically stable to use the adjacency ma ⎛ 1 1 ⎞ trix ⇑(MΠ3∧ ) = ⎝ 1 1 ⎠ instead of MΠ3∧ . Next, 1 we append needed information to the diagonal to obtain ⇑(M̂︁Π3∧ ), here they are identical. Let us compute the eigenvalues of ⇑(M̂︁Π3∧ ).
⇔ ⇔ ⇔
( ⇑(M̂︁Π3∧ ) − I)
⎛ 1 − ⎜⎝ 1 1 −
1 − 3 + 2 2 − 1 ( − 1)( 2 − − 1)
⎞ 1 ⎟⎠ 2 = 3 = can compute powers of ⇑(M̂︁Π∧ ) eficiently. However, 3 unlike the iteration method in which we let the method determine a fixpoint condition, here we need to determine the power in advance. Fortunately, we can set a suficiently large to ensure that the fixpoint is reached following Proposition 1. In this example, as = 3, we have a suficient number of iterations to reach the fixpoint = ⌈2(3) − 1⌉ = 1, then we just need to raise A to the power of + 1 = 2. Accordingly, the partial evaluated matrix is: ⎛ 1 2 1 ⎞ Q · A2 · Q− 1 = ⎝ 0 2 1 ⎠ 0 1 1 This matrix can be translated into a logic program: peval(MΠ3∧ ) = { ← ∧ ∧ , ← ∧ , ← ∧ } ¬ ¬ ℎ ¬ℎ ¬ ¬ ℎ (d) MΠ1 a b c d e f g h x1 ¬a ¬c ¬d ¬g ¬h
1 1 1 1/21/2 1
1 which is the partial evaluated program of Π 3∧. Because there is no -rule in this case, so peval(MΠ∧ ) is also the par3 tially evaluated program of Π 3.
Using eigendecomposition for partial evaluation is
computationally more eficient than the iteration method,
especially when the number of iterations is large. However, the
eigendecomposition method requires the matrix to be
diagonalizable [
In linear algebra, the JNF, also known as the Jordan canonical form, is a specific type of upper triangular matrix called a Jordan matrix.
Definition 8 (Jordan normal form [
⎞ ⎟ = ⎜⎜⎜ ⎟ ⎠⎟ ⎝ ⎛(1) (2)
. . .
() that can be simplified by computing powers of each Jordan block. The power of a Jordan block of the size × can be computed by: () = ⎜⎜⎜⎝⎜⎜⎜⎜⎜⎜ ︀(︀( 1 )︀)︀ . . .−− 21 ...... ... ... ...... (︀ ︀(−−112)︀)︀ ...... −− 1+2⎟⎟⎟⎠⎟⎟⎟⎟⎟⎟ ⎛ ︀( 1 )︀ − 1 2 . . . . . . (︀ )︀ − +1⎞ where (︀ )︀ is the binomial coeficient describing the alge braic expansion of powers of a binomial.
Now let us consider an example to illustrate the idea of using JNF for partial evaluation.
Example 3. Given a normal logic program: P4 = { ← , ← , ← , ← , ← ¬ , ← ¬ , ← ¬, ← ¬ , ← ¬ , ← ¬ }.
Standardized logic program: Π 4 = { ← ∨ , ← ∨ , ← ¬ ∨ ¬, ← ¬ ∨ ¬, ← ¬ ∨ ¬}.
There is no -rules, so we only need to consider M̂︁Π4∨ . The matrix is not diagonalizable as (M̂︁Π4∨ ) = 0, so we will use the JNF to compute powers of M̂︁Π4∨ . First, let us compute the eigenvalues of ⇑(M̂︁Π4∨ ): ¬ ¬ ¬ 1 1 Following the algorithm described in [30], one can find the JNF of ⇑(M̂︁Π4∨ ) = P · J · P− 1 where: 2The algebraic multiplicity of an eigenvalue is the number of times it appears as a root of the characteristic polynomial. ¬ ¬ ¬ ¬ ¬ ¬ 1 0 1 1 0 1 0
0 General approach using matrix decomposition To summarize this section, we have shown how to use eigendecomposition and JNF to compute the powers of a matrix in the context of PE of logic programs. A baseline step-by-step is as follows:
We focus on evaluating the performance of the proposed
linear algebraic PE with iteration method (I) and the
matrix decomposition method (II) using the logic programs
in Failure Modes and Efects Analysis ( FMEA) benchmarks
[31] that also has been reported in [
Table 1 reports the statistical data of the datasets and a detailed comparison of the execution time of the proposed algorithms. It can be seen that (I) is the fastest on all datasets while (II) is significantly slower. Table 2 reports the comparison for the cyclic case. In this case, we also report the execution time for the cycle-resolving step (resolve for short). peval + resolve is the total run time for this case. Augmented cycles do not change much the structure of the dataset, so the comparison is similar to the acyclic case.
The reason for (II) being slow in our benchmark is that all program matrices in the benchmarks are not diagonalizable, and Algorithm 3 must call sympy for JNF decomposition. As sympy is meant for symbolic computation, it can only handle matrices of up to 100 atoms in a reasonable time. For program matrices of this size, according to Proposition 1, (I) can reach a fixed point in a few iterations, and then it dominates (II). JNF is also known to be numerically unstable that is a small perturbation in the input matrix can lead to a large change in the Jordan form [32]. This leads to the low adoption of JNF in API libraries for numerical computation that we cannot find an available one in sparse format.
In general, (I) is the best choice for linear algebraic PE in practice because it is simple, fast, and stable.
To wrap things up, we have proposed several techniques to extend the linear algebraic PE to accommodate -rules and cycles in logic programs. First, the matrix representation of a standardized program Π is separated into MΠ∧ and MΠ∨ , then PE for -rules and -rules can be handled similarly. Next, we introduced cycle-resolving techniques to ensure that linear algebraic PE works efectively even with local cycles in the Π ∧ or Π ∨. Moreover, by seeing the PE as computing the power of the matrix representation of the program, we can further leverage eigenvalues and eigenvectors or program matrices to perform PE in vector spaces. To the best of our knowledge, this is the first attempt to incorporate matrix decomposition techniques into linear algebraic PE for LP. Although the decomposition method does not perform really well in practice, it opens up a new direction for future research where we focus on leveraging eigenvalues and eigenvectors of program matrices for reasoning with LP. It is also important to connect LP to spectral graph theory [33] in which researchers have also studied the connection between the eigenvalues of the adjacency matrix of a graph and its properties. Future work also includes investigating to extend linear algebraic PE to globally handle both -rules and -rules in a logic program even with global cycles.
This work has been supported by JSPS KAKENHI Grant Number JP21H04905 and JST CREST Grant Number JPMJCR22D3. [30] S. H. Weintraub, Jordan canonical form: theory and practice, Springer Nature, 2009. [31] R. Koitz-Hristov, F. Wotawa, Faster horn diagnosis-a performance comparison of abductive reasoning algorithms, Applied Intelligence 50 (2020) 1558–1572. [32] C. Moler, C. Van Loan, Nineteen dubious ways to compute the exponential of a matrix, twenty-five years later, SIAM review 45 (2003) 3–49. [33] R. A. Brualdi, Spectra of digraphs, Linear Algebra and its Applications 432 (2010) 2181–2213.