Provenance refers to the task of identifying and tracing the axiomatic origins of a consequence from a knowledge base. Semiring provenance uses two operators to represent (i) axioms that together yield the consequence and (ii) the diferent possible derivations. To-date, most provenance approaches are limited to inexpressive logics mainly due to the dificulty in dealing with complex constructors like negations. We surpass this issue through a general notion of provenance for interpretation-based semantics. We then show how weighted automata can be exploited to compute this provenance, hence providing an efective method for computing the provenance of ℒ consequences.
The question of tracing the provenance of consequences has gained quite some interest over the last years, being translated to and used for dealing with many diferent knowledge representation languages. In its basic form, provenance refers to the task of tracing the “origin” or “sources” of a given consequence, among the pieces of knowledge available—that is, the axioms of a knowledge base—and, perhaps, rules for manipulating them.
Semiring provenance refers to a general framework that uses two operators—the “addition”
and “product” of the semiring—to represent the full provenance of a consequence. In a nutshell,
the product is used to express which axioms can combine to produce the consequence, while
the addition represents diferent possible derivations of the same result. Although the name
originates from the database community [
Existing definitions of semiring provenance over diferent languages have a common feature:
they rely (sometimes implicitly) on a notion of “proof.” The idea is that the provenance
information does not only indicate which pieces of knowledge are responsible for a consequence, but
also how they interact for the derivation. The disadvantage of such a view is that it becomes
dificult to apply in knowledge representation languages for which a natural definition of a
proof is unavailable, or dificult to handle within the semiring operations. One example of
such a language is the description logic ℒ [
When an ℒ KB entails a consequence, it is often important to understand which of the constraints (axioms) are violated. Here, provenance comes into play. And yet, it is unclear how to define the provenance in this situation due, as mentioned already, to the lack of a notion of proof which can be manipulated in this language. To alleviate this issue, we introduce a general notion of provenance which depends, instead, on an interpretation-based semantics. Intuitively, the provenance of a consequence is based on the combinations of axioms that exclude each possible interpretation not satisfying the consequence. Through this idea, we provide a sound notion of provenance which is suitable for ℒ, but also for any KR language with interpretation-based semantics.
The next question is whether this provenance can be efectively computed. We provide a
positive answer to this question whenever the underlying KR language allows for an
automatabased decision procedure, under minor assumptions. In brief, we check that a decision procedure
based on an axiomatic automaton—which encodes the automata for all the sub-KBs of a given
KB—can be modified into a weighted automaton (over a semiring) whose behaviour corresponds
precisely to the provenance of the consequence. We also show how to compute this behaviour,
for arbitrary weighted tree automata. In addition, we show that the behaviour computation
requires only polynomial time in the number of states, although potentially exponential time
on the number of transitions. Yet, for some specific cases (as when the semiring is a lattice)
the latter exponential time upper bound can be reduced. Since there exist automata-based
procedures for reasoning in ℒ and other DLs [
It is important to consider that, although our motivation arises from trying to understand the consequences of a KB, the formalism presented in this paper is very general. Our definition of provenance is applicable to any knowledge representation language with interpretationbased semantics; and the automata-based provenance computation algorithm works for any consequence that can be decided through an axiomatic automaton. The main limitation is that our proofs of correctness require the underlying semiring to be distributive, idempotent, and commutative. Yet, as we argue at the end of the paper, relaxing any of these conditions is likely to have important negative consequences on the complexity of the problem.
We assume basic knowledge of DLs [14] and in particular of ℒ. We provide the background knowledge on semirings and weighted automata needed for understanding the rest of this work.
A semiring is an algebraic structure S = (, ⊕ , ⊗ , 0, 1) where ⊕ and ⊗ are two associative binary operators over , called the addition and product, respectively, such that ⊕ is commutative and has neutral element 0; 1 is the neutral element of ⊗ ; and ⊗ distributes over ⊕ on both sides.1 As usual, ⊗ has precedence over ⊕ .
Such a semiring is commutative if ⊗ is commutative, ⊕ -idempotent if ⊕ = for all ∈ , and ⊗ -idempotent if ⊗ = for all ∈ . S is idempotent if it is both, ⊕ - and ⊗ -idempotent.
In the context of provenance, for reasons that will become clear later, one often considers commutative idempotent semirings. A typical example of such a semiring is the structure L = (, ∨, ∧, 0, 1), where is a bounded distributive lattice, ∨ and ∧ are the join and meet operators of , and 0 and 1 are its least and greatest elements, respectively. A semiring or lattice S is distributive if both operations distribute over each other. Distributive lattices have the additional property of being annihilating: for any two elements , ∈ , it holds that ⊗ ( ⊕ ) = = ⊕ ( ⊗ ). Importantly, other distributive idempotent semirings exist, and other types of semiring may be of interest in diferent contexts [15, 16, 17].
In this paper, we follow a common approach from provenance and consider distributive idempotent and commutative semirings only. A useful observation is that if (, ⊕ , ⊗ , 0, 1) is a distributive idempotent commutative semiring, then so is its dual semiring S := (, ⊗ , ⊕ , 1, 0). That is, exchanging the product and addition operations yields a new semiring. In the following sections, we will resort to this dual semiring for some constructions and computations.
From now on, unless otherwise specified, S refers to an arbitrary–but fixed–distributive idempotent commutative semiring over the set , S = (, ⊕ , ⊗ , 0, 1), and to an element of .
Weighted tree automata generalise tree automata by allowing weights—from a given semiring— on their transitions [18, 19]. We consider only weighted automata on infinite trees [17, 20]. Given a number ∈ N, we denote as the set {1, . . . , }, and * is the set of all finite words over . We see * as an infinite tree, where each word ∈ * is a node interpreted in the standard manner, with being the root and the -th successor of . For a set , an -labelled tree is a function lab : * → which assigns an element of to each node of the tree. To make the reference to a tree explicit, we often name the function lab as . For a node ∈ * , →−−lab() − denotes the tuple (lab(), lab(1), . . . , lab()).
Definition 1 (weighted automata). Let S be a semiring and ∈ N. A weighted looping tree automaton (WTA) over S for arity is a tuple = (, in, wt) where is a finite set of states; in : → is the initial weight function; and wt : +1 → is the transition weight function.
A run of the WTA is a -labelled tree : * → . The class of all runs of is denoted by run. The weight of the run is wt() := ⨂︀∈* w→t−− (−()). The behaviour of the WTA is ‖‖ :=
⨁︁ in(()) ⊗ wt().
Weighted tree automata generalise unweighted tree automata [21]. A looping tree automaton (LTA) is a tuple = (, , ∆) where is the set of states, ⊆ is the set of initial states, and ∆ ⊆ +1 is the transition relation—recall that is the tree arity. Consider now the Boolean 1Typically, but not always, 0 is required to annihilate over ⊗ . semiring B := ({0, 1}, ∨, ∧, 0, 1), where ∨ and ∧ are the standard Boolean disjunction and conjunction over the truth values 0 (false) and 1 (true). The LTA (, , ∆) can be seen as the weighted automaton (, in, wt) over B where in and wt are the characteristic functions of and ∆ , respectively. Under this view, accepted runs are those with weight 1, and the automaton is non-empty (accepts at least one run) if its behaviour is 1—and is empty if its behaviour is 0. Note that since we only consider distributive, idempotent, and commutative semirings, the behaviour of a WTA is well-defined.
Despite being a special case, for consistency and readability we use the notation (, , ∆) when dealing with LTA and (, in, wt) when dealing with WTA. Both types of automata will be denoted with , allowing the context to clarify if it is a TA or a WTA.
The basic idea behind provenance is to keep track of the diferent combinations of axioms in a knowledge base which yield a consequence of interest. In logic-based KR languages, this is usually instantiated as a mirror of how (derived) consequences can be combined to yield new (previously implicit) consequences. The issue with this approach is that provenance semantics must be defined anew for each logical formalism, and it is not obvious how to define the provenance in settings where consequences are not cumulative in this sense. For instance, it is not obvious how to define provenance for ℒ consequences in this manner. We introduce a general notion of provenance based on (tree-shaped) interpretation semantics. Definition 2 (KR language). A KR language is a triple (T, I, |=) where T is a potentially infinite set of axioms, I is a class of labelled trees called interpretations, and |= ⊆ I × T is the binary satisfiability relation . A knowledge base (KB) is a finite set of axioms ⊆ T. The interpretation ∈ I is a model of the KB if |= for all ∈ . An axiom ∈ T is a consequence of a KB (denoted |= ) if |= holds for every model of .
Under this definition, the consequence relation between KBs and axioms is monotonic: adding more axioms to a KB can never remove a consequence. DLs are examples of KR languages (Φ , I, |=), where Φ is the set of all GCIs, I is the class of all DL interpretations, and |= ⊑ if ⊆ as usual. In this case, a KB (called often TBox in DL) is inconsistent if |= ⊤ ⊑ ⊥. We fix an arbitrary KR language (T, I, |=), and assume that every axiom is annotated with an element of the semiring S. The provenance of a consequence traces the combinations of axioms that yield it, as formalised next.
Definition 3 (provenance). Let S be a semiring and (T, I, |=) a KR language. An annotated KB is a pair ( , lab) where ⊆ T and lab : → . The provenance of ∈ T w.r.t. the annotated KB ( , lab) is Prov ( ) := ⨂︀∈I,̸|= ⨁︀ ∈ ,̸|= lab( ).
We analyse this definition in more detail. Traditionally, provenance is defined as an addition of products of labels referring to combinations of axioms that yield a consequence. We take a dual approach inspired by an approach from process analysis [22]. For to be a consequence, any interpretation that does not satisfy must be excluded from the set of models; this is expressed by the outer product. The “addition” ⨁︀ ∈ ,̸|= lab( ) intuitively expresses that at least one axiom violated by is needed to exclude . This is clarified by the following example. 1 2 3 Example 4. Consider the annotated ℒ KB
:= {⊤ ⊑ ∃., ⊤ ⊑ ∀., ⊓ ⊑ ⊥, ⊑ ¬}, with the axioms labelled as 1, . . . , 4, respectively. is inconsistent; that is, |= ⊤ ⊑ ⊥. To compute the provenance for inconsistency, we have to multiply over all interpretations (since none satisfies ⊤ ⊑ ⊥) the addition of the labels of the axioms they violate. Since we consider only idempotent semirings, it sufices to partition I by the axioms they violate. Representatives of these classes are depicted in Figure 1. The interpretation 1 violates 1 only. 2 violates 2 and 4 yielding 2 ⊕ 4; and 3 similarly yields 3 ⊕ 4. Prov (⊤ ⊑ ⊥) is the product of those additions: 1 ⊗ (2 ⊕ 4) ⊗ (3 ⊕ 4).
If the semiring S is annihilating, distributing this expression yields (1 ⊗ 4) ⊕ (1 ⊗ 2 ⊗ 3). The attentive reader will notice that the sets of axioms corresponding to each of these products (that is, {⊤ ⊑ ∃., ⊑ ¬}, and {⊤ ⊑ ∃., ⊤ ⊑ ∀., ⊓ ⊑ ⊥, }) characterise the minimal inconsistent sub-KBs; also known as justifications in the DL literature [23, 24].
As this example suggests, our definition of provenance traces the axioms that are responsible
for a consequence. Consider the notion of a justification of a consequence w.r.t. a KB as a
(subset-) minimal sub-KB that entails the consequence [24, 25]. If the underlying semiring is
annihilating, the provenance of a consequence can be obtained by operating over the labels of
the axioms appearing in the justifications [ 26]. Thus, as expected, our notion of provenance
generalises that of justification-based explanations; also known as axiom pinpointing [
From a diferent point of view, this definition also generalises reasoning problems based on Gödel (fuzzy) logic or min-based possibilistic logic [27, 28]. Despite the simplicity of Example 4, it is in general not obvious how to compute the provenance of a consequence. In fact, a direct application of Definition 3 is made impossible from the fact that the class I of interpretations is potentially infinite. In Example 4 we had to resort to a partition of I into equivalence classes defined by the axioms each interpretation violates. In more general settings, or as the number of axioms grows, it is not obvious how to apply this approach. In Section 5 we see that for the special case of ℒ, creating and handling this partition is always possible.
Next we develop a method for computing the provenance of consequences for arbitrary KR languages having automata-based decision processes, with only some minor limitations.
Recall that it is possible, for a given ℒ TBox , to construct an automaton whose runs characterise the models of . Consistency can thus be verified through an emptiness test of the constructed automaton: does it accept at least one successful run? The automaton is empty if is inconsistent. Similarly, our definition of provenance requires us to operate, akin to the behaviour of weighted automata, over all possible interpretations. This suggests that it should be possible to modify the automata-based decision procedure into the problem of computing the behaviour of an adequate weighted automaton.
Before formally describing the construction of the weighted automaton, two things should be taken into account. First, there is a duality between the emptiness of an automaton, and the consequence of interest. If the consequence (in the case of ℒ inconsistency) holds, then its automaton is empty; that is, its behaviour is 0—which is usually interpreted as not having a property. Dualising the Boolean semiring and using B instead yields the “intuitive” answer of 1 when the consequence follows. Building on this intuition, the weighted automaton uses the dual structure S instead of the original one S.
Second, the automata-based decision procedure for a consequence cannot be based on an arbitrary construction; rather, it should grasp the efect of each axiom from the KB over the derivation of the consequence. Otherwise, it becomes impossible to trace the provenance of the consequence. To deal with this issue, we recall the notion of axiomatic automata from [29]. Briefly, we consider automata-based decision procedures which take a KB and an axiom , and construct a LTA , such that |= if , is empty. To grasp the influence of the axioms in the KB over the consequence, we consider only automata that “contain”—in a sense that will become clear briefly—all the automata for each sub-KB ′ ⊆ . The idea is that the automaton ′, for each ′ ⊆ can be obtained by adding states and transitions to , . This is achieved through restricting functions.
Definition 6 (restricting functions). Let = (, , ∆) be a LTA of arity , and a KB. A transition restricting function is a function ∆ res : → P(+1); an initial restriction function is a function res : → P(). They are extended to sets of axioms in ′ ⊆ by defining ∆ res( ′) := ⋂︁ ∆ res( ), ∈ ′ res( ′) := ⋂︁ res( ). ∈ ′ Given ′ ⊆ , the ′-restricted subautomaton of w.r.t. ∆ res and res is the LTA | ′ := (, ∩ res( ′), ∆ ∩ ∆ res( ′)).
The restricting functions express which of the initial states and transitions are allowed for a given axiom ∈ . Hence, if a whole set of axioms is considered, only the elements of that are allowed by all of them (the intersection) can be included. By including more axioms in a sub-KB, we disallow more initial states and transitions, which makes it more likely to obtain an empty automaton. This is coherent with the monotonicity of consequences. This also simulates the notion of entailment from Definition 2. Each run of the automaton acts as a representative of a class of interpretations, and the restricting functions as a means to express which interpretations are satisfied by which axioms.
Definition 7 (axiomatic automata). Let = (, , ∆) be an LTA of arity , a KB, and ∆ res : → P(+1), res : → P() restriction functions. The triple (, ∆ res, res) is called an axiomatic automaton for . Let be an axiom such that |= . The axiomatic automaton (, ∆ res, res) is correct for |= (w.r.t. the underlying KR language) if for every ′ ⊆ it holds that ′ |= if | ′ is empty.
Under this definition, we can check which combinations of axioms entail a consequence simply by checking emptiness of the restricted automata as long as the axiomatic automaton is correct for this consequence relation. The next step is to transform a correct axiomatic automaton for |= into a process that computes the provenance of the consequence w.r.t. the labels of the axioms in . The approach constructs a weighted automaton whose behaviour corresponds precisely to the desired provenance. The main idea is very natural: we combine the information from the axiomatic automaton with the notion of axioms that are violated in an interpretation to keep track of the provenance operations. In this sense, the weights of the automaton correspond to the annotations of the axioms that they violate; these are expressed through two violating functions, constructed over the restricting functions. Recall that we consider a fixed but arbitrary distributive semiring S = (, ⊕ , ⊗ , 0, 1). Moreover, as usual, we define ⨁︀∈∅ := 0; i.e., an addition over an empty set is the neutral element 0. Definition 8 (provenance automata). Let (, ∆ res, res) be an axiomatic automaton for |= with = (, , ∆) of arity . The violating functions ∆ vio : +1 → and vio : → are: ∆ vio(0, 1, . . . , ) :=
lab( ), vio() := ⨁︁ { ∈ |(0,...,)∈/Δres( )} ⨁︁ { ∈ |∈/res( )} lab( ).
The provenance automaton induced by (, ∆ res, res) is the WTA over S = (, ⊗ , ⊕ , 1, 0) Prov := (, in, wt) where: in() := {︃vio() ∈ , 1 otherwise; wt(0, . . . , ) := {︃∆ vio(0, . . . , ) (0, . . . , ) ∈ ∆ , 1 otherwise.
If a run of is accepted by then its weight is wt() = ⨁︀∈ ∆ vi →o−− (−());2 otherwise, wt() = 1. From the definition of ∆ vio, this expression resembles the internal addition in the definition of provenance (Definition 3). This is not coincidental. The behaviour of the automaton Prov, which applies ⊗ over the weights of all runs yields the provenance as expected. Theorem 9. If (, ∆ res, res) is correct for |= , then ‖Prov‖ = Prov ( ).
This result tells us that the behaviour of the WTA Prov yields the provenance of a consequence; yet, we still do not know how to compute this behaviour. To our knowledge, the only efective algorithms for computing the behaviour of weighted automata appear in [ 29, 30]. Abstracting from the acceptance conditions that they handle, the proofs of their correctness rely on specific properties of distributive lattices and are not directly applicable to our case where distributive semirings are considered. We provide an algorithm that builds on the ideas of the standard emptiness test approach for unweighted automata [31]. 2Recall that we are using the dual semiring S, where the semiring “product” is ⊕ .
weight of all successful runs of . From the distributivity of S, it follows that Let be a WTA over the semiring S. To compute the behaviour of , we need to compute the ‖‖ =
⨁︁ in(()) ⊗ wt() = ⨁︁ in() ⊗ the addition of the weights of all runs starting with ; that is, swt() = ⨁︀∈run Based on this insight, we construct a function swt : → computing, for each state ∈ , ,()= wt().
This function is constructed recursively, by considering runs of increasing depth. We start with the function swt0 where swt0() := 0 if for all 1, . . . , ∈ , wt(, 1, . . . , ) = 0 and swt0() = 1 otherwise. It identifies the weights of runs of depth 0; that is, those that only contain the root node, and allow for at least one transition. Then we iteratively construct for each ∈ N the functions: swt+1() = swt() ⊕
wt(, 1, . . . , ) ⊗ ⨁︁ (︂ 1,...,∈ =1 ⨂︁ swt() .
︂)
It is easy to verify, based on distributivity, that swt() yields the sum of all the runs of depth at most starting with the state . Let swt be the limit of the functions swt as grows to infinity. Then we get the following result.
Theorem 10. Let be a WTA and swt the function defined above. ‖‖ = ⨁︀∈ in() ⊗ swt().
Let ():={ ∈ | ∃0, . . . , ∈ .wt(0, . . . , ) = } be the set of all weights appearing in . All values appearing in the functions swt belong to the semiring generated by (); that is, they are constructed through arbitrary additions and products of elements of ().3 Due to distributivity, every such element can be rewritten in monomial form; that is, it can be expressed as an addition of monomials, where a monomial is a product of elements of (). Idempotency allows us to restrict this even further, by requiring that each monomial appears at most once in the addition, and each element of () appears at most once in a monomial. Note that since S can be any arbitrary distributive idempotent semiring, and the weights of the transitions can be arbitrary elements of , the monomial form of an element may not be unique. For our purposes, it sufices to know that there always exists one.
Define a partial ordering over the elements of as follows. Let , ∈ ; is contained in (denoted ⊆ ) if there are monomial forms of and such that every monomial from appears also in . One can see that for every ∈ N and every ∈ it follows that swt() ⊆ swt+1(); that is, the construction of swt is monotonically increasing and swt is its least fixpoint [ 32]. This maximal element ˆ := ⨁︀ ⊆ () ⨂︀ ∈ constructed as ifxpoint is bounded from above by the the sum of all possible monomials over ().
By the previous arguments, if there is an ∈ N such that swt = swt+1, then swt = swt. To understand how expensive it is to compute swt is sufices to bound the number of iterations that yield diferent functions. Since swt() ⊆ swt+1(), if swt ̸= swt+1 there exists some 3In particular, 1 is the monomial formed by empty products, and 0 is the object with an empty addition of monomials. state ∈ and a monomial appearing in swt+1() but not in swt(). That is, every strictly increasing iteration must add at least one monomial to some state. The number of monomials is bounded by 2|()|; thus after at most || · 2|()| iterations the fixpoint is found. Assuming that semiring operations take constant time,4 each iteration requires as many operations as there are transitions in ; i.e., |+1| of them for each state. Thus, the time for each iteration is bounded polynomially by the number of states of yielding the following result. Theorem 11. The behaviour of a WTA = (, in, wt) over a distributive, commutative, idempotent semiring S can be computed in time polynomial in || but exponential on the cardinality of the range of wt.
As usual, this upper bound is based on the worst-case scenario and can be reduced in special
cases. For instance, if S is a distributive lattice, the annihilation property limits the class of
monomials of interest to (perhaps surprisingly) a polynomial tree-depth, yielding a polynomial
upper bound over || which does not depend explicitly on the range of wt [26, 29].
5. Provenance in ℒ
We now pivot to the special case of ℒ and show how the automata-based approach can be
used to trace the provenance of inconsistency of a TBox in this setting. The automata-based
decision procedure for ℒ TBox inconsistency tries to construct a special kind of tree-shaped
model called a Hintikka tree [
Given a TBox , sub( ) denotes the set that contains ¬ ⊔ for each ⊑ ∈ , and is closed under subconcepts. A set ⊆ sub( ) is a Hintikka set if (i) ⊓ ∈ implies {, } ⊆ ; (ii) ⊔ ∈ implies {, }∩ ̸= ∅; and (iii) for every ∈ {, ¬} ̸⊆ . In words, a Hintikka set is a logically consistent set of concepts, which preserves the semantics of ⊓ and ⊔. Such a set is compatible with the GCI ⊑ if either = ∅ or ¬ ⊔ ∈ .
Hintikka sets label the nodes of the tree, and existential restrictions are satisfied by their successors. Let be the number of existential restrictions in sub( ). To know which successor refers to which existential restriction we fix an arbitrary bijection : {∃. | ∃. ∈ sub( )} → . Some successors will be labeled with the dummy Hintikka set ∅ to keep the constant arity . The tuple of Hintikka sets (0, 1, . . . , ) satisfies the Hintikka condition if for every ∃. ∈ sub( ), (i) if ∃. ∈ 0, then {} ∪ { | ∀. ∈ 0} ⊆ (∃.); and (ii) if ∃. ∈/ 0, then (∃.) = ∅. It is compatible with the GCI if 0, . . . , are all compatible with .
Definition 12 (ℒ automaton). Let be a TBox and the number of existential restrictions in sub( ). The axiomatic automaton for is the triple ( , ∆ res , res ) where = (, ∆ , ) with the set of all Hintikka sets and ∆ the set of tuples satisfying the Hintikka condition; ∆ res maps each ∈ to the set of tuples compatible with ; and res ( ) = for all ∈ . 4Depending on the structure of S, this assumption may require a more precise specification. For instance [ 29] introduce structure sharing for eficient calculations.
For the case of ℒ, the fundamental element is ∆ res , which guarantees that all nodes in the tree satisfy the GCIs of the sub-TBox of interest. Or, from a dual view, can be used to see which axioms are violated in a tree-shaped interpretation.
Theorem 13. The axiomatic automaton ( , ∆ res , res ) is correct for w.r.t. inconsistency.
Prov yields the provenance for inconsistency of the TBox
By Theorem 9, the behaviour of . Thus this provenance can be efectively computed.
As usual for ℒ and other DLs, the approach for dealing with inconsistency can be applied, with minor variations, to other reasoning tasks. For instance, if one is interested in verifying whether a concept is unsatisfiable w.r.t. —that is, whether every model of is such that = ∅—it sufices to modify the set of initial states of the automaton (Definition 12) to contain only those Hintikka sets that include the concept . Then, the provenance for the entailment of ⊑ w.r.t. becomes the provenance for unsatisfiability of ⊓ ¬.
Consider once again Example 4. Under the assumption of annihilation, we first computed the provenance to be equivalent to 1 ⊗ (2 ⊕ 4) ⊗ (3 ⊕ 4). It turns out that each of these additions characterises a so-called diagnosis: a minimal set of axioms that, when removed from the KB, cancel the consequence [33]. For instance, we notice that if we remove the first axiom, the resulting KB {⊤ ⊑ ∀., ⊓ ⊑ ⊥, ⊑ ¬} is consistent. This is consistent with the wellknown duality between justifications and repairs, observed in diferent domains [ 34, 35, 36, 37]. Thus, if rather than explaining a consequence through its provenance one was interested in removing it, one could use a similar technique to compute this “correction provenance.” The only necessary change would be to consider the original semiring S as underlying the weights of the provenance automaton, rather than the dual S as done for provenance.
One assumption that we make in the definition of general KR languages (see Definition 2) is that any combination of axioms can form a KB—indeed, a KB is defined as a set of axioms. In some cases, it makes sense to restrict the class of KBs to so-called admissible sets of axioms, where if a set is admissible, then any subset of is also admissible [38]. For instance in expressive description logics, some axioms can only be used if the symbols that appear in them do not appear in other axioms [39]. Importantly, even if we restrict the KBs of KR languages to such admissible sets of axioms, the definition of an axiomatic automaton and the construction of the provenance automaton as presented above still work. Hence, our approach is general enough to handle also the settings discussed in [38].
We have considered a semantic notion of provenance, which can be readily applied to arbitrary knowledge representation languages that allow for an interpretation-based consequence relation. In contrast to other existing notions of provenance [40, 41, 42], our notion does not depend on an executional consequence relationship between the axioms in a knowledge base, but rather on how they combine to exclude interpretations negating the consequence of interest. The advantage of our definition is that it allows us to handle provenance in languages where consequence-based reasoning methods are not available, or require awkward constructions.
At first sight, our definition of provenance may not be very intuitive. It is based on finding the combinations of axioms that guarantee consequences to be entailed, taking into consideration the interpretation-based semantics. As a means to justify our approach, we show that it naturally generalises one of the best known special cases of provenance; namely, that of finding all subsetminimal sub-KBs that entail the consequence. Moreover, it generalises the cases of weighted reasoning where weights come from a distributive lattice [43]. It is worth mentioning that, while we use axiom pinpointing as a motivation and an example for the formalism, the approach is applicable to provenance over any distributive, idempotent, and commutative semiring.
From a practical point of view, we showed how to transform any axiomatic automaton which is correct for deciding a consequence, into a weighted automaton whose behaviour corresponds precisely to the provenance of the consequence. We also provide an efective algorithm for computing this behaviour by recursively considering runs of increasing length. Computing the provenance is not more expensive than standard reasoning (based on automata emptiness), except for a potential exponential overhead on the number of diferent transition weights.
To showcase the importance and use of our definitions, we instantiated the framework on
ℒ. Although there exist consequence propagation methods for this logic [
One may consider that limiting the framework to distributive, idempotent, commutative semirings is a very strong restriction. Yet, these assumptions are justified in the context of our framework. Idempotency and commutativity are relatively common requirements in the context of provenance for expressive languages; see e.g., [41]. Indeed, there is some evidence that a lack of idempotency yields to a high complexity, and perhaps even undecidability of provenance-related problems. If the operators are not commutative, then one can construct increasingly long monomials, in detriment to the resource upper bounds derived. Distributivity, on the other hand, is useful for the automata behaviour computation. Indeed, it is known that even for the case of lattice-valued WTA, the polynomial-time upper bounds depend strongly on distributivity [44]. Moreover, the construction of the provenance automaton depends on the dualisation of the semiring, which is only guaranteed for the class of algebras considered here. This last issue can be solved by considering diagnose-based provenance, instead of explanations. On the other hand, some applications of provenance do consider less restrictive scenarios looking at e.g., the Viterbi semiring whose product is not idempotent or the tropical semiring with non-idempotent addition.
Some automata-based reasoning methods are not based on the interpretation semantics, but follow a more consequence-based approach of building “proofs” for the derivation of a consequence. Examples of this view are propositional resolution [45] and the completion-based approach for ℰℒ [46]. In future work we will study the connection between these automata-based approaches, and verify whether provenance can be computed eficiently over them.
This work was partially supported by the MUR for the Department of Excellence DISCo at the University of Milano-Bicocca and under the PRIN project PINPOINT Prot. 2020FNEB27, CUP H45E21000210001. [14] F. Baader, D. Calvanese, D. McGuinness, D. Nardi, P. Patel-Schneider (Eds.), The Description Logic Handbook: Theory, Implementation, and Applications, second ed., Cambridge University Press, 2007. [15] A. Kaya, M. Satyanarayana, Semirings satisfying properties of distributive type, Proceedings of the American Mathematical Society 82 (1981) 341–346. [16] F. Pastijn, Y. Guo, The lattice of idempotent distributive semiring varieties, Science in
China Series A: Mathematics 42 (1999) 785–804. doi:10.1007/BF02884266. [17] Z. Fülöp, H. Vogler, Weighted tree automata – may it be a little more?, 2022. doi:10.48550/
ARXIV.2212.05529. [18] H. Seidl, Finite tree automata with cost functions, in: J. C. Raoult (Ed.), CAAP ’92, Springer,
Berlin, Heidelberg, 1992, pp. 279–299. [19] M. Droste, W. Kuich, H. Vogler, Handbook of Weighted Automata, EATCS, 1st ed., Springer, 2009. [20] M. Droste, G. Rahonis, Weighted automata and weighted logics on infinite words, in: Proc. of DLT 2006, volume 4036 of Lecture Notes in Computer Science, Springer, 2006, pp. 49–58. doi:10.1007/11779148_6. [21] H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, C. Löding, S. Tison, M. Tommasi, Tree automata techniques and applications, 2008. [22] D. Deutch, Y. Moskovitch, V. Tannen, A provenance framework for data-dependent process analysis, Proc. VLDB Endow. 7 (2014) 457–468. doi:10.14778/2732279.2732283. [23] R. Peñaloza, Explaining axiom pinpointing, in: C. Lutz, U. Sattler, C. Tinelli, A. Turhan, F. Wolter (Eds.), Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, volume 11560 of Lecture Notes in Computer Science, Springer, 2019, pp. 475–496. doi:10.1007/978-3-030-22102-7_22. [24] M. Horridge, J. Bauer, B. Parsia, U. Sattler, Understanding entailments in OWL, in: Proceedings of the Fifth OWLED Workshop, volume 432 of CEUR Workshop Proceedings, CEUR-WS.org, 2008. URL: http://ceur-ws.org/Vol-432/owled2008eu_submission_23.pdf. [25] R. Peñaloza, Axiom pinpointing, in: Applications and Practices in Ontology Design, Extraction, and Reasoning, volume 49 of Studies on the Semantic Web, IOS Press, 2020, pp. 162–177. URL: https://ebooks.iospress.nl/volumearticle/56013. doi:10.3233/SSW200042. [26] F. Baader, M. Knechtel, R. Peñaloza, Context-dependent views to axioms and consequences of semantic web ontologies, J. Web Sem. 12–13 (2012) 22–40. doi:10.1016/j.websem. 2011.11.006. [27] N. Preining, Gödel logics – a survey, in: Logic for Programming, Artificial Intelligence, and Reasoning, Springer, Berlin, Heidelberg, 2010, pp. 30–51. [28] D. Dubois, H. Prade, Possibilistic logic - an overview, in: Computational Logic, volume 9 of Handbook of the History of Logic, Elsevier, 2014, pp. 283–342. doi:10.1016/ B978-0-444-51624-4.50007-1. [29] F. Baader, R. Peñaloza, Automata-based axiom pinpointing, J. Automated Reas. 45 (2010) 91–129. doi:10.1007/s10817-010-9181-2. [30] M. Droste, W. Kuich, G. Rahonis, Multi-valued MSO logics over words and trees, Fundamenta Informaticae 84 (2008) 305–327. [31] M. Y. Vardi, P. Wolper, Automata-theoretic techniques for modal logics of programs, Journal of Computer and System Sciences 32 (1986) 183–221. doi:10.1016/0022-0000(86)