From TAMI

Analyzing the AIR Language : A Semantic Web (Production) Rules Language

Authors: Ankesh Khandelwal (Thanks to Jie Bao for his guidance and feedback on parts of this work)

Abstract

Accountability in RDF (AIR) language is an N3 based, Semantic Web production rules language, with support for logical negation for closed world reasoning. AIR reasoner computes closure for facts, in RDF, with respect to AIR rules and provides explanations for the inferred facts. The explanations generated by the reasoner can be declaratively modified by attaching natural language descriptions to the rule actions and by hiding actions of certain rules, to either save sensitive information from being revealed or to reduce the size of explanations. AIR leverages a rich set of built-ins from N3Logic and some of its own to support scoped contextualized reasoning, scoped negation and querying of SPARQL end points. In this paper, we present an in depth analysis of the AIR language. First, we provide a declarative semantics of AIR rules through translation to stratified Logic Program (LP). Then, we show that specialized classes of stratified LPs can be losslessly rewritten in AIR, and suggest an incremental change to AIR to support all classes of stratified LPs. We also show that SPARQL queries can also be losslessly rewritten using AIR. Finally, we compare AIR with other rule systems.

1. Introduction

AIR [KHW2008] was developed as an extension to N3Logic [BCKSH2008] and was structured to meet the requirements of the Web information systems. Some of the design features of AIR language are as follows :

1. It is grounded in N3 [B2005]. N3 provides a human-readable syntax for RDF, which is more easily writable, readable and is more symmetrical than the RDF/XML syntax. N3 extends expressiveness of RDF with abilities to use graphs as literal values, variables (universally or existentially quantified) over a graph and built-in functions and operators represented as RDF properties.
2. It supports contextually scoped reasoning, like N3Logic.
3. The rules have unique ids (IRIs), so that they are part of the linked data cloud. In that way the rule definitions can be reused.
4. The rules are defined as production rules of the form if <condition> then <then-actions>s else <else-action>s. All the then-actions are effected when the condition succeeds. Similarly, all the else-actions are effected when the condition fails.
5. The rule conditions are expressed in graph patterns, similar to SPARQL [SP2008] (BGPs). The conditions are pattern matched against N3 graphs.
6. AIR supports nested activation of rules through nesting of rules. This leads to better expressivity because the splitting of conditions into sequentially activated rules appears to provide a more natural way to model real world rules and laws.
7. The actions can assert triples to the fact base or activate a nested rule.
8. The actions can be associated with natural language descriptions, which are included in the justification produced by the reasoner.
9. The justifications are encoded in N3.
10. The explanations for actions by certain rules can be hidden, because justifications can potentially reveal sensitive information from the knowledge base or expose any bias.

While AIR has production rule syntax, the negation in AIR is logical because AIR is limited to assertions of facts (and addition of new rules), and neither facts can be removed from the current state of the world nor any procedural attachments be called. In context of Logic Programs (LP), Przymusinski [P1988] states that "finding a suiltable declarative or intended semantics for logic programs(LP) is one of the important problems, especially finding a suitable formalization of the type of non-monotonic reasoning used in the LP. The semantics must be associated with any LP P so that we know what facts can be inferred from it. The semantics of a logic program P can be declarative or procedural. The declarative semantics can be specified in proof-theoretic or model-theoretic ways. The procedural semantics of an LP is specified by providing a procedural mechanism."

In this work we will define the declarative semantics of the AIR-program in model-theoretic way, by translating the AIR-program to a stratified LP. Earlier Jess ⁴, a production rule language, has been translated from and to Situated Ordinary LP (SOLP) ⁵ and Situated Courteous LP (SCLP) [GGF2002], showing interoperability of the two rule languages. However, Jess and AIR are very different rule languages. Jess, unlike AIR, supports procedural attachments and it's negation is same as the (stratified) Negation as Failure (NAF) [GGF2002]. Not only is the notion of nesting of rules absent from Jess, we will also see that AIR's negation is different from NAF. The authors are not aware of any other related work.

The remainder of the paper is organized as follows. Section 2 introduces the AIR language syntax and AIR reasoning. In section 3 we review LP related concepts and define a specialized class of stratified LP - Positively Stratified Negatively Hierarchical LP (PSNHLP). In section 4, we define the translation of AIR-Program to PSNHLP, and prove some claims on the complexity of AIR language based off the translation. In section 5, we compare AIR with different classes of LPs, and SPARQL [SP2008] queries. In the following section we compare AIR with other rule systems. We conclude in section 7, with a discussion on future work.

2. AIR overview

The AIR production rule system has two components- the AIR language and the AIR reasoner. The AIR reasoner computes the closure (AIR-closure) for given facts, in N3, with respect to an AIR-program. An AIR-program is defined as a collection of AIR-rules, and the document containing it is referred to as AIR-document. The AIR language has separate ontologies for rules and justification. We introduce the AIR rules language (ontology) in section 2.1 and the AIR reasoning algorithm in section 2.2. Please refer to PML based AIR justification for justification ontology.

2.1. AIR Rules Language

Notation3 or N3[B2005] provides a human-readable syntax for RDF, which is more easily writable, readable and is more symmetrical than the RDF/XML syntax. For instance a collection, or RDF list, can be represented concisely by enumerating objects of the list enclosed in parantheses. i.e. ( object1 object2 ) is short for [ rdf:first object1; rdf:rest [ rdf:first object2; rdf:rest rdf:nil ] ], for example. N3 also extends expressiveness of RDF with abilities to use graphs as literal values, variables (universally or existentially quantified) over a graph, built-in functions and operators represented as RDF properties, and with abilities to define (horn) rules using the log:implies property, which is a relationship between two graphs. N3 graphs can be quoted within N3 graphs using "{" and "}". Existentially and universally quantified variables are indicated by @forSome and @forAll declarations, respectively.

AIR language is based on N3. The rules are described using following properties ⁶ : air:if, air:then, air:else, air:description, air:rule and air:assert, according to the abstract syntax ⁷. A template for declaring an AIR-program is shown in Figure 1. This template will be used in the later sections.

When we refer to s and o related by p1.p2 we mean that s p1 [ p2 o] holds.

The rules are of the form air:if <condition> air:then <then-action>s air:else <else-action>s. The condition is specified as graph pattern, similar to the Basic Graph Pattern (BGP) of SPARQL queries, which is pattern matched against N3 graphs. Whenever the condition matches the current state of the world, i.e. the facts known or inferred so far, all the then-actions are fired, otherwise all the else-actions are fired.

The rules are grouped under rule-sets. The rules nested directly under the rule-set are referred to as the top rules of the rule-set. The rule (child rule) nested under another rule (parent rule) via air:then.air:rule is said to be positively nested and that nested via air:else.air:rule is said to be negatively nested. A chain of rules is defined as a sequence of rules, such that every rule, barring the first in the chain, is nested under the preceding rule. t_action_is and e_action_is are the then-actions and else-actions, respectively. Together they are referred to as actions. The actions can be annotated with natural language description through air:description property.

Fig 1. AIR-program template

The existentially quantified variables may be declared within the condition graph patterns. The blank nodes (items in the graph not directly identified by a URI) in RDF graph have a form of existential variable. The universally quantified variables are declared outside of the rule. The scope of an existentially quantified variable is the graph pattern in which it is declared, where as that of a universally quantified variable is any rule chain, with the first rule as a top rule.

The graph pattern asserted in the action is declared using air:assert, and the nested rule is declared using the air:rule property. The asserted graph patterns cannot contain blank nodes or existentially quantified variables. When the nested rule is activated an instance of the rule with known variable bindings substituted is created. When a rule under an air:else property is activated, its condition can not contain unbounded universally quantified variables.

Since rules (can) have an id they can be reused. Therefore <ruleid_i> and <ruleid> in Figures 1A and 1C can be defined outside of this AIR document, in an AIR document that AIR reasoner can pull. The effect of reusing a rule is that all the rule chains starting with that rule are reused. Therefore AIR-program can be developed modularly.

While in Figure 1B the rule is typed as air:BeliefRule, it can be alternatively typed as air:HiddenRule or air:EllipsedRule, in order to modify the justifications in the output generated by the reasoner. This typing doesn't affect the logical semantics of the rules.

2.1.1. AIR Built-ins

N3Logic uses N3 syntax and extends RDF with a vocabulary of predicates. Most of the N3Logic built-ins ⁸ for cryptographic, math, string, list and time functions are supported in AIR. { :LEN math:notGreaterThan 6 } is an example graph pattern that uses the math:notGreaterThan built-in. Arguments to N-ary functions and built-ins is declared using the RDF list. N3 graph in web documents can be accessed using the built-in function log:semantics, and whether a graph is it's subgraph can be checked using the log:includes property. Whether a graph is not included in another graph can be checked using the log:notIncludes property. The SPARQL CONSTRUCT queries can be sent to the SPARQL end-points, described using the sparql:queryEndPoints property assertion, and sub-graph patterns can be searched for in the graph returned by the end point. The air:justifies property can be used to check if the AIR-closure of facts in some RDF documents w.r.t. the AIR-program in AIR-documents RDF-entail a graph pattern. When used in the condition of an if {condition} else action> type rule, air:justifies can be used to check if the graph pattern is not entailed. The RDF and AIR documents can be dynamically determined. i.e. RDF and AIR documents can be referred to by variables that acquire bindings at the time of reasoning, depending on the input facts.

Figure 2 lists example triple patterns that can be included in the rule conditions for contextualized reasoning. In the examples the IRIs with all upper-case local names can be assumed to be universally quantified variables, and the rest as constants.

Fig 2. Examples of AIR built-ins that can be used for contextualized reasoning.

The triple pattern in the example #1 checks if one of the N3 documents in the list includes the graph pattern {:S :P :O . }. It is not required that the variables (:S, :P, :O) be bound, in which case they acquire bindings based on the subgraphs they match with. The triple pattern in the example #2 is true if the rdfdoc₁ doesn't contain the triple { :s :p :o }. The graph pattern in the example #3 binds the variable :S (assuming :S is not bound already) to all bindings for variable ?S in the SPARQL query, which is dynamically created for every binding of the :CLASS variable, at the sparql-endpoint. The triple pattern in example #4 is true if the closure of the union of RDF triples in rdfdoc₁ and rdfdoc₂, and the union of AIR-programs in airdoc₁ and airdoc₂ entails the graph pattern {:s :p :o }. The graph pattern can have unbound variables as well. The union of AIR-programs is simply the resultant of combining AIR-programs in multiple documents into a single document.

2.1.2. Example AIR-program

Let us now look at a running example, shown in Figure 3. It defines conference policy, that a paper accepted in the conference should be published in a proceedings of the conference only if one of the author's has presented the paper in the conference (pol:CheckAtLeastOneAuthReg), or the first author has received an exemption from one of the co-chairs under special circumstances (pol:CheckFirstAuthExempted). The former condition is interpreted , for the purposes of example, as one of the co-authors on the paper has registered for the conference. It is assumed that the conference activities are logged using the same vocabulary as used in the rules.

Fig 3. Example AIR-program, describing the publication policy.

pol:CheckPubInProc is the only top rule, and pol:CheckNonCompliance, pol:CheckAtLeastOneAuthReg, and pol:CheckFirstAuthExempted are it's child rules. pol:CheckPubInProc checks for publications published in the proceedings of the conference, and for each publication activates instances of child rules (by substituting bindings for :PUBL). When pol:CheckNonCompliance is activated a description, obtained by substituting bindings for :PUBL in (:PUBL " published in this conference), is associated with it, which is maintained by the TMS. If the condition of pol:CheckAtLeastOneAuthReg or pol:CheckFirstAuthExempted rules is true then the publication is inferred to be compliant with the policy. The pol:CheckNonCompliance rule checks if rest of the rules have inferred that the publication is compliant with the policy. If not then it asserts that the publication is non-compliant with the policy.

2.2. AIR reasoning algorithm (Procedural Semantics)

AIR reasoner employs a RETE [F1982] based forward chaining approach to compute the AIR-closure. Figure 4 describes the main algorithm - COMP-CLOSURE (Figure 4B) - and related algorithms and the data structures (Figure 4A). The data structures and algorithms described here are abstractions of the actual implementation. For instance, FB (Fact Base) which is treated as set of facts is actually an efficiently indexed triple store, and RB (Rules Base) which is defined as set of active rules is compiled into the RETE framework in the actual implementation. The abstraction may give a false impression that steps #3 & #4 of ADD-TO-RULEBASE (Figure 4C) and step #2 of ADD-TO-FACTBASE (Figure 4D) are inefficient. For the purposes of analyzing the semantics of AIR this abstraction serves well. Readers are referred to [S2008] for implementation details.

Fig 4. The COMP-CLOSURE algorithm, and related data-structures and algorithms

The COMP-CLOSURE function computes the closure of input facts w.r.t the AIR-program. FB is initialized in step #1. In step #2 top rules are added to RB one by one, using the ADD-TO-RULEBASE function, which updates the RB, SRF (Successful Rules to Fire) and FRF (Failed Rules to Fire). SRF and FRF are queues of rules that need to be fired, because their conditions matched a subgraph in fact base or did not match at all, respectively. In step #3 elements from SRF and FRF queues are retrieived and rules are fired one by one, using the RULE-FIRE (Figure 4B) function. Preference is given to rules whose conditions are true. When a rule is added to the RB, and it's condition is not true, it is appended to the FRF (step #5 of ADD-TO-RULEBASE). However, before the rule gets fired some triples may have been added to the FB such that the rule's condition is matched. In such a scenario rule's success attribute would have been updated to true (step #2.2.1 of ADD-TO-FACTBASE). All such rules, that were added to the FRF but eventually succeeded are removed in step #3.2. Then the world is sort of closed, and all failed rules are fired. Please note that it is possible that a failed rule (say rule1) may fire such that triples asserted by it satisfy following failed rule (rule2), but rule2 would still fire once as a failed rule. Though this may not be very intuitive it elliminates unintended rule ordering dependencies. One cycle of step #3 is referred to as a stage, i.e. steps #3.1 to #3.3 (#3.3.1 and #3.3.2 included) constitute one stage of the algorithm. Further, step #3.1 is referred to as a positive stage, denoted as stage⁺ and steps #3.2 & #3.3 constitute a negative stage, denoted as stage^-. We will be using stage_i, stage_i⁺ and stage_i^- to refer to the i-th stage, stage⁺ and stage^-, respectively. The COMP-CLOSURE algorithm computes the next stage until a fix-point is reached, which in our case is reached once both the SRF and FRF are both empty.

When a rule is fired, it can activate zero or more instances of child rule and assert zero or more graphs. Before rule activation or assertion, the rules (along with their descendant rules) or graphs, respectively, and the description, if there is one, are instantiated with the bindings passed in the call to the RULE-FIRE function. The rules are added to the RB and the graph triples are added to the FB. The justification for this action is added, and maintained thereafter, by the TMS.

In the ADD-TO-RULEBASE function, the rule condition is matched (pattern matching) against the triples in the FB. The AIR reasoner, like the CWM [BCKSH2008] reasoner treats specially those properties it knows as calculable functions which occur in the condition. If the rule condition is satisfied it's success attribute is set and a tuple of rule and variable-bindings is added to the SRF queue, for every bindings for which the condition is true. If the rule condition is not true, the rule is added to the FRF.

The asserted triples are added to the FB in the ADD-TO-FACTBASE function. As a result of addition of inferred facts some of the rule's conditions may become true. All such rules are appended to SRF with the bindings, and their success attribute is set to true.

Fig 5. Arbitrary rule nesting

In order to exemplify rule nesting we consider an arbitrary nesting shown in Figure 5. Initially, i.e. before entering the stage 1, only Rule_A and Rule_B are in the rule-base. Then, if Rule_B condition is satisfied Rule_D would be active in stage 1. However, if in stage 1 Rule_B doesn't succeed, then Rule_C will be added to the rule-base after the world is closed for stage 1, and will be active from stage 2. Now in stage 2 if Rule_C succeeds then Rule_E will become active in stage 2. Otherwise Rule_F will be active from stage 3. Note that if Rule_B succeeds in later stages, say stage 3, then Rule_D will also be active (in addition to Rule_C) from stage 3 onwards.

Consider an example log in Figure 6 and the example AIR-program from Figure 3. The AIR-closure contains one additional triple colog:pub1 air:compliant-with pol:PubInProcPolicy. In order to compute the closure, FB is initialized by triples in the example log, and pol:CheckPubInProc will be added to the RB. When the rule is added it's condition has a match, and it is added to the SRF with pol:PUBL bound to colog:pub1. When it fires the three child rules are added to the RB . Only, pol:CheckAtLeastOneAuthReg succeeds, and other rules are added to the FRF. The pol:CheckAtLeastOneAuthReg is added to the SRF with :AUTH bound to colog:auth1. It fires next, and asserts the triple { colog:publ1 air:compliant-with pol:PubInProcPolicy }. When that triple is added, it satisfies the pol:CheckNonCompliance's condition and the rule's success attribute is set to true. SRF is now empty and the pol:CheckNonCompliance is next removed from FRF. The sole rule in FRF, pol:CheckFirstAuthExempted doesn't have an air:else property. The fixpoint is reached at the end of first stage itself. The output generated by the AIR reasoner is shown in Figure 7. The justification shown here uses the tms ontology (rather than the new PML based ontology).

colog:pub1 air:compliant-with pol:PubInProcPolicy .
pol:CheckPubInProc tms:justification tms:premise .
{ colog:pub1 air:compliant-with pol:PubInProcPolicy . 
} tms:description  ( "One of the Authors" colog:auth1 "registered for the conference" );
         tms:justification  [
             tms:antecedent-expr  [
                 a tms:And-justification;
                 tms:sub-expr  [
                     air:instanceOf pol:CheckAtLeastOneAuthReg;
                     tms:justification  [
                         tms:antecedent-expr  [
                             a tms:And-justification;
                             tms:sub-expr pol:CheckPubInProc,
                                    {<http://www.conf.org> conf:hasProceedings colog:proc .
                                     colog:proc conf:hasPaper colog:pub1 . } ];
                         tms:rule-name pol:CheckPubInProc ] ],
                        {<http://www.conf.org> conf:registeredBy colog:auth1 .
                         colog:pub1 conf:hasAuthor colog:auth1 . } ];
             tms:rule-name pol:CheckAtLeastOneAuthReg ] .
    { <http://www.conf.org> conf:hasProceedings colog:proc;
             conf:registeredBy colog:auth1 .
        colog:proc conf:hasPaper colog:pub1 .
        colog:pub1 conf:hasAuthor colog:auth1 .
        } tms:justification tms:premise .

3. Logic Programs

We will review some standard terminologies of logic programs [R1994]. A term is either a variable or a constant symbol. We assume that finite universe U of constant symbols is given. p(t₁, ..., t_n) is an atom, where t₁, ..., t_n are terms and p is an N-ary predicate symbol. A literal is either an atom or a negated atom, negated using the negation as failure (NAF) operator not. A normal logic program (NLP) is a finite set of rules of the form : A ← L₁, ..., L_n, where A is an atom, and L_is are literals. A and L₁, ..., L_n are called the head and the body of the rule. We prefix all variable names by '?'. Rules with negative literals in the body are referred to as negative rules, and those with no negative literals in the body are referred as positive rules. By instantiated atoms and rules we mean that values from U are substituted for all variables in the atoms and rules, respectively. Ground(R) refers to the set of all possible instances of R (with respect to U). The notion of instantiation we use for LPs is different from the one used for AIR-programs. Not all variables in an AIR-rule are substituted when an AIR-rule is instantiated.

In rest of the paper when we refer to logic program(LP) we will mean NLP, unless explicitly stated otherwise. An LP is range restricted (alternatively safe) if every variable occuring in the head of a rule or in a negative literal in the body also occurs in a positive litereal in the body. A positive logic program (PLP) is a NLP that has no rule with negative literals.

An LP is stratified if there is an assignment of ordinal levels to predicates such that whenever a predicate appears negatively in the body of a rule, the predicate in the head of that rule is of strictly higher level, and whenever a predicate appears positively in the body of a rule, the predicate in the head has at least that level. A stratification of normal program P is a partition of P given by : P = P₁ ∪ ... ∪ P_n, such that each rule A ← L₁, ..., L_m in P is in P_i iff ordinal level assigned to A is i. An LP is hierarchical if there is an assignment of ordinal levels to predicates such that whenever a predicate appears in the body (negatively or positively), the predicate in the head of that rule is of strictly higher level. A hierarchical LP is stratified. An LP is locally stratified if there is an assignment of ordinal levels to ground atoms such that whenever a ground atom appears negatively in the body of an instantiated rule, the head of that rule is of strictly higher level, and whenever a ground atom appears positively in the body of an instantiated rule, the atom in the body has at least that level. A stratified LP is locally stratified. A local stratification of normal program P is a partition of Ground(P) given by: Ground(P) = P₁ ∪ ... ∪ P_n, such that each clause A ← L₁, ..., L_m in Ground(P) is in P_i iff ordinal level assigned to A is i.

T_P is the one step deduction operator associated with LP P, and is defined as :
T_P(I) = { A₀ ∈ BP | P contains a rule whose instantiation is A₀ ← A₁, …, A_n such that I |= A₁, …, A_n}
where I is the given set of atoms that are true. The powers of T_P are defined as :

T_P^↑0(I) = I

T_P^↑n+1(I) = T_P(T_P^↑n(I)) ∪ T_P^↑n(I)

T_P^↑ω(I) = ∪_n=0^∞ T_P^↑n(I)

The semantics of stratified and locally stratified LP P is defined in terms of its perfect model, also called the standard model [P1988]. We will refer to the perfect model of P by PM(P). P entails ground atom A iff A belongs to PM(P). Let P₁ ∪ ... ∪ P_n be the stratification (local stratification) of P (Ground(P)). Then PM(P) = M_n, which is defined by :

M₁ = T_P1^↑ω(∅),

M₂ = T_P2^↑ω(M₁),

...

M_n = T_Pn^↑ω(M_n-1)

Next we will introduce a new class of stratified LP - Positively Stratified Negatively Hierarchical Logic Program (PSNHLP) - which is relaxed compared to hierarchical LP but stricter than stratified LP. The authors are not aware of any class of LPs with same characterization as that of PSNHLP.

3.1. Positively Stratified Negatively Hierarchical Logic Programs

An LP P is PSNHLP if there is an assignement of ordinal levels to predicates such that whenever a predicate appears in the body (negatively or positively) of a negative rule, the predicate in the head of that rule is of strictly higher level, and whenever a predicate appears in the body of a positive rule, the predicate in the head has at least that level. Similarly LP P is locally PSNHLP if such an assignment of ordinal levels is possible over ground atoms for Ground(P). Let P = P₁ ∪ ... ∪ P_n be the stratification of (locally) PSNHLP P. Consider a partition of P_i, P_i = P_i⁺ ∪ P_i^- such that a rule from P_i is in P_i⁺ if it is positive and in P_i^- otherwise. Note that all predicates in the body of any rule in P_i^- have ordinal level strictly smaller than i. The PSNH-stratification of P is defined as P = P₁⁺ ∪ P₁^- ∪ ... P_n⁺ ∪ P_n^-.

We will now show that the perfect model of P can be defined as :

M₁ = T_P1^↑ω(∅),

M2' = TP2-↑1(M1),

M2 = TP2+↑ω(M2'),

...

Mn' = TPn-↑1(Mn-1),

Mn = TPn+↑ω(Mn')

where Mn = PM(P) and M1, M2, ..., Mn are defined as : M1 = TP1↑ω(∅), and for i > 1 Mi = TPi↑ω(Mi-1). i.e. M1 = TP1+↑ω(∅), and for i > 1 Mi = TPi+↑ω(TPi-↑1(Mi-1)). It is easy to see that the first part holds, because P1 = P1+ (P1- = ∅). The latter follows from the claim below.

Claim 1 : TPi↑ω(Mi-1) = TPi+↑ω(TPi-↑1(Mi-1))
Proof : Since Mi-1 is the union of closures of Pj, j < i, Mi-1 contains all the ground facts in PM(P) for predicates with ordinal levels less than i. Also, all the predicates in the body of the rules in Pi- are of ordinal levels less than i. Therefore, TPi-↑2(Mi-1) = TPi-↑1(Mi-1). For the same reasons, it is safe to separate positive rules in Pi from the negative rules in Pi, because predicates (symbols) in the body of Pi- are disjoint from those in the head of Pi+. i.e. the deductions from rules in Pi+ can not trigger deductions from the rules in Pi-. Q.E.D.

Claim 2: PSNHLP is PTime-complete in data-complexity and ExpTime-complete in program-complexity.
Proof : Stratified LP (or Stratified Datalog with Negation) P is PTime-complete in data-complexity and ExpTime-complete in program-complexity [DEGV2001, implicit in ABW1988]. This comes from the fact that in the worst case, computation of the fix-point for a stratum may require rc^a applications of T_P, where P is the stratum, r = #relations in P, c = #unique constants defined (used) in P, and a = maximum of arities of relations in P [ABW1988]. The same holds for a PSNHLP. Q.E.D.

4. Declarative Semantics of AIR

The declarative semantics of an AIR-program can be defined in terms of a semantically equivalent PSNHLP. We will first define the translation Τ from AIR-program (Α) to an LP (Ρ), and then show that Ρ is a PSNHLP and the AIR-closure of Α and input facts (ƒ) (mapped as ground facts) is same as the PM(Ρ).

Α can be translated to an LP with rules constructed using the following predicates : t, t_s, active_rule and cond :

• t is a ternary predicate that represents a N3 triple. t(s, p, o) represents a N3 triple {s p o}
• t_s(s, p, o, c, n) represents a N3 triple {s p o}, true within the context c, in the n-th stage of reasoning (COMP-CLOSURE algorithm).
• active_rule(ruleid, ?v₁, ..., ?v_m, c, n) means that rule ruleid is active at stage n, in the context c. The exact instance of the rule is determined by the partial bindings of ?v_is. ?v_is are the universally quantified variables used in the chain of rules to which ruleid belongs. For example, the rule pol:CheckAuth has two variables ?PUBL and ?AUTH. The predicate active_rule(pol:CheckAuth, colog:pub1, ?AUTH, c, 1) implies that an instance of the rule pol:CheckAuth is active at the 1st stage with ?PUBL bound to colog:pub1 in the context c. Here ?AUTH is unbound, i.e. the predicate is true for all possible bindings of ?AUTH from the universe of constants U.
• cond(ruleid, ?cv₁, ..., ?cv_m, c, n) means that the condition of the rule ruleid is true at the n-th stage, in the context c for some variable bindings. The ?cv_is are universally quantified variables occurring in the rule's condition. The VAR_IN_COND(ruleid) function returns all these variables, for a given rule. For example, cond(pol:CheckAuth, colog:pub1, colog:auth1, c, 1) implies that the condition for the rule is true in stage 1 when ?PUBL is bound to colog:pub1 and ?AUTH is bound to colog:auth1.
• succ (successor) and ≤ predicates are used with their usual meanings.

The context may be defined by a collection of N3 and/or AIR-program sources, and is identified with an ID.

Fig 8. TRANS(ele, n) function definition.

Fig 9. Additional semantics of predicates used in Ρ

Τ(Α) is the union of rules from TRANS(setid) and TRANS(ruleid), respectively for every rule sets and production rules in Α.
The TRANS(ele, ?n) for the elements in built-ins free AIR-program is defined in Fig 8. The translation steps (TSs) are defined based on the template descriptions of eles in Fig 1. ?n is an optional argument.
The MAP(val) maps val to ?val or val depending on whether val is declared to be a variable or not, respectively. UB is the finite upper bound on the number of stages encountered by the COMP_CLOSURE algorithm before the fix point is reached, for given rule and fact bases. Computation of UB is described in Appendix I.
Additional rules on predicates that hold irrespective of the Α are shown in Fig 9. Rules once activated remain so ever after (TS-9). Similarly, triples inferred to be true are true for all the future stages (TS-10). Finally, the closure contains all the triples that were inferred at any of the stages (TS-10).

For example, the TRANS(pol:ChkNonCompl) will return the following rules (For translation of other rules please see Appendix V):

• t_s(?PUBL, air:non-compliant-with, pol:PubInProcPolicy, ?c, ?m) ← active_rule(pol:CheckNonCompliance, ?PUBL, ?AUTH, ?REASON, ?c, ?n), not(cond(pol:CheckNonCompliance, ?PUBL, ?c, ?n)), succ(?n, ?m), ?n≤ UB .
  
• cond(pol:CheckNonCompliance, ?PUBL, ?c, ?n) ← t_s(?PUBL, air:compliant_with, pol:PubInProcPolicy, ?c, ?n), ?n≤ UB .

?n ≤ UB ensures that the closure for Ρ is finite. However UB need not be computed for every Α, as the rules can be rewritten such that TS-9 and TS-10 become redundant, as shown in Appendix III. Further, we assume that none of the properties in the condition are built-ins. In Appendix IV the TRANS function is extended to handle the air:justifies (and log:includes and log:notIncludes as well) built-in. Many other built-ins, math built-ins for example, can be defined through LP rules. Remaining can be handled through external predicates, crypto built-ins for example. The detailed analysis of LP representation for all the AIR built-ins is a future work.

Claim 3 : Ρ is locally PSNHLP.
Proof : Let the assignment of ordinal levels to ground atoms for all predicates except t be equal to the value of its last term. For example t_s(s, p, o, cntxt, n) is assigned level n. Further, let predicate t be assigned an ordinal level equals to UB. This assignment gives a local PSNH-stratification of Ρ. Q.E.D.

We can replace the atom t_s(s, p, o, c, n) by t_sn(s, p, o, c). We can do so for other atoms with t_s, active_rule and cond predicate symbols, by introducing t_sn, active_rule_n and cond_n predicate symbols, for all n ≤ UB. Although the TS-9, TS-10 and TS-11 rules will expand O(UB²) times and the rest O(UB) times, changes to TSs in Figures 8 and 9 are straightforward. Then the resulting Ρ, say Ρ`, is a PSNHLP as against being just locally PSNHLP.

Let |Α| be the size of the AIR program Α, nUV(Α) gives the number of universal variables in Α and nChains(Α) gives the maximum number of unique chains that start with one of the top rules in Α. The size of Α, |Α|, is the number of distinct BeliefRules, EllipsedRules and HiddenRules defined or used in Α. Furthermore, let |ƒ| be the size of input data ƒ, and |Ρ| be the size of the translated LP, Ρ, which is defined by number of rules in Ρ

Claim 4: |Ρ| = O(|Α| + |ƒ|), i.e. size of translated LP is linear in size of AIR program and in size of input data. But, |Ρ| = O(exp(|Α|) + |ƒ|) if rules in translated LP are forced to be safe. i.e. the size of translated LP such that the LP is safe may be exponential in size of AIR program.
Proof: According to the translation scheme, translation of an AIR rule to LP rule is independent of other rules in every sense but one. The variables in active_rule atom is determined by the variables occurring in the rule chain. In contrast the variables in the cond predicate is determined only by looking at the variables in the if-pattern of the rule. Given a set of rules, they may form exponential number of rule chains. Therefore a rule from the set may appear in exponential number of chains, requiring exponential number of translated LP rules for each chain. i.e. in the worst case |Ρ| = O(|Α| * 2^nUV(Α)), where 2^nUV(Α) is the upper-bound on combination of variables used by different rule chains.
However, we can reduce the complexity by first observing that the translated LP rules are unsafe. For example rules generated by TS-2. Then we can allow every active_rule atoms to have all the universal variables used in the AIR program Α, instead of restricting them to the set of variables occurring in the rule chains to which a particular rule belongs. With this change the translation is linear in size.
In order to restrict translation to safe rules, where rules generated by TS-2 may be disallowed for example, the rule chain structure can not be overlooked. The rules cannot be translated independently of other rules. Instead of one active_rule predicate, a new predicate must be used per rule, per chain of the AIR program. nChains(Α) may be exponential in |Α|. Therefore the translation may be exponential in size of AIR program in the worst case. Q.E.D.

Let Ground(Ρ) = P₁⁺ ∪ P₁^- ∪ ... ∪ P_UB⁺ ∪ P_UB^- be the partitioning of Ground(Ρ). We can show semantic equivalence, denoted by ∼, between the steps for computation of PM(Ρ) and the AIR-closure of Α and ƒ. T ∼ s is used to denote the direct correspondence between extensions of predicates active_rule and t_s, inferred after the application of T operator during the computation of PM(Ρ), and the rules activated and triples asserted after completion of stage s of COMP-CLOSURE execution.

Claim 5 : TP1+↑ω ~ stage1+. For i > 1, TPi-↑1 ~ stagei-1- and TPi+↑ω ~ stagei+. i.e.:

1. active_rule ground fact belongs to TPi+↑ω(Mi') (Mi) iff corresponding rule instance is in RB after stagei+.
2. t_ns ground fact is in M_i iff corresponding triple is in FB after stage_i⁺.
3. active_rule ground fact belongs to TPi-↑1(Mi-1) (Mi') iff corresponding rule instance is in RB after stagei-1-.
4. t_ns ground fact is in M_i' iff corresponding triple is in FB after stage_i-1^-.
   

Proof : We'll prove the claim through induction. The base case is that TP1+↑ω ~ stage1+, and TP2-↑1 ~ stage1-.
The ground facts in Ρ come from TS-1 and TS-8. The ground facts from TS-8 correspond to triples given in ƒ. RB is initialized by top rules. Correspondingly active_rule ground facts will be inferred in TP1+↑1(∅), for all combinations of bindings for u_varis and ?cntxt = cntxtid, because of the rules from TS-2. Next, whenever condition of a rule in RB is matched in stage1+, the corresponding cond predicate will be inferred in TP1+↑k(∅), for some k. Further, since that rule is in RB, corresponding active_rule predicate would also have been inferred. As a result, while then-actions are executed in stage1+ and RB and FB are updated, corresponding active_rule and tns will also be inferred in some TP1+↑k(∅). When a rule instance is added to RB, multiple active_rule ground facts are inferred, such that variables that are bound by the matched graph in corresponding rule instance, are the same for all those facts. From this close correspondence, it is evident that active_rule ground fact belongs to TP1+↑ω(∅) (M1) iff corresponding rule instance is in RB after stage1+. Also, tns ground fact is in M1 iff corresponding triple is in FB after stage1+.
None of the failed rules in RB fire in stage1+. They fire in stage1-. Since the condition of failed rule has no match in FB, the corresponding cond predicate is also not in M1. Again since the rule is in RB, corresponding active_rule ground fact is in M1. Therefore, when else-actions fire once for each rule in stage1- corresponding active_rule and tns are also inferred in TP2-↑1(M1). Therefore, active_rule ground fact belongs to TP2-↑1(M1) (M2') iff corresponding rule instance is in RB after stage1-. Also, tns ground fact is in M2' iff corresponding triple is in FB after stage1-.
The above arguments similarly hold for higher i's. Therefore for all i's, active_rule ground fact belongs to TPi+↑ω(Mi') (Mi) iff corresponding rule instance is in RB after stagei+. Also, tns ground fact is in Mi iff corresponding triple is in FB after stagei+. Similarly for all i's, active_rule ground fact belongs to TPi-↑1(Mi-1) (Mi') iff corresponding rule instance is in RB after stagei-1-. Also, tns ground fact is in Mi' iff corresponding triple is in FB after stagei-1-. Q.E.D.

Let Ν be the N3 graph obtained by taking N3 representation of extensions of predicate t in PM(Ρ).

Claim 6 : The AIR-closure of Α and ƒ is same as Ν.
Proof : Let Ν_i be the N3 representation of extensions of predicate t_s in M_i, i.e. Ν_i = {(s p o) | t_s(s, p, o, c, i) ∈ M_i}. Note that M_i is the model obtained after computing fixed-point for P_i, which equals P_i^- ∪ P_i⁺.
From claim 5 it follows that Ν_i ∩ Ν is same as the triples asserted by the end of stage_i⁺, for all i > 1. Since the fix-point is achieved before the UB-th stage, it follows that Ν_UB ∩ Ν is same as the triples in the AIR-closure of Α and ƒ. However, Ν_UB contains, exactly, the extensions of predicate t_s in M_UB and by TS-11 rule the extensions of predicate t in M_UB, and PM(Ρ) = M_UB. Q.E.D.

From the relation between AIR and stratified programs, we can immediately obtain the complexity result for AIR. Note that data complexity is the complexity of computing the model when the rules-base (logic program) is fixed and the fact-base (input database) is an input. The program complexity is the complexity of computing the model when the fact-base is fixed but the rules-base is an input.

Claim 7 : AIR-closure computation is PTime-complete in data-complexity and ExpTime-complete in program-complexity.
Proof. We have shown that any AIR program can be translated to equivalent PSNHLP Ρ', with upper bound on number of stratums, UB, polynomial in size of input data. We have also shown the direct correspondence between the steps for computing the perfect model of Ρ (similarly, Ρ'), and those for AIR-closure of Α and ƒ. Therefore, the complexities for PSNHLP are an upper bound for AIR-closure computation. However, since all PSNHLPs can be encoded in AIR (Claim 9) complexities for PSNHLP are also a lower bound for AIR-closure computation. Thus AIR-closure computation complexities are same as that for PSNHLP (Claim 2). Q.E.D.

5. AIR and Logic Programming

Logic programming is a well-known declarative method of knowledge representation and programming. Like LPs we define rules in AIR programs. However, AIR rules have different semantics from the LP-rules, and they can be nested under one another. Different nesting of same rules yields (semantically) different AIR programs. In this section we investigate logic programming through AIR.

Any safe rule A ← A₁,...,A_n, not(B₁), ..., not(B_m), where A_is and B_is are atoms can be written in AIR, by rewriting the rule as :

A ← A₁, ..., A_n, not(Aux) .

Aux ← B₁ .

...

Aux ← B_m .

where Aux is a new predicate and it's arguments are all the variables that appear in the rule body. Then the original rule can be rewritten in AIR as shown in Fig 10.

Fig 10. Rewriting a LP rule in AIR.

There are two popular approaches for representing N-ary relations on semantic web⁹ - 1. represent relation as an OWL class, 2. use lists for arguments of the relation. When new inferences are drawn by a rule a new instance of some OWL class or a new unique id for RDF list must be used. Assertions with blank nodes are not recommended in AIR, to avoid definitions of logic programmes with unbounded closures. Creating URIs programmatically for the inferred instance or RDF list, respectively, is not an option. However, N-ary predicate p(t₁, ..., t_n) can be represented in N3 as (t₁, ..., t_n) p true. The function PRED_IN_N3(pred) returns this N3 representation of predicate pred.

An LP is a collection of rules and ground facts. The semantics of LP is not only dependent on the semantics of individual rules but also on how they interact. We will say that something (usually some LP) can be loss-lessly rewritten (or translated) in AIR if that something can be written in AIR with unchanged semantics. Next we will show that PLP, PSNHLP and SPARQL can be losslessly rewritten in AIR, by taking advantage of nesting of rules and the associated semantics.

Claim 8 : PLPs can be loss-lessly rewritten in AIR.
Proof : Since there is no non-monotonicity, the order in which rules are applied does not matter. Therefore it is sufficient to rewrite each rule of the LP in AIR and make them child of a single rule-set. Q.E.D.

Corollary 1 : OWL 2 RL ¹⁰ inference rules can be encoded in AIR, and used concurrently with other rules.

Claim 9 : PSNHLP P can be loss-lessly rewritten in AIR.
Proof : Let P = P₁⁺ ∪ P₁^- ∪ ... ∪ P_n⁺ ∪ P_n^- be the PSNH-stratification of the PSNHLP P, and each P_i^- has n_i^- rules and P_i⁺ has n_i⁺ rules. Let the k-th rule in stratums P_i⁺ and P_i^- are encoded in AIR with rule ids :r_ik⁺ and :r_ik^- respectively. Then the nesting of rules shown in Fig 11 would yield a loss-less translation of P.

The rules in P_i⁺ and P_i+1^- are activated after stage_i-1. Therefore, at the end of stage_i⁺ all the ground facts of predicates with ordinal level less than i + 1 in PM(P) have been inferred. Q.E.D.

Corollary 2 : Non-recursive datalogs can be losslessly rewritten in AIR.
Proof : Non-recursive datalog is a PSNHLP.

While it may be difficult to appreciate the need for nesting shown above, it is notable that such a nesting can be created programmatically. More importantly the justification generated by the AIR reasoner for computing closure w.r.t this AIR-program will reflect exactly the order of execution taken by an LP engine for finding the perfect model of P.

Claim 10 : Not all stratified LPs can be losslessly rewritten into AIR.
Proof: We prove by a contra-example. The following LP cannot be translated in AIR for arbitrary facts:

P(x, z) ← P(x, y), P(y, z), not(Q(x, z)) .

R(x, y) ← S(x, y), not(P(x, y)) .

Q.E.D.

We propose an extension to AIR syntax to allow nesting of rule-sets using the property air:hasHigherPriority. :rs₁ air:hasHigherPriority :rs₂ will imply that rules in :rs₂ are activated after a fixed point is reached for the rules in :rs₁. i.e. the COMP-CLOSURE proceduce is first run for the rules in :rs₁ and when that terminates (i.e. fixpoint is achieved), it will be run again after addition of rules in :rs₂ to the RB. This feature is similar to salience in Jess, where rules are assigned priorities using integer values. The rules are fired in order of their priorities.

Claim 11 : Stratified LPs can be losslessly rewritten into AIR with feature for nesting of the rule-sets.
Proof : Let P = P₁ ∪ ... ∪ P_n be the stratification of stratified LP P. Let the k-th rule in stratum P_i is encoded in AIR with id :r_ik. Then the following nesting of rules would yield a loss-less translation of P :

when i < n :

when i = n :

Claim 12 : SPARQL SELECT and CONSTRUCT queries can be losslessly rewritten in AIR, and therefore they can be executed by the AIR reasoner.
Proof : It has been shown that SPARQL queries (without the query modifies like ORDER BY, LIMIT etc.) can be translated to non-recursive Datalog (Π_Q) with NAF [P2007], under the answer set semantics [GL1991]. The answer set semantics coincides with stable model semantics and perfect model semantics for stratified LPs. From the corollary 2 it follows that Π_Q can be losslessly rewritten in AIR.
Π_Q is defined in terms of τ, which is recursively defined as in Figure 12. The solutions of Q are represented by the extension of predicate answer₁ in the answer set M of Π_Q. The SPARQL CONSTRUCT queries are handled by adding the rule : triple(s, p, o, C) :- answer₁(vars(P^C), default) to Π_Q, for each triple {s p o} in the construct pattern P^C. With the addition of these rules, the resulting datalog Π_Q is not non-recursive any-more. Since there is no provision in SPARQL for matching BGPs in the query against the constructed triples [SP2008], the head of these rules can be changed to triple_C(s, p, o, C), where triple_C is a new predicate symbol. Now, the resulting Π_Q is non-recursive again, and therefore can be loss-lessly translated. Q.E.D.

Fig 12. Translation Π_Q from SPARQL queries semantics to Datalog [P2007]

5.1. AIR and SPARQL

We've seen that SPARQL queries can be encoded in AIR. Although Π_Q can be translated to AIR based on the approach discussed earlier, since SPARQL and AIR are both RDF based languages and both suport contextualized querying translation of Π_Q to AIR deserves closer attention.

The answer_i, answer_i' and triple_C are N-ary relations (variable n) and their N3 representation can be obtained by the application of PRED_TO_N3 function. The triple(s, p, o, D) can be represented as RDF triple {s p o} when D = 'default', otherwise - i.e. for named graphs - using the log:includes property as D log:includes { s p o }. Certain variables are assigned null values, for example in (5). Although the assignment of null value is done in the head of the rules, the same can be done in the body through <X> str:matches "null", where the variable X is set to null.

The portion of Π_Q^C generated from (8) can be written concisely. τ(V, P, g, i) for g in (V ∪ I) can be written as following : { @forAll :GRAPH . :r a air:BeliefRule; air:if { :GRAPH in (<ng₁> ... <ng_n>) }; air:then :r2 .}, where ng_i are named graphs declared using the FROM NAMED <ng_i> clause and :r2 is the AIR translation of answer_i(V, D) :- answer_i(V, :GRAPH). Note that g has been replaced by :GRAPH and other checks in the body - isIRI(g), not g = default- have been removed as they are now redundant.

There is a similar work in translating SPARQL to N3 [S2009]. However, there the objective is to annotate the SPARQL queries for policy checking purposes. Therefore, BGP₁ OPTIONAL BGP₂ is treated same as BGP₁ INTERSECTION BGP₂, for example.

Not all SPARQL filter expressions can be expressed in AIR, currently. For example there is no AIR built-in for regular expression based string matching although there are built-ins such as string:startsWith, string:endsWith and string:contains. Similar to [P2007], !BOUND(X) condition can be checked using following triple {X string:matches "null"} in a rule's condition.

All variables in the SPARQL query must be assigned an IRI and included in some @forAll declaration. For all graphs whose triples are part of the default graph (declared using FROM <uri> clause), we add a rule, say default-graph-rule (dgr), to the ruleset : @forAll :S, :P, :O. :dgr a air:BeliefRule; air:if { <uri> log:includes {:S :P :O . } }; air:then [ air:assert { :S :P :O . } ] .

Networked Graphs (NGs) [SS2008] is a declarative mechanism for defining RDF graphs both, by extensionally listing RDF triples and by intensionally using views on other graphs. NGs can have circular dependencies. The relationships between graphs are described declaratively using SPARQL queries and an extension of the SPARQL semantics. SPARQL queries are defined over networked graphs, instead of named graphs, for example.

We will argue without going in details that a restricted form of NGs - NGs without circular dependencies and PSNH negation - can be implemented in AIR. We have seen that SPARQL queries can be loss-lessly rewritten in AIR. As the constructed graph is included in the default networked graph triple_C(s, p, o) can be represented as RDF triple {s p o}. Since SPARQL queries are defined over intensionally defined graphs, whenever SPARQL translation was mapped to <uri> log:includes (s p o), where uri is the IRI of a NG, must now be mapped to (() (<uri>)) log:justifies (s p o), assuming that the extensional triples of the NG have been included in it. One way to include extensional triples is to make the RDF graph which contain those triples object of the assertion property (obj) in the following rule : :r a air:BeliefRule; air:if {}; air:then [ air:assert obj ] .

6. AIR and Other Rule Systems

There are many rule languages and rule systems, some advanced and others at prototypical levels. Senlin Liang et. al. give a nice overview of popular, and often advanced, rule systems [Liang2009]. We consider AIR, N3Logic, NGs, SCLP [G2001], SILK [GDK2009], SWRL [S2004], in addition to DLV ¹⁰, DROOLS ¹², IRIS ¹³, Jena ¹⁴, Jess ¹⁵, Ontobroker ¹⁶, SwiftOWLIM ¹⁷ and XSB ¹⁸. Some of these are rule languages - N3Logic, NG, SCLP and SWRL - while some are rule engines - DLV, IRIS, Jena, Ontobroker, SwiftOWLIM and XSB. Rest are rule systems with their rule language and rule-engine. It may be argued that Jess and Drools are rule engines for the same production rule language, however, without clear semantics it is hard to show so.

Networked Graphs (NGs) is SPARQL based rule language where rules are defined using the CONSTRUCT SPARQL query. Situated Courteous LP (SCLP) extends LP with procedural attachments and priority conflict handling (rule ordering). Semantic Inferencing on Large Knowledge (SILK)'s knowledge representation is hyper logic programs that includes prioritized defaults, conflict handling, higher order features, full classical logic, and actions and events. DLV is a bottom up rules system based on answer-set programming [GL2002]. DROOLS and Jess are Java based production rule systems, with bottom-up evaluation of rules, that can call arbitrary Java methods. Jess has certain top down inference capabilities and the Java objects can be accessed by the rules. IRIS and Ontobroker are bottom up rule inference engines based on the well-founded (WF) semantics. Jena is a Java-based framework for building Semantic Web applications. Jena rules engine and SwiftOWLIM are rule engines over RDF data. In Jena, rule can be declared as forward or backward rule for forwards vs backward chain reasoning. SwiftOWLIM does bottom-up evaluation. XSB is an optimized Prolog engine.

AIR is a function free language that supports non-monotonic negation, with the semantics described in the earlier sections. In comparison, NGs, IRIS and Ontobroker support the well-founded (WF) negation, SCLP and XSB support negation-as-failure, and DLV supports negation defined in terms of the stable model semantics. N3Logic supports monotonic negation through log:notIncludes. Drools and Jess support non-logical negation. However subsets of Jess and SCLP are inter-representable [GGF2002]. SILK supports WF non-monotonic negation as well as classical negation. Others do not support negation. IRIS, Ontoprise and XSB support function symbols.

Rule Interchage Format (RIF) [K2008] (and Rule Markup Language (RuleML)) is an effort towards developing standards to facilitate interoperability of rules in these disparate rule based systems over the semantic web. RIF has two major dialects - Framework for Logic Dialects (FLD) and Production Rule Dialect (PRD). The RIF PRD action language can be used to add, delete and modify fact base, and to call externally defined actions. While actions in AIR can not modify or remove facts, they can add new production rules. The latter is special class of actions not explicitly considered in RIF PRD. However, we have argued earlier that AIR negation is logical, and has declarative semantics. Hence, we can compare AIR with RIF FLD. RIF-FLD is an extensible framework for rule-based languages, and includes the Basic Logic Dialect (BLD), which corresponds to the definite Horn rules with equality and a standard first order logic semantics. AIR is neither more nor less expressive than RIF BLD. Unlike BLD, function symbols are not supported in AIR (BLD also allows disjunctions in the body, which is more of a syntactic sugar. Moreover, AIR also allows some forms of disjunctions through the list built-in list:in). Where as AIR supports nonmonotonic negation. However, which logic based on FLD can express the semantics of AIR negation is a subject of investigation. Both AIR and BLD have extensive set of built-ins.

SWRL is a function free rule language limited to binary and unary predicates, and all it's features, barring different-from, are covered by RIF-BLD. Therefore, AIR is at-least as expressive as SWRL. (The axioms corresponding to different-from can be expressed using AIR.)

Nesting of rules is unique to AIR amongst the systems mentioned above. The OPS/YES [SDLT1986] extends the OPS5 [F1981] production rule system with many features including the that allows matching in the actions. This is referred to as incremental rule addition and AIR has a similar notion of rule nesting. Jena also supports nesting of rules, (?p rdfs:subPropertyOf ?q), notEqual(?p,?q) → [ (?a ?q ?b) ← (?a ?p ?b) ], for example. However, Jena doesn't allow nesting when condition is not satisfied.

The trace of reasoning steps performed by the reasoner is the basic form of justification available from reasoners. For instance Jena inference engine returns the trace for deductions, referred by derivations. It can be argued that details relevant to the proof of some conclusion often has to be mined from the trace. Also, a natural langauge description is helpful in understanding the proofs. Amongst the above systems, only AIR and Ontobroker provide such justifications. The Ontonova system [AMOSW2003] provides natural language explanation of proof trees for conclusions by the Ontobroker, through meta-inferencing. The meta-inferencing rules are defined for different rule instantiations and applied over the logs generated by Ontobroker during the inferencing process. The logs contain intantiated rules that were successfully applied and led to the derivation of answer. A similar mechanism for generating proofs for defeasible reasoning system DR-DEVICE is described in [BAG2007]. Defeasible rules can be translated to XSB rules that can be interpreted by XSB. The XSB trace is processed and tagged with a proof schema. In contrast, AIR allows writers to declare natural language explanation in the rule definition itself, and the details revealed in the justification can be selectively pruned. In general, the derivation steps leading to a conclusion can be explained through the Inference Web explanations (IW explanations) [MS2004]. For this the reasoner, and inference steps, must be registered with the IWBase. The proofs are marked up in PML, and are portable. The registration of AIR inference steps with IWBase has to be investigated. Currently, work is underway to mark-up proofs generated by AIR reasoner using PML.

The TMS has been used for dependency tracking in [BK2003] as well. However, [BK2003] is devoted to computing the RDFS closure, whereas in AIR we compute closure with respect to general rules. Dependency tracking in [BK2003] is tailored to optimize the maintenance of closure upon deletion of RDF data, whereas AIR reasoner tracks dependencies to generate justifications for the deduced triples in the closure. The justification has an N3 representation and can be utilized for different tasks such as proof checking, and evaluating the trustworthiness of results.

[PFH2006] gives a formal definition of LPs with context and scoped negation (CALP - context aware logic program). Contextualized reasoning is important for web rule languages, because information on the web is often assumed to be incomplete, and it's correctness is subject to the trustworthiness of the source. AIR borrows it's contextualized reasoning aspects from N3Logic. Other than them, NGs and SILK [GDK2009] support contextualized reasoning. In SPARQL queries, the query patterns can be restricted to selective named graphs, and as a result NGs naturally supports contextualized reasoning.

We formalize scoped reasoning in AIR via an additional term for context in the predicates in the translated LP. This is very similar to the approach in [PFH2006], where the model of CALP is defined in terms of the stable models and well founded models of constituent LPs. i.e. the model of an AIR program can be defined in terms of AIR closures of AIR programs under different contexts. Note that a CALP consists of multiple LPs where predicates are scoped to one or more of these LPs.

AIR, Jena, N3Logic and SwiftOWLIM are RDF based rule languages. Since RDF has fixed ternary representation these engines are optimized for RDF inferencing compared with other non RDF based rule languages.

7. Conclusion and Future Work

In this paper we have analyzed AIR, a rules language for the Semantic Web. AIR supports non-monotonic negation, and we have provided a declarative semantics that supports this negation by translating AIR programs to a specialized class of (locally) stratified LPs - PSNHLPs. While AIR does not support well-founded negation and is less expressive than other rule systems, its ability to construct explanations, declaratively manipulate them, and its support for scoped contextualized reasoning make it sufficiently unique and useful for Web reasoning. As AIR is a language for the Web, scoped contextualized reasoning is especially relevant. AIR also allows for the nesting of rules; this allows for the segmentation of the conditions of a rule so that only part of them are revealed in the justifications. We have shown that nesting can also be leveraged to order rules and therefore encode fairly expressive LPs such as PSNHLP. With slight modifications to the AIR language, it is possible to encode stratified LPs as well. Finally, we have shown that SPARQL queries may be executed by the AIR reasoner.

We plan to investigate ways to increase the expressiveness of AIR in the future. This is a twofold task. We have shown that PSNHLP (and stratified LP, with small changes to the language) can be encoded in AIR, but do not think that this is the most expressive LP that can be expressed in AIR. It may also be possible to investigate an alternative AIR reasoning algorithm in which actions that fire under the assumption of a failed condition are retracted when the rule's conditions match later on. Furthermore, with a well-defined LP translation of AIR program, it is possible to develop goal-based query answering mechanisms for these programs. We are also interested in investigating contextualization more closely. Currently, AIR does not support strategies for conflict-resolution; it may be beneficial to investigate such strategies. Finally, verification of AIR-based policies to ensure that they are behaviorally consistent with expectations may be investigated. We believe that a combination of these features will make AIR a language well-suited to the specification of policies for use in Linked Data contexts.

APPENDIX

I. Computing the upper bound UB on the number of stages that COMP_CLOSURE algorithm runs before the fix-point is achieved, for given AIR-program and facts.

Fig 13. Building blocks for graphical representation of AIR-program

Next a directed edge (dotted line) from an Assertion node to a Rule node is added if the instantiated graph pattern and the instantiated rule condition have one or more common triples. All the directed edges (single headed) from a rule node are then deleted if the union of triples in the assertion nodes, that have dotted links to this rule node, does not satisfy the rules condition. These deletions are cascaded, i.e. all the nodes at the end of the edges that were removed and all their descendants are removed. Note that, the double headed edges from a rule are not removed even when the unions of assertions in the assertion nodes, having dotted links to the rule, satisfies the condition (because a rule can first fail and succeesd in later stage). The resulting graph defines sort of the search space that is searched by the AIR reasoner. We will call the search space as the instantiatted-search-space (ISS). The AIR-closure is a subset of union of triples in the assertion nodes of the ISS. The ISS is finite since the number of rules is finite and so are their possible instantiations.

Let the weight of the double-headed edges be 1 and that of all other edges be 0. Further, the distance between two nodes in the tree is defined as the maximum of the weighted lengths of the directed paths between the two nodes, such that no two edges in the directed path are the same, and no assertion node is repeated. The intuition behind no assertion node being repeated is that once a triple is asserted, their reassertion doesn't have any effect (or it can not trigger a rule again). Similarly, the reason for not taking the same edge is that edge is representative of rule firing, and rule fires at max once, for a given set of variable bindings. Now, UB is defined as the maximum of the distances between the root and all assertion nodes. UB is finite because the ISS is finite, and no two edges in the path are the same. Since |U|, which is polynomial in number of triples in the fact base, is finite, |T| = |U|³ is also finite. By the pigeon hole principle number of assertion nodes is less than |T|. Further, since the assertion nodes are not repeated in the path that determines UB, UB ≤ |T| * maxnest, which is polynomial in number of triples in the fact base.

Corollary 3 : AIR closure is computed in finite number of stages, for arbitrary AIR programs and facts.
Proof : It follows from UB being finite.

II. Rewriting AIR rules such that all asserted graph patterns have single triple and every rule has either one air:then or one air:else property.

We show that without loss of generality, we can assume that for every rule the asserted graph pattern has single triple, maximum cardinality of air:then and air:else is 1 and every rule has only one of those properties. i.e. in Figures 1 D and 1 B, n = 1 and n₃ + n₄ = 1 always, respectively. Given any general ruleset it can be rewritten within above mentioned restrictions by duplicating rules with n > 1 and n₃ + n₄ > 1. When n > 1 but n₃ + n₄ = 1, the rule is duplicated n times and a distinct triple pattern can be retained in each of them, as shown in Figure 14 A. When n = 1 but n₃ + n₄ > 1, the rule is duplicated n₃ + n₄ times and distinct air:then or air:else property is retained in each of them, as shown in Fig 14 B. For the case when both n > 1 and n₃ + n₄ > 1, we can first duplicate rules such that n = 1 for the duplicated rules and then we are left with n rules with n = 1 and n₃ + n₄ > 1. All of the operations discussed above are lossless because of the following reasons. The asserted graph patterns can not have blank nodes or existentially quantified variables, therefore the graph pattern resulting from variable substitution is a conjunction of triples with fixed URIs for the subject, property and object and hence each of the triple pattern is independently true. In Figure 14 B, in the new rule set when :r is activated, it activates rules :r₁ to :r_n as well, that have the same condition that of :r in the original rule-set. Referring to the algorithm described in Figure 4, if condition cond is true for some set of variable bindings then all the rules (:r₁ to :r_n) will be added to SRF and will fire before any failed rule is fired. If condition cond is not true until we reach step 3.2 then none of the rules (:r₁ to :r_n) would be removed from FRF and they will fire in step 3.3.2. In both the cases the effect is same as that of rule :r firing in the original rule-set. We will refer the above modifications by lossless expansion, as we end up with more number of rules but with unchanged semantics. Please note that the transformation discussed here is similar to Lloyd-Topor transformation [L1987].

Fig 14. Lossless expansion of rules with more than 1 triple in asserted graph pattern or more than 1 then and else properties.

III. LP translation such that translated LP has a finite closure.

The TRANS function in Figure 8 & 9 can be modified, as shown in Figure 15. Unlike earlier scheme, a is true only at the stage(s) where it is inferred. Similarly, active_rule is true for an instance of ruleid, only at the stage where it is activated. The cond predicate has been refined, and an additional predicate cond_at_latest_stage, which is a restrictive form of cond predicate, is introduced. The cond_at_latest_stage(..., n) predicate is true if the corresponding cond predicate (cond(..., n)) is true and if one of the triples in the rule's condition is true at stage n (TS'-3.2). The truthfulness of cond_at_latest_stage(..., n) sort of suggests that the condition may not have been true previous to this stage as one of the subconditions was inferred only in the current stage. The TS-4 rule has been modified and is now translated to two rules instead of one. In the first (TS'-4.1), body is true if the rule is active at stage n and it's rule condition is true at current or any previous stage. While in the second (TS'-4.2), the body is true if the rule is active at some previous stage and the condition is true in the current stage. The changes discussed so far are not sufficient. Consider the factbase of one triple {:s :p :o} and the following rule-set :

:rs a air:RuleSet ;

air:rule :r1 .

:r1 a air:BeliefRule ;

air:if { :s :p :o } ;

air:then :r2 .

:r2 a air:BeliefRule ;

air:if { owl:Thing rdfs:subClassOf owl:Nothing . } ;

air:then [ air:assert { :s :p :o } ] .

While the COMP-CLOSURE would terminate and compute the closure {:s :p :o} successfully, the translated LP closure would not be finite. The closure would not be finite because, because of :r2 t_ns(:s, :p, :o, cntxtid, n + 1) will be true for every n where t_ns(:s, :p, :o, cntxtid, n) is true (since active_rule(:r1, cntxtid, 0) is true). Therefore we perform additional checks in TS'-4 and TS'-5 that the head is not true in any previous stage, expressed through known_already predicate. Like cond predicate, we need unique known_already predicates per action.

Fig 15. Revised TRANS function such that the closure Ρ is finite and UB need not be calculated.

IV. LP translations to account for the air:justifies built-in

Some of the TSs in Figures 8 and 9 must be changed and few must be added. Figure 16 lists those changes and additions only. It is assumed that the closure is being computed for facts in facts_i files and AIR-program in the airdoc_i. log:includes and log:notIncludes can also be handled similarly.

Fig 16. Extension of the TRANS function to handle the air:justifies built-in

V. Example: Translating AIR program to LP

From the translation given in Figure 17, translation to LP that doesn't require computation of UB, as described in Appendix III, may be readily apparent.

Fig 17. Translation of example AIR program to LP. qnames should be used in their expanded forms, and treated as (quoted) strings, however we use them as it is for compactness.

References

[AMOSW2003] J. Angele, E. Mönch, H. Oppermann, S. Staab and D. Wenke. Ontology-based Query and Answering in Chemistry: Ontonova @ Project Halo. In Proceedings of the Second International Semantic Web Conference 2003 (2003).
[ABW1988] K. R. Apt, H. A. Blair, and A. Walker. Towards a theory of declarative knowledge. In Foundations of Deductive Databases and Logic Programming (1988).
[A1990] K. R. Apt, “Logic Programming” Handbook of Theoretical Computer Science. Elsevier Science Publishers, pp.495–574 (1990)
[BAG2007] N. Bassiliades, G. Antoniou and G. Governatori. Proof Explanation in the DR-DEVICE System. In Proceedings of 1st International Conference on Web Reasoning and Rule Systems (RR 2007), Innsbruck, Austria (2007)
[BAV2006] N. Bassiliades, G. Antoniou and I. Vlahavas. A defeasible logic reasoner for the semantic web. In : International Journal of Semantic Web Information Systems (2006).
[B2005] T. Berners-Lee. Primer: Getting into RDF and Semantic Web using N3.
[BCPS2005] T. Berners-Lee, D. Connolly, E. Prud'homeaux, Y. Scharf. Experience with N3 rules. Position Paper in W3C Rules language Workshop, April 2005.
[BCKSH2008] T. Berners-Lee, D. Connolly, L. Kagal, Y. Scharf, J. Hendler. N3logic: A logical framework for the world wide web. In Theory and Practice of Logic Programming (2008)
[BK2003] J. Broekstra and A. Kampman. Inferencing and Truth Maintenance in RDF Schema: exploring a naive practical approach. In Workshop on Practical and Scalable Semantic Systems (PSSS) 2003.
[DEGV2001] E. Dantsin, T. Eiter, G. Gottlob, A. Voronkov. Complexity and expressive power of logic programming. In ACM Computing Surveys (2001)
[D1979] J. Doyle. A truth maintenance system. Artificial Intelligence,
[F1981] C.L. Forgy. The OPS5 user's manual. In: Tech. Rept., Carnegie-Mellon University, Dept. of Computer Science (1981).
[F1982] C.L. Forgy. Rete: a fast algorithm for the many pattern/many object pattern match problem, Artificial Intelligence 19 (1982) 17-37
[GL1991] M. Gelfond and V. Lifschitz. Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing, 9:365–385 (1991).
[GL2002] M. Gelfond and N. Leone. Logic programming and knowledge representation — the A-Prolog perspective. In Artificial Intelligence, 138(1–2):3–38 (2002).
[GGF2002] B.N. Grosof, M.D. Gandhe, T.W. Finin. Sweetjess: Inferencing in situated courteous ruleml via translation to and from jess rules. In Proceedings of the ISWC ’02 International Workshop on Rule Markup Languages for Business Rules on the Semantic Web, Sardinia, Italy, (2002)
[GDK2009] B. Grosof, M. Dean and M Kifer. The SILK System: Scalable and Expressive Semantic Rules. In International Semantic Web Conference 2009 (Poster and Demo) (2009).
[G2001] B. Grosof. Representing E-Business Rules for the Semantic Web: Situated Courteous Logic Programs in RuleML, In Proc. Workshop on Information Technologies and Systems (WITS '01), 2001.
[KHW2008] L. Kagal, C. Hanson, and D. Weitzner. Using Dependency Tracking to Provide Explanations for Policy Management. IEEE Policy 2008.
[K2008] M. Kifer. Rule Interchange Format: The Framework. In Proceedings of the 2nd International Conference on Web Reasoning and Rule Systems (2008)
[K1986] K. Kunen. Negation in Logic Programming. J. of Logic Programming 3, 1986.
[Liang2009] S. Liang, P. Fodor, H. Wan, and M. Kifer. Openrulebench:an analysis of the performance of rule engines. In Proceedings of the 18th International Conference on World Wide Web (WWW), pages 601–610, 2009.
[L1987] J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, 1987.
[MS2004] D. L. McGuinness and P. P. da Silva. “Explaining answers from the Semantic Web: the Inference Web approach”. Journal of Web Semantics, 1(4), 2004, pp. 397-413 (2004).
[P2007] A. Polleres. From SPARQL to rules (and back) : Proceedings of the 16th international conference on World Wide Web (2007)
[PFH2006] A. Polleres, C. Feier, A. Harth : Rules with contextually scoped negation. In: Proceedings of the 3rd European Semantic Web conference (ESWC2006) (2006)
[P1988] T. C. Przymusinski. On the declarative semantics of deductive databases and logic programs. In Foundations of deductive databases and logic programming 1988.
[R1994] K. A. Ross. Modular stratification and magic sets for Datalog programs with negation. In Journal of the ACM (1994)
[R2004] http://www.w3.org/TR/rdf-mt/. RDF Semantics. W3C Recommendation 10 February 2004
[RL2009] http://www.w3.org/TR/owl2-profiles/. OWL 2 Web Ontology Language Profiles W3C Recommendation 27 October 2009.
[S2008] J. Scharf. Reasoning strategies for semantic Web rule languages. M. Eng Thesis, Dept. of Electrical Engineering and Computer Science, MIT, 2008.
[SS2008] S. Schenk, S. Staab. Networked graphs: a declarative mechanism for SPARQL rules, SPARQL views and RDF data integration on the web. Proceedings of the 17th international conference on World Wide Web (2008)
[SDLT1986] M. I. Schor, T. P. Daly, H. S. Lee, and B. R. Tibbitts. Advances in Rete pattern matching. In Proceedings of the Fifth National Conference on Artificial Intelligence (1986).
[S2009] J. H. Soltren. Query-Based Database Policy Assurance Using Semantic Web Technologies. M. Eng Thesis, Dept. of Electrical Engineering and Computer Science, MIT, 2009.
[SPM1991] W. Swartout, C. Paris and J. Moore. Explanations in Knowledge Systems: Design for Explainable Expert Systems. In IEEE Expert (1991)
[SP2008] http://www.w3.org/TR/rdf-sparql-query/. SPARQL Query Language for RDF. W3C Recommendation 15 January 2008
[S2004] http://www.w3.org/Submission/SWRL/. SWRL: A Semantic Web Rule Language Combining OWL and RuleML. W3C Member Submission 21 May 2004