PyReason: Software for Open World Temporal Logic

Abstract

The growing popularity of neuro symbolic reasoning has led to the adoption of various forms of diferentiable (i.e., fuzzy) first order logic. We introduce PyReason, a software framework based on generalized annotated logic that both captures the current cohort of diferentiable logics and temporal extensions to support inference over finite periods of time with capabilities for open world reasoning. Further, PyReason is implemented to directly support reasoning over graphical structures (e.g., knowledge graphs, social networks, biological networks, etc.), produces fully explainable traces of inference, and includes various practical features such as type checking and a memory-eficient implementation. This paper reviews various extensions of generalized annotated logic integrated into our implementation, our modern, eficient Python-based implementation that conducts exact yet scalable deductive inference, and a suite of experiments. PyReason is available at: github.com/lab-v2/pyreason.

Keywords

• eol>Logic programming
• Neuro Symbolic Reasoning
• Generalized annotated logic
• Temporal logic
• First order logic
• Open world reasoning
• Graphical reasoning
• AI Tools

1. Introduction

Various neuro symbolic frameworks utilize an underlying logic to support capabilities such as fuzzy logic [ 1 ], parameterization [ 2 ], and diferentiable structures [ 3 ]. Typically, implementations of such frameworks create custom software for deduction for the particular logic used, which limits modularity and extensibility. Further, emerging neuro symbolic use cases including temporal logic over finite time periods [ 4 ] and knowledge graph reasoning [ 5 ] necessitate the need for a logical frmaework that encompasses a broad set of capabilities. Fortunately, generalized annotated logic [ 6 ] with various extensions [ 7, 8, 9 ] capture many of these capabilities. In this paper we present a new software package called PyReason for performing deduction using generalized annotated logic that captures many of the desired capabilities seen in various neuro symbolic frameworks including fuzzy, open world, temporal, and graph-based reasoning. Specifically, PyReason includes a core capability to reason about first order (FOL) and propositional logic statements that can be annotated with either elements of a lattice structure or functions over that lattice. Further, we have provided for additional practical syntactic and semantic extensions that allow for reasoning over knowledge graphs, temporal logic, reasoning about various network difusion models, and predicate-constant type checking constraints. This implementation provides for a fast, memory optimized, implementation of the ifxpoint operator used in the deductive process. By implementing the fixpoint operator directly (as opposed to a black box heuristic) the software enables full explainability of the result. As such is the case, this framework captures not only classical logic, but a wide variety of other logic frameworks including fuzzy logic [ 10, 11, 12 ], weighted real valued logic used in logical neural networks [ 2 ], van Emden’s logic [ 13 ], Fitting’s bilattice logic [ 14 ], various logic frameworks for reasoning over graphs or social networks [ 9, 8, 15 ] (as well as the various network difusion models captured by those frameworks), and perhaps most importantly, logic frameworks where syntactic structure can be learned using diferentiable inductive logic programming [ 3, 16 ] as well as other neuro symbolic frameworks [ 17, 7 ]. The key advantages of our approach include the following: 1. Direct support for reasoning over knowledge graphs. Knowledge graph structures are one of the most commonly-used representations of symbolic data. While black box frameworks such as [ 18 ] also permit for reasoning over graphical structures, they do not aford the explainability of our approach. 2. Support for annotations. Classical logic implementations such as Prolog [19] and Epilog [20] inherently do not support annotations or annotation functions, hence lack direct support for capabilities such as fuzzy operators. Further, our framework goes beyond support for fuzzy operators by enabling arbitrary functions that can be used over real values or intervals of reals. This is a key advantage to reasoning about constructs learned with neuro symbolic approaches such as [ 2, 3, 16, 17, 7 ]. 3. Temporal Extensions. While the framework of [ 6 ] was shown to capture various temporal logics, extensions such as [ 9 ] have provided for syntactic and semantic addons that explicitly represent time and allow for temporal reasoning over finite temporal sequences. Following [ 9 ], we use a semantic structure that represents multiple time points, but we have implemented this in a compact manner to preserve memory. Our solution allows for fuzzy versions of rules such as “if () then () in time steps.” Note that these capabilities are not present in nearly every current implementation of fuzzy logic. 4. Use of interpretations. We define interpretations as annotated function over predicates and time together. It allows us to capture facts which are true before = 0. While annotated logic [ 6 ] can subsume various temporal logics without additional constructs, we have enabled temporal reasoning through incorporating a temporal component in interpretations. By combining annotated predicates and the time variable, we believe our framework is more flexible and suitable for emerging neuro symbolic applications involving time - as such applications will inherently require both time and real-valued annotations. Additionally, it is to be noted that we do not make a closed world assumption i.e. anything that is not mentioned in the initial set of interpretations is . Instead, we consider all other interpretations to be unknown at the beginning of time. 5. Graphical Knowledge Structures. We also implement [ 8 ] which provides graphical syntactic extensions to [ 6 ]. This is included in our implementation, notably adding extended syntactic operators for reasoning in such structures (e.g., an existential operator requiring the existence of items). An example of such a rule would be a fuzzy version of “if () and there exist number of ’s such that (, ) then ()”.1 6. Reduction to computational complexity due to grounding. Our software leverages both the inherent sparsity of the graphical structure along with a novel implementation of predicate-constant type checking constraints that significantly improves utility in a variety of application domains but also provide drastic reduction to complexity induced by the grounding problem. We are not aware of any other framework for first-order logic that provides both such capabilities. 7. Ability to detect and resolve inconsistencies in reasoning. As logical inferences are deduced through applications of the fixpoint operator over predefined logical rules, logical inconsistencies can not only be detected but also located exactly where in the inference process the inconsistency occurred. We resolve any such inconsistencies by leveraging uncertainty. In the software implementation, as soon as an inconsistency is detected we relax and fix the bounds to complete uncertainty. The ability to check and locate inconsistencies enhance the explainability feature. Neuro symbolic approaches like [ 2, 7 ] may also look to leverage inconsistency as part of loss during the training phase.

In section 2, we outline the syntax and semantics of [ 6 ] as well as our extensions. Our software implementation is described in section 3 and is expanded upon in the online only supplement. In section 4, we provide experimental results of our framework to demonstrate reasoning capabilities in two diferent real-world domains. We have conducted experiments on a supplychain [21] (10 constants), and a social media [22] (1.6 constants) dataset. For evaluation, we used various manually-curated logic programs specifying rules for the temporal evolution of the graph, completion of the graph, and other such practical use-cases (e.g., identifying potential supply chain disruptions) and examined how various aspects afect runtime and memory usage (e.g., number of constants, predicates, timesteps, inference steps, etc.). The results show that both runtime and memory remain almost constant over large ranges, and then scale sub-linearly with increase in network size.

Online Resources

Open source python library is available at: pypi.org/project/pyreason. PyReason codebase can be found at: github.com/lab-v2/pyreason.

Online only supplement is available at: github.com/lab-v2/pyreason/tree/main/lit

2. Logical Framework

In this section, we provide an overview of the annotated logic framework with a high-level description of the logical constructs, knowledge graph structure, key optimizations, and 1Note that while this example is classical, PyReason supports fully annotated logic, allowing for arbitarily defined fuzzy operators (e.g., t-norms); See section 2 and online supplement for technical details. operation of the fixpoint algorithm.

Knowledge graph. We assume the existence of a graphical structure = (, ) where the nodes are also constants (denoted set ) in a first-order logic framework. The edges, denoted ⊆ × , specify whether any type of relationship can exist between two constants. Similar to recent frameworks combining knowledge graphs and logic [ 3, 18 ], we shall assume that all predicates in the language are either unary (which can be thought of as labeling nodes) or binary (which can be thought of as labeling edges). We note that we assume the existence of a special binary predicate rel , which we shall treat as a reserved word. For (, ) ∈ we shall treat rel (, ) as a tautology and for (, ) ∈/ we shall treat rel (, ) as uncertain. Note that we can support no restrictions among the pairing of constants by creating as a fully connected graph. Likewise, we easily support the propositional case by using a graph of a single node (essentially treating unary predicates as ground atoms). We provide a running example in this section. In Figure 1, we illustrate how a knowledge graph is specified in our framework. Example 2.1 (Knowledge Graph). Consider the following nodes: three students- Phil, John, Mary and two classes- English and Math. Nodes and edges have unary and binary predicates as shown in Fig. 1. Hence we get the following non-ground atoms: student(S), gpa(S), promoted(S) class(C), difficulty(C) friend(S,S’) takes(S,C), grade(S,C), expertise(S,C) Here, S, S’, and C are variables which when grounded with constants from the graph, produce ground atoms such as: student(john), student(phil), student(mary) class(math), class(english) takes(john,math), takes(mary, english) ...

In the propositional case, a non-ground atom reduces to a propositional statement. For e.g. The predicate “takes(john,math)” can be represented as a propositional statement: “John takes Math class” and can be either True or False. It is true in this example, as shown in Fig. 1. Real-valued Interval Annotations. A key advantage of annotated logic [ 6 ] is the ability to annotate the atoms in the framework with elements of a lattice structure as well as functions over that lattice. In our software, we use a lower lattice structure consisting of intervals that are a subset of [ 0, 1 ]. This directly aligns with the truth interval for fuzzy operators [ 12 ], as well as paradigms in neuro symbolic reasoning [ 2, 7 ], and social network analysis [ 8, 9 ]. We can fully support scalar-valued annotations by simply limiting manipulations to the lower bound of the interval and keeping the upper bound set at 1. These annotations can support classical logic by limiting annotations to be [0, 0] (false) and [ 1, 1 ] (true). It can also support tri-valued logic by permitting [ 0, 1 ], which represents no knowledge. Of course, there is no need to conduct restrictions, especially if it is desirable to support logics that make full use of the interval [ 2, 8, 9 ]. Additionally, we support literals as detailed in [ 7 ]. We treat negations the same way as in [ 1 ] - for an atom annotated with [ℓ, ], we annotate its strong negation(¬) with [1− , 1− ℓ]. Example 2.2 (Real-valued Interval Annotations). Continuing with the previous example, we can support a variety of annotations as described above.

Propositional logic: student(john): [ 1,1 ] (example of a True statement) takes(mary,math): [0,0] (example of a False statement) Fuzzy logic (using scalar values):

gpa(john): [X,1], X ∈ [ 0,1 ] Full interval usage:

difficulty(english): [0.3,0.7] (both bounds are used here to capture the variation among students regarding the perceived dificulty of the subject “english”).

Modeling uncertainty and/or tri-valued logic: Let’s assume that we do not have complete knowledge of this network - specifically, we do not have any information about the friendship between John and Phil. So, they might be friends (annotated [ 1,1 ]) or not friends (annotated [0,0]). Our framework can model such a case as: friend(john,phil): [ 0,1 ] Interpretations. Commonly in logic frameworks, an initial set of facts is used. We use the term “initial interpretations” to capture annotations correct at the beginning of a program. In the envisioned domains - to include the ones in which we perform experiments - these initial interpretations shall be represented as a knowledge graph that not only includes graph but also attributes on the nodes and edges (resembling predicates) and real-valued interval annotations (specifying the initial annotations for each element). Additionally, following intuitions from various temporal logic frameworks that incorporate both temporal and other realvalued annotations [ 9, 8, 23, 24, 25 ], we extend our syntax to provide for temporal annotations as part of the interpretations. Following the related work, time is represented as finite discrete timepoints. The initial interpretations comprises what is to be treated as true before time 0. Further, with the initial interpretations we can specify predicates as being either static (in other words, ground atoms formed with those predicates retain the same annotation across all time periods) or non-static (which are permitted to change). The ability to add this restriction has clear benefit in certain domains, and also allows for key implementation eficiencies for reasoning across time periods. Further, it is noted various inductive logic programming paradigms [ 3, 26 ] utilize “extensional” predicates that are also unchanging - which could be treated as “static” in PyReason.

Syntax:

(, ^) : [, ] where, can be an atom (propositional case) or predicate (first order logic), ^ is either the time point = for which the interpretation is valid, or if the interpretation is static, i.e. remains unchanged for all time-points then ^ = . So, ^ = {︃, if (, ^) is static , ∈ if (, ^) is time-variant (1) Annotation [, ] → [ 0, 1 ] (or, in propositional case [, ] ∈ [0, 0], [ 1, 1 ]). We incorporate literals in our system by having separate interpretations for an atom and its negation. We note that, excepting the case of static atoms, ground atoms at diferent time points need not be dependent upon each other. For example, atom “a” at time 1 can be annotated with [0.5, 0.7] and annotated with [0.1, 0.2] at time 2. There is no monotonicity requirement between time points.

Example 2.3 (Interpretations). Continuing the previous example, Initial set of facts regarding student enrollment:

I(student(john),0) = [ 1,1 ] (John is enrolled as a student) I(student(mary),0) = [ 1,1 ] (Mary is enrolled as a student)

I(student(phil),0) = [0,0] (Phil is not enrolled as a student) Static interpretations can be used for always true facts like:

I(class(english), s) = [ 1,1 ] (English is a class ofered at all time-points) Using temporal annotation to capture variation over time:

I(takes(john,math),1) = [ 1,1 ] (John takes Math class at time = 1) I(takes(john,math),5) = [0,0] (But is no longer taking Math at = 5) All other interpretations, if unspecified at = 0, are initialized with [ 0, 1 ].

Logical Rules. Rules are the key syntactic construct that enables changes to atoms formed with non-static predicates. Historically logical rules had mostly been written by domain experts, until early work like Apriori [27] and FOIL [28] to learn association rules from data followed by the emergence of rule mining techniques like causal rule mining [29] and annotated probabilistic temporal logic [24, 30, 31]. More recently, there has been research on Diferentiable Inductive Logic Programming (ILP) - an inductive rule learning method to learn logical rules from examples [ 3, 16, 32 ]. In the below list and are arbitrarily sets of unary and binary predicates relevant to the rules while is always a non-static predicate. Note that the total number of atoms in the body is assumed to be (across all diferent conjunctions). The symbol ∃ means there exists at least number of constants such that the ensuing logical sentence is satisfied.

1. Ground rule for reasoning within a single constant or edge: () : (1, . . . , ) ← Δ ⋀︀∈ () : (, ′) : (1, . . . , ) ← Δ ⋀︀∈ (, ′) : 2. Universally quantified non-ground rule for reasoning within a single constant or edge: ∀ : () : (1, . . . , ) ← Δ ⋀︀∈ () : ∀, ′ .. (, ′) ∈ : (, ′) : (1, . . . , ) ← Δ ⋀︀∈ (, ′) : ∧ ⋀︀∈ () : ∧ ⋀︀∈′ (′) :

3. Universally quantified non-ground rule for reasoning across an edge:

∀ : () : (1, . . . , ) ← Δ ∃′ : (, ′) : [ 1, 1 ] ∧ ⋀︀∈ (, ′) : ∧ ⋀︀∈ () : ∧ ⋀︀∈′ (′) :

4. Non-ground rule with rule based quantifier in the head:

() : [(1, 2, . . . , ), (1, 2, . . . , )] ← ⋀︀ s.t. (,)∈ ′(, ) : [, ] Here, ,() could be the ℎ rule based quantifier defined over set such that, ,() = ℎ highest value in set .

Example 2.4 (Logical Rules). For the continuing example we can formulate some interesting rules based on the formats given above as: 1. () : [ (1, 2), (1, 2)] ← Δ=1 () : [1, 1] ∧ () : [2, 2] which says, “If is a student with bounds [1, 1] and has a gpa with bounds [2, 2], then is likely to be promoted, at the next timestep, with bounds given by a function of [1, 1] and [2, 2].”

Here, could be a T-norm. Some well known examples of T-norms are:

a) Minimum: (, ) = (, ) = (, ) b) Product: (, ) = (, ) = · c) Łukasiewicz: (, ) = (, ) = (0, + − 1) PyReason also supports other well known logical functions like − , algebraic functions like , , , among others. 2. ∀, (, ) : [0.6 * , 1] ← Δ=0 [, ] : [, 1] ∧ () : [ 1, 1 ] ∧ ( ) : [ 1, 1 ] which says, “If is a student who obtains a grade [, 1] in class , then we can estimate ’s expertise of subject by defining an annotation function [0.6 * , 1] over a single annotation [, 1].” 3. (ℎ) : [ 1+2 2 , 1] ← Δ=0 ∃=2 ∈ : () : [ 1, 1 ] ∧ (ℎ, ) : [ 1, 1 ] ∧ (ℎ, ) : [, 1] which says, “If ℎ takes and earns grades for two classes, then his can be calculated using the algebraic function in the head of the given existentially quantified ground rule.” 4. (, ′) : [ 1, 1 ] ← Δ=2 (, ) : [ 1, 1 ] ∧ (′, ) : [ 1, 1 ] ∧ () : [ 1, 1 ] a propositional rule with temporal extension which states, “If two students and ′ take the same class , they develop a friendship after two timesteps.” 5. ∀, ′, ′′ (, ′′) : [ 1, 1 ] ← Δ=1 (, ′) : [ 1, 1 ] ∧ (′, ′′) : [ 1, 1 ] an universally quantified non-ground rule analogous to the associative rule in mathematics which encapsulates, “Having a common friend ′ leads to friendship between two people and ′′.” Fixpoint Operator for Deduction. Central to the deductive process is a fixpoint operator (denoted by Γ) which has previously been proven to produce all atoms entailed by a logic program (rules and facts) in [ 6, 7 ] and these results were extended for the temporal semantics in [ 9, 8 ]. It is noteworthy that this is an exact computation of the fixpoint, and hence providing the minimal model associated with the logic program allowing one to easily check for entailment of arbitrary formulae. Further, the result is fully explainable as well: for any entailment query we would have the series of inference steps that lead to the result. This difers significantly from other frameworks that do not provide an explanation for deductive results [ 18 ] though a key diference is that the reasoning framework implemented in PyReason allows for exact and eficient polynomial time inference, while others have an intractable inference process. Example 2.5 (Fixpoint Operator(Γ)). Consider we have the following set of initial interpretations in addition to the ones specified before: I(takes(john,english),1) = I(takes(john,english),2) = [ 1,1 ] I(takes(mary,english),2) = I(takes(mary,english),3) = [ 1,1 ] (John takes English at t=1,2 and Mary takes English at t=2,3) I(friend(mary,phil),s) = [ 1,1 ] (Mary and Phil are friends for the entire time considered) And we consider the rule set to be made of rule 4 and 5 from above. We initialize: ∀S,S’ I(friend(S,S’),0) = [ 0,1 ] (all relationships initialized as unknown) and then update: I(friend(mary,phil),s) = [ 1,1 ] (from initial interpretations) Application of Γ at T=0 and 1 yields no change in as none of the rules are fired. At T=2, rule 4 fires with the following groundings: (ℎ, ) : [ 1, 1 ] ← Δ=2 (ℎ, ℎ) : [ 1, 1 ] ∧ (, ℎ) : [ 1, 1 ] ∧ (ℎ) : [ 1, 1 ] (, ℎ) : [ 1, 1 ] ← Δ=2 (, ℎ) : [ 1, 1 ] ∧ (ℎ, ℎ) : [ 1, 1 ] ∧ (ℎ) : [ 1, 1 ] This would result in a change in at T = 4, as Δ = 2 for the rule above and it is fired at T=2. I(friend(john,mary),4) = [ 1,1 ] I(friend(mary,john),4) = [ 1,1 ] At T=3, as is still unchanged, application of Γ does not lead to any of the rules firing. At T=4, application of Γ with the updated interpretation leads to firing of grounded rule 5 as: (ℎ, ℎ) : [ 1, 1 ] ← Δ=1 (ℎ, ) : [ 1, 1 ] ∧ (, ℎ) : [ 1, 1 ] And results in: I(friend(john, phil),5) = [ 1,1 ] The above illustrates how PyReason makes logical inferences by exact application of the fixpoint operator(Γ). In this example, we are able to trace how the interpretation I(friend(john, phil),t) changed over time, and which rules caused these changes. This shows that this process is completely explainable, and can be leveraged in emerging neuro symbolic applications. Constant-Predicate Type Checking Constraints. Key to reducing the complexity and speeding up of the inference process is type-checking. We leverage the sparsity commonly prevalent in knowledge graphs to significantly cut down on the search space during the grounding process. We noticed that typically a graph will have nodes of diferent types, and predicates typically were defined only over constants of a specific type. While initializing the interpretations, type checking takes this into account and only creates ground atoms for the subset of predicateconstant pairs which are compatible with each other. However, we note that this is an option, as in some applications such information may not be available.

Example 2.6 (Constant-Predicate Type Checking). In the continuing example we see that the predicates student, gpa, promoted are only limited to constants of type student. Similarly, predicates class, difficulty are exclusive to the constants english and math. Type checking ensures that we do not consider ground atoms like student(english) or class(phil).

Likewise for binary predicate takes(S,C), the first variable is always grounded with a student type constant, and the second with a class type constant. Even in this miniature example, type checking reduces the number of ground atoms under consideration from 25 to only 6 - a 76% reduction. Such gains significantly reduce complexity as size and sparsity of the graph increases.

Detecting and Resolving Inconsistencies. Inconsistency can occur in the following cases: 1. For some ground atom, a new interpretation is assigned an annotation [′, ′] that is not a subset of the current interpretation [, ] (we assume ≤ ). i.e. if either < ′ or ′ < . 2. When an inconsistency occurs between an atom and its negation like “a” and “not a”.

Or between complementary predicates like “ℎ()” and “()” which cannot hold simultaneously. e.g. Literal A has annotation [1, 1] and Literal B is the negation of literal A with annotation [2, 2]. The fixpoint operator attempts to assign [′1, 1′ ] to Literal A, and [′2, 2′ ] to Literal B. But new bounds are inconsistent, i.e. either ′1 > 1 − ′2 or 1′ < 1 − 2′ .

PyReason flags all such inconsistencies arising during the execution of the fixpoint operator and reports them. Further, as the fixpoint operator provides an explainable trace, the user can see the precise cause of the inconsistency. As an additional, practical feature, PyReason includes an option to reset the annotation to [ 0, 1 ] for any identified inconsistency and set the atom to static for the remainder of the inference process. In this way, such inconsistencies cannot propagate further. These initial capabilities provide a solid foundation for more sophisticated consistency management techniques such as providing for local consistency or iterative relaxation of the initial logic program.

Example 2.7 (Detecting and Resolving Inconsistencies.). Consider we have the following prior knowledge:

I(takes(phil,math), 4) = [ 1,1 ] I(takes(mary,math), 4) = [ 1,1 ]

I(friend(phil,mary), 5) = [0,0] However, the following logical rule with grounding ← ℎ, ′ ← , ← ℎ: (, ′) : [ 1, 1 ] ← 1 (, ) : [ 1, 1 ] ∧ (′, ) : [ 1, 1 ] gets fired at = 4. resulting in:

I(friend(phil,mary), 5) = [ 1,1 ] But clearly this is an inconsistency as I(friend(phil,mary), 5) cannot be both [0, 0] and [ 1, 1 ] simultaneously. So, we conclude that at least one of those two interpretations must be incorrect. If there is no way to ascertain which is correct, we may resolve this logical inconsistency by setting:

I(friend(phil,mary), s) = [ 0,1 ] at = 5.

3. Implementation

We have endeavored to create a modern Python-based framework to support scalable yet correct reasoning. We allow graphical input via convenient Graphml format, which is commonly used in knowledge graph architectures. The python library Networkx is used to load and interact with the graph data. We are currently in the process of directly supporting Neo4j. The initial conditions and rules are entered in YAML format and we use memory-eficient implementation techniques to correctly capture semantic structures. We use the Numba open-source JIT compiler to translate many key operations into fast, optimized machine code while allowing the user to interact with Python and the aforementioned front-ends. Our implementation can support CPU parallelism, as evidenced by our experiments run on multi-CPU machines.

Our software stores interpretations in a nested dictionary. For computational eficiency and ease of use, our software allows specification of a range of time-points = 1, 2, . . . instead of a single time-point , for which an interpretation remains valid. To reduce memory requirements, only the one set of interpretations (current) are stored at any point in time. However, past interpretations can be obtained using rule traces, which retains the change history for each interpretation and the corresponding grounded logical rules that caused each change. Rule traces make our software completely explainable, as every inference can be traced back to the cascade of rules that led to it.

MANCaLog [ 9 ] showed the use of the fixpoint operator for both canonical and non-canonical models. By recomputing interpretations at every time step, we not only require significantly less memory but also, support both the canonical and the non-canonical cases. Due to this design, increase in computation time is observed to be minimal.

Furthermore, we make significant advances on [ 33] by supporting static predicates, and having in-built capabilities for non-graph reasoning, and type checking as detailed in section 2.

Our implementation can be found online as specified in section 1 and detailed pseudo-code can be found in the supplemental information.

4. Experiments

4.1. Honda Buyer-Supplier Dataset We conduct our experiment on a Honda Buyer-Supplier network [21]. The dataset (network) contains 10,893 companies (nodes) and 47,247 buyer-supplier relationships between them (edges).

We design an use case, where we assume that operations of all companies from a particular country are disrupted, and observe the efects that this may have on companies across the world. We feel this is akin to supply chain issues faced worldwide during the COVID-19 pandemic. For our tests, we use the following logical rule which in practice would be either learned or come from an expert. () : [ 1, 1 ] ← Δ=1 ∀(, ) : [ 1, 1 ], ∃/2() : [ 1, 1 ] It states that, a company is disrupted at a particular timestep if at least 50% of its suppliers are totally disrupted in the previous timestep. We conduct this experiment for three diferent countries (USA, Taiwan, and Australia), having a wide range of proportion of companies in the dataset. We do not fix the number of inference steps, instead we let the difusion process run until it converges (in bold). The results are shown in Table 1.

To test if our approach could scale, we use two inference rules which jointly state, a company is disrupted at a particular timestep if any of its supplier(s) are completely disrupted in the previous timestep, or if at least 50% of its suppliers are disrupted to at least 50% of their capacity. We conduct this experiment for diferent graph sizes, and for diferent number of timesteps to show the scaling capability of our software in Table 2.

The results show that both runtime and memory remain almost constant over large ranges, and then scale sub-linearly with increase in network size. 4.2. Pokec Social Media dataset Pokec is a popular slovakian social network, and this dataset [22] contains personal information like gender, age, pets (attributes) of 1.6 million people (nodes), and 30.6 million connections between them (edges).

We take inspiration from the advertising community to design our use case. We consider, a small proportion of the population, who has pet(s), to be customers of a pet food company. The company, using Pokec data, must identify relevant advertising targets among the population. A realistic strategy can be captured by two logical rules: 1. ∀, () : [0.6, 1] ← Δ=1 ( ) : [ 1, 1 ] ∧ (, ) : [ 1, 1 ]

Friend of a relevant target or existing customer (always relevant), is at least 60% relevant. 2. ∀, () : [ 1, 1 ] ← Δ=1 ( ) : [ 1, 1 ] ∧ (, ) : [ 1, 1 ] ∧ ℎ (, ) : [ 1, 1 ] ∧ ℎ (, ) : [ 1, 1 ]

Friend of a relevant target is totally relevant if they have pet(s) of same kind - dog, cat, . . .

The difusion process converged after 8 timesteps, took 42 minutes to complete and used 58.36 GB of memory - which further showcases the scalability of our framework. The results are shown in Table 3.

The process of inference is completely explainable, and an user may use rule traces, an optional output of PyReason, to identify the logical rules that led to change in each interpretation. An example of a rule trace from the previous experiment is presented in Table 4.

All experiments were performed on an AWS EC2 container with 96 vCPUs (48 cores) and 384GB memory.

5. Related work

In section 1, we discussed how PyReason extends on the early modern logic programming languages like Prolog [19], Epilog [20] and Datalog [34] by supporting annotations. Recent neuro symbolic frameworks show great promise in the ability to learn or modify logic programs to align with historical data and improve robustness to noise. Many such frameworks rely on an underlying diferentiable, fuzzy, first order logic. For example, logical tensor networks [ 1 ] uses diferentiable versions of fuzzy operators to combine ground and non-ground atomic propositions while logical neural networks [ 2 ] associate intervals of reals with atomic propositions and uses special parameterized operators. Meanwhile, induction approaches such as diferentiable ILP [ 3 ] fuzzy logic programs (using the product t-norm) are learned from data based on template rule structures in a manner that support recursion and multi-step inference. In [ 17 ], Logical Neural Networks was used interpret learned rules in a precise manner. Here also, gradient descent was used to train the parameters of the network. In the last two years, two paradigms have emerged with much popularity in the neuro symbolic literature. Logical Tensor Networks (LTN) [ 1 ] extend neural architectures through fuzzy, real-valued logic. Logical Neural Networks (LNN) [ 2 ] provide a neuro symbolic framework with parameterized operators that supports open world reasoning in the logic. As stated earlier, both can be viewed as a subset of annotated logic. Hence, PyReason can be used to conduct inference on the logic for both frameworks, in addition to providing key capabilities such as graph-based and temporal reasoning, which currently are not present in the logics of those frameworks.

In both the forward pass of various neuro symbolic frameworks [ 35, 2, 1 ], as well as for subsequent problems (e.g., entailment, abductive inference, planning, etc.), a deduction process is required. PyReason is designed to provide this precise capability. Generalized annotated programs [ 6 ] has been shown to capture a wide variety of real-valued, temporal, and fuzzy logics as it associates logical atoms with elements of a lattice structure as opposed to scalar values. As a result it can capture all the aforementioned logics, while retaining polynomial-time deduction due to the monotonicity of the lattice. The use of a lattice structure allows for us to associate logical constructs with intervals, thus enabling open world reasoning. In our recent work [ 7 ], we provided extensions to [ 6 ] that allows for a lower lattice structure for annotations. This enables the framework to capture paradigms such as LNN [ 2 ] and the MANCALog [ 9 ] for graph-based reasoning. However, that work only showed that analogs to the theorems of [ 7 ] for the lower lattice case and did not provide an implementation or experimental results.

By supporting generalized annotated logic, and its various extensions PyReason enables system design that is independent of the learning process. As a result, once a neuro symbolic learning process creates or modifies a logic program based on data, PyReason can be used to eficiently answer deductive queries (to include entailment and consistency queries) as well as support more sophisticated inference such as abductive inference or planning.

Today knowledge graphs are crucial in representing data for reasoning and analysis. Recent research on creation of knowledge graphs [36, 37] proposes methods to automatically convert conceptual models into knowledge graphs in GraphML format for enterprise architecture and a wide range of applications. PyReason, which supports the graphml format, could be an efective tool to reason about knowledge graphs obtained from one of these platforms.

6. Conclusion and Future Work

In this paper, we presented PyReason: an explainable inference software supporting annotated, open world, real-valued, graph-based, and temporal logics. Our modern implementation extends established generalized annotated logic framework to support scalable and eficient reasoning over large knowledge graphs and difusion models. We are currently working on a range of extensions to this work. This includes adding more temporal logic operators for specification checking, learning rules from data through induction, and using the inference process to create new knowledge in non-static graphs (e.g., adding nodes and edges). We will also look to explore how PyReason can be used in conjunction with LTN [ 1 ], and LNN [ 2 ]. In supporting frameworks such as these, we will look to add capabilities for symbol grounding [38], leveraging the results of the training process from frameworks such as LTN. Finally, we also plan on extending PyReason to act as a simulator for reinforcement learning based agents.

Acknowledgments

The authors are supported by internal funding from the Fulton Schools of Engineering and portions of this work is supported by U.S. Army Small Business Technology Transfer Program Ofice or the Army Research Ofice under Contract No.W911NF-22-P-0066. [19] A. Colmerauer, Prolog and infinite trees, Logic Programming 16 (1982) 2. [20] L. K. Schubert, C. H. Hwang, Episodic logic meets little red riding hood: A comprehensive, natural representation for language understanding, Natural language processing and knowledge representation: Language for Knowledge and Knowledge for Language (2000). [21] T. Yan, T. Y. Choi, Y. Kim, Y. Yang, A theory of the nexus supplier: A critical supplier from a network perspective, Journal of Supply Chain Management 51 (2015) 52–66. [22] L. Takac, M. Zabovsky, Data analysis in public social networks, in: International scientific conference and international workshop present day trends of innovations, 2012. [23] A. Dekhtyar, M. I. Dekhtyar, V. S. Subrahmanian, Temporal probabilistic logic programs, in: International Conference on Logic Programming, 1999, p. 109–123. [24] S. Khuller, M. V. Martinez, D. S. Nau, A. Sliva, G. I. Simari, V. S. Subrahmanian, Computing most probable worlds of action probabilistic logic programs: scalable estimation for 1030, 000 worlds, Ann. Math. Artif. Intell. 51 (2007) 295–331. [25] P. Shakarian, A. Parker, G. Simari, V. V. S. Subrahmanian, Annotated probabilistic temporal logic, ACM Trans. Comput. Logic 12 (2011). [26] M. V. França, G. Zaverucha, A. S. d’Avila Garcez, Fast relational learning using bottom clause propositionalization with artificial neural networks, Machine learning 94 (2014). [27] R. Agrawal, H. Mannila, R. Srikant, H. Toivonen, A. I. Verkamo, et al., Fast discovery of association rules., Advances in knowledge discovery and data mining 12 (1996) 307–328. [28] J. R. Quinlan, Learning logical definitions from relations, Machine learning 5 (1990). [29] A. Stanton, A. Thart, A. Jain, P. Vyas, A. Chatterjee, P. Shakarian, Mining for causal relationships: A data-driven study of the islamic state, in: ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, 2015, pp. 2137–2146. [30] P. Shakarian, A. Parker, G. Simari, V. V. Subrahmanian, Annotated probabilistic temporal logic, ACM Transactions on Computational Logic (TOCL) 12 (2011) 1–44. [31] P. Shakarian, G. I. Simari, V. Subrahmanian, Annotated probabilistic temporal logic: Approximate fixpoint implementation, ACM Transactions on Computational Logic (TOCL) 13 (2012) 1–33. [32] P. Sen, B. W. de Carvalho, R. Riegel, A. Gray, Neuro-symbolic inductive logic programming with logical neural networks, in: AAAI Conference on Artificial Intelligence, 2022. [33] J. N. Paredes, G. I. Simari, M. V. Martinez, M. A. Falappa, Detecting malicious behavior in social platforms via hybrid knowledge- and data-driven systems, Future Generation Computer Systems 125 (2021) 232–246. [34] S. Abiteboul, R. Hull, V. Vianu, Foundations of databases, volume 8, Addison-Wesley

Reading, 1995. [35] Z. Yang, A. Ishay, J. Lee, Neurasp: Embracing neural networks into answer set programming, in: International Joint Conference on Artificial Intelligence, IJCAI, 2020. [36] M. Smajevic, D. Bork, From conceptual models to knowledge graphs: a generic model transformation platform, in: 2021 ACM/IEEE International Conference on Model Driven Engineering Languages and Systems Companion (MODELS-C), IEEE, 2021, pp. 610–614. [37] P.-L. Glaser, S. J. Ali, E. Sallinger, D. Bork, Model-based construction of enterprise architecture knowledge graphs, in: Enterprise Design, Operations, and Computing: 26th International Conference, Springer, 2022, pp. 57–73. [38] S. Harnad, The symbol grounding problem, Physica D: Nonlinear Phenomena 42 (1990).

References

[1] S. Badreddine , A. d'Avila Garcez , L. Serafini , M. Spranger , Logic tensor networks , Artificial Intelligence 303 ( 2022 ) 103649 .

[2] R. Riegel , A. Gray , F. Luus , N. Khan , N. Makondo , I. Y. Akhalwaya , H. Qian , R. Fagin , F. Barahona , U. Sharma , S. Ikbal , H. Karanam , S. Neelam , A. Likhyani , S. Srivastava , Logical neural networks, 2020 .

[3] R. Evans , E. Grefenstette , Learning explanatory rules from noisy data , J. Artif. Int. Res . 61 ( 2018 ) 1 - 64 .

[4] M. Ma , J. Gao , L. Feng , J. Stankovic, STLnet: Signal temporal logic enforced multivariate recurrent neural networks , in: Advances in Neural Information Processing Systems , volume 33 , Curran Associates , Inc., 2020 , pp. 14604 - 14614 .

[5] P. Sen , B. W. Carvalho , I. Abdelaziz , P. Kapanipathi , S. Roukos , A. Gray , Logical neural networks for knowledge base completion with embeddings & rules , in: Conference on Empirical Methods in Natural Language Processing , 2022 , pp. 3863 - 3875 .

[6] M. Kifer , V. Subrahmanian , Theory of generalized annotated logic programming and its applications , J. Log. Program . 12 ( 1992 ) 335 - 367 .

[7] P. Shakarian , G. I. Simari , Extensions to generalized annotated logic and an equivalent neural architecture , in: 2022 TransAI , 2022 , pp. 63 - 70 .

[8] P. Shakarian , G. I. Simari , D. Callahan , Reasoning about complex networks: A logic programming approach , Theory Pract. Log. Program . 13 ( 2013 ).

[9] P. Shakarian , G. I. Simari , R. Schroeder , Mancalog: a logic for multi-attribute network cascades , in: International conference on Autonomous Agents and Multi-Agent Systems , AAMAS, 2013 , pp. 1175 - 1176 .

[10] U. Höhle , Probabilistic uniformization of fuzzy topologies , Fuzzy Sets and Systems ( 1978 ).

[11] C. Alsina , E. Trillas , L. Valverde , On some logical connectives for fuzzy sets theory , Journal of Mathematical Analysis and Applications 93 ( 1983 ) 15 - 26 .

[12] P. Vojtáš , Fuzzy logic programming , Fuzzy sets and systems 124 ( 2001 ) 361 - 370 .

[13] M. H. Van Emden , R. A. Kowalski , The semantics of predicate logic as a programming language , J. ACM 23 ( 1976 ) 733 - 742 .

[14] M. Fitting , Bilattices in logic programming , City University of New York, Lehman College, Department of Mathematics and Computer Science , 1990 .

[15] P. Shakarian , M. Broecheler , V. Subrahmanian , C. Molinaro , Using generalized annotated programs to solve social network difusion optimization problems , ACM Transactions on Computational Logic 14 ( 2013 ).

[16] H. Shindo , M. Nishino , A. Yamamoto , Diferentiable inductive logic programming for structured examples , in: AAAI Conference on Artificial Intelligence , 2021 , pp. 5034 - 5041 .

[17] P. Sen , B. W. S. R. d . Carvalho, R. Riegel , A. Gray , Neuro-symbolic inductive logic programming with logical neural networks , AAAI conference on Artificial Intelligence ( 2022 ).

[18] P. Hohenecker , T. Lukasiewicz, Ontology reasoning with deep neural networks , in: Journal of Artificial Intelligence Research , volume 68 , 2020 , pp. 503 - 540 .