\documentclass{llncs}
\usepackage{url,color,floatflt, array, multirow,amsmath}
\usepackage{fancyvrb,relsize,url,graphicx,epsfig}

\setlength{\abovecaptionskip}{0pt}
\setlength{\belowcaptionskip}{0pt}

%\addtolength{\oddsidemargin}{-.3in}
%\addtolength{\evensidemargin}{-.3in}
%\addtolength{\textwidth}{.6in}

%\addtolength{\topmargin}{-.875in}
%\addtolength{\textheight}{1.75in}

% to fix the line wrapping issue
\sloppy

\DefineVerbatimEnvironment%
   {VerbatimN3}%
   {Verbatim}%
   {fontsize=\scriptsize, xleftmargin=0.25in}
\DefineVerbatimEnvironment%
   {VerbatimScript}%
   {Verbatim}%
   {fontsize=\scriptsize}

% comment out a section
\long\def\comment#1{\relax}

% something to do with air
\newcommand{\air}[1]{{\footnotesize {\textbf{#1}}}}

% qname
\newcommand{\qname}[1]{\texttt{#1}}

% something to do with lp
%\newcommand{\lp}[1]{\textrm{#1}}
\newcommand{\lp}[1]{\texttt{#1}}

% something to do with func
\newcommand{\func}[1]{{\footnotesize \textsf{#1}}}

% something to do with rdf/n3
\newcommand{\rdf}[1]{{\bf #1}}

% Put remarks in the paper easily located by ``bigodot'' in margin
% Usage: \todo{twf: we need a better example here.}
\newcommand{\todo}[1]{
\mbox{}\marginpar[\hfill$\bigodot$]{$\bigodot$\hfill}
{\sc#1}}
%\newcommand{\todo}[1]{{\bf TODO:} #1}

\comment{\newcommand{\qed}{\hfill \ensuremath{\Box}}}

%% ISWC 2010 Research Track
%% http://iswc2010.semanticweb.org/node/8

\begin{document}

\title{Analyzing the AIR Language: A Semantic Web (Production) Rule Language
\thanks{\small This work was supported in part by  NSF Cybertrust award CNS-0831442, IARPA award 
    FA8750-07-2-0031, AFOSR award FA9550-09-1-0152, and
support to RPI from the Information Technology Alliance in Network and
Information Science by U.S. ARL and the U.K. MoD under Agreement
Number W911NF-06-3-0001}}

\author{Ankesh Khandelwal\inst{1} \and Jie Bao\inst{1} \and Lalana
  Kagal\inst{2} \and Ian Jacobi\inst{2} \and Li Ding\inst{1} \and
  James Hendler\inst{1}}

\institute{
Rensselaer Polytechnic Institute \\
Troy, NY 12180\\
\email{\{ankesh, baojie, dingl, hendler\}@cs.rpi.edu} 
\and
Massachusetts Institute of Technology \\
Cambridge, MA 02139 \\ 
\email{ \{lkagal, jacobi\}@csail.mit.edu}
}

\maketitle
\setcounter{footnote}{0} 
\begin{abstract}
The {\bf A}ccountability {\bf I}n {\bf R}DF ({\it AIR}) language is an
N3-based, Semantic Web production rule language that supports nested
activation of rules, negation, closed world reasoning, scoped contextualized
reasoning, and explanation of inferred facts. Each AIR rule has
unique identifier (typically an HTTP URI) that supports reuse of rule. 
In this paper we analyze the semantics of AIR language by: i) giving
the declarative semantics that support the reasoning algorithm, ii) 
providing complexity of AIR inference; and iii) evaluating the expressiveness
of language by encoding Logic Programs of different expressivities in 
AIR.
\end{abstract}

\comment{{\bf Keywords} : rule language, rule engine, production rule, 
non-monotonic reasoning, negation, formalization, web language.}

\section{Introduction}
\label{sec:intro}

AIR was developed as an extension to N3Logic~\cite{N3Logic} to support 
accountable privacy protection in Web-based information systems~\cite{KHW2008}. 
While N3Logic supports scoped contextualized reasoning (SCR), nested
graphs, and built-in functions, AIR additionally supports rule reuse, 
rule nesting and explanation of rule-based inference. AIR rules are 
encoded in N3\footnote{http://www.w3.org/DesignIssues/Notation3.html}, which
extends the expressiveness of RDF with (i) the ability to use graphs as literal values,
(ii) universal or existential quantification of variables in a graph and 
(iii) built-in functions and operators represented as RDF properties.

AIR is designed to provide detailed explanations for actions performed by 
AIR reasoner. AIR permits natural language descriptions to be added to 
actions, so that when an action is performed the description is included
in the justification, by the reasoner. Since justifications can 
potentially reveal sensitive information from the knowledge base or
expose bias in the rules, AIR also provides ways to customize explanations,
e.g. hiding actions of certain rules.

AIR rules have unique IDs (IRIs), which enables the rules to be part
of the linked data cloud and reused by other rule definitions.
Furthermore, AIR rules can be nested. These features are natural to 
model real-world rules and laws where conditions are often split into
sequentially-activated rules, and rules are frequently reused.

AIR supports rule definitions in which Web resources, such as
triple stores with SPARQL~\cite{SPARQL} end-points, can be objectively
checked for patterns. Sometimes the data has an associated intensional
component, defined through rules. For complete access to the data, AIR
supports inclusion of certain inferences without allowing the rules in 
the intensional component to be applied to the entire input data. SCR is
important for a Web rule languages because information on the Web is
often assumed to be incomplete, and its correctness is subject to the
trustworthiness of the source.

There are many rule languages and rule systems; some are more advanced
while others are at prototypical levels. Liang et. al. give a nice
overview of popular, and often advanced, rule systems in
\cite{LFWK2009}. Examples of rule languages include N3Logic,
NG~\cite{SS2008}, SILK~\cite{G2009}, and SWRL~\cite{SWRL}, while some
rule engines include Jess\footnote{http://www.jessrules.com/},
Jena\footnote{http://jena.sourceforge.net/}, and
XSB\footnote{http://xsb.sourceforge.net/}. These languages and
systems have different levels of expressiveness and features.

Networked Graphs (NGs) supports the well-founded (WF) negation, XSB
supports Negation as Failure (NAF), and Jess, a production rule
system, supports non-logical negation. SILK supports WF negation, as
well as classical negation. SWRL and Jena do not support negation.  In
comparison, N3Logic supports monotonic negation, and AIR supports
non-monotonic negation, which is different from negation accepted by the systems above.

Rule Interchange Format (RIF)~\cite{K2008} has two major dialects --
the Framework for Logic Dialects (FLD) and the Production Rule Dialect
(PRD). Unlike PRD, actions in AIR cannot modify or remove facts, but
they can add new production rules. 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
standard first-order logic semantics. AIR is neither more nor less
expressive than BLD. Unlike BLD, function symbols are not supported in
AIR, whereas AIR supports negation. SWRL is a function-free rule
language limited to binary and unary predicates, and all its features,
barring different-from, are covered by BLD. AIR is as expressive as
SWRL, and also supports negation.

OPS/YES~\cite{SDLT1986} extends the OPS5~\cite{F1981} production rule
system with many features including {\it incremental rule addition},
which allows matching in the actions. AIR has a similar notion of rule
nesting. Other than AIR, of the systems mentioned above, only Jena
supports (partially) nesting of rules.

In SPARQL, query patterns can be restricted to selective named graphs,
and as a result NGs naturally supports SCR. Other than N3Logic,
AIR, and NGs, SILK also supports SCR\comment{~\cite{G2009}}.

The Ontonova system~\cite{AMSW2003} provides natural language
explanation of proof trees for conclusions by the
Ontobroker\footnote{http://ontobroker.semanticweb.org/} through
meta-inferencing. A similar mechanism for generating proofs for
defeasible reasoning system DR-DEVICE is described in
\cite{BAG2007}. In contrast, the explanations for conclusions in AIR
are generated by the reasoner itself, and the justification can be
declaratively modified by changing rule definitions.

AIR's focus on explanation generation for Web reasoning makes it
unique. Other distinguishing features include AIR's ability to treat 
AIR rules as part of linked data and the ability to match
patterns against remote triple stores.

\comment{Some of the other
features of AIR are present in other rule systems, but there are no
systems with all of them. Therefore, we analyze the semantics and
expressiveness of AIR.} While AIR has a production rule syntax, it is limited to
assertions of facts, and addition of rules. Neither can facts be
removed from the current state of the world nor any procedural
attachments may be called. Therefore, we can define its declarative semantics. 
In this work we define the model-theoretic semantics of AIR-programs, 
by defining the translation of an arbitrary AIR-program to a semantically equivalent stratified
Logic Program (LP).

There has been an earlier work on translating Jess to and from
Situated Ordinary LP (SOLP)\footnote{http://sweetrules.projects.semwebcentral.org/sweetrules-overview-presentation-2005-04-24-v3.pdf}
and Situated Courteous LP (SCLP)~\cite{GGF2003}, showing
interoperability of the two rule languages. However, Jess and AIR are
very different rule languages. Jess, unlike AIR, supports procedural
attachments and with certain restrictions on its features has been
shown to support (stratified) NAF~\cite{GGF2003}. Not only is the
notion of nesting of rules absent from Jess, AIR's negation is
different from NAF. \comment{We also formalize the notion of context in AIR,
and our approach is similar to that in \cite{PFH2006}, which
formalizes contextualized reasoning in LP.} The authors are not aware
of any other related works.

The remainder of the paper is organized as follows. Section 2 provides
an overview of the AIR language and reasoning. In section 3, we define 
a new class of stratified LP - Positively Stratified Negatively 
Hierarchical LP (PSNHLP). In section 4, we define the declarative 
semantics, and provide the data and program complexities of AIR programs. 
In section 5, we show how LP rules and fairly expressive LPs, such as 
PSNHLP, can be encoded in AIR. We conclude in section 6 with a summary and
discussion on future work.

There is a longer version of the paper~\cite{KBKJDH2010}\footnote{http://tw.rpi.edu/proj/tami/AIR\_Language\_Formalization}, 
that includes review of standard terminologies used in Logic Programming, 
proofs of all the claims, and detailed comparison of AIR with other rule 
systems.

\section{AIR Overview}
\label{sec:overview}

The AIR production rule system has two components- the rule language
and the rule engine (reasoner). The reasoner computes the closure, 
{\bf AIR-closure}, for given facts, in N3, with respect to given AIR-program. 
An {\bf AIR-program} contains one or more AIR-rules. The 
closure contains the initial facts and all the facts that can be 
deduced from it using the given rules. We will review the AIR 
language, and introduce the algorithm for computing the closure 
in sections \ref{sec:language} and \ref{sec:algorithm}. 
The details about AIR justification are available at~\cite{kagal10gasping}.
%\footnote{http://dig.csail.mit.edu/2010/Papers/ISWC-AIR/paper.pdf}.

\subsection{AIR Language}
\label{sec:language}

AIR rules are defined using following properties: \qname{air:if},
\qname{air:then}, \qname{air:else}, \qname{air:description},
\qname{air:rule} and \qname{air:assert}, according to the AIR abstract
syntax\footnote{http://tw.rpi.edu/proj/tami/AIR\_Abstract\_Syntax}.
A template for declaring an AIR-program is shown in
Figure~\ref{fig:template}.  This template will be used in the later
sections. When we refer to s and o related by \qname{p1.p2} we mean
that \qname{s p1 [ p2 o ]} holds.

\begin{figure}[!t]
\begin{center}\scriptsize
\parbox{0cm}
{\begin{tabbing}
A. RULE SET\\
\# $m_1 \ge 0$, $m_2 > 0$ \\
@forAll $<u\_var_1>, \ldots, <u\_var_{m_1}>$ .\\
\\
$<$setid\=$>$ a air:RuleSet ;\\
\>    air:rule $<ruleid_1>, \ldots, <ruleid_{m_2}>$ . \\
\\
B. RULE\\
\# $n_1, n_2, n_3, n_4 \ge 0, n_3 + n_4 > 0$\\
$<$ruleid\=$>$ a air:BeliefRule ; \# alternatively air:HiddenRule, air:EllipsedRule\\
\>    air:if \{ \=@forSome $<e\_var_1>, \ldots, <e\_var_{n_1}>$ . \\
\> \>             $s_1 <p_1> o_1$ . \\
\> \>             $\ldots$ \\
\> \>             $s_{n_2} <p_{n_2}> o_{n_2}$ . \} ; \\
\>    air:then $<t\_action_1>, \ldots, <t\_action_{n_3}>$ ; \\
\>    air:else $<e\_action_1>, \ldots, <e\_action_{n_4}>$ .\\
\\
C. ACTIVATING NEW RULE\\
$<$action\=$>$ air:description (list\_of\_var\_and\_str) ;\\
\>    air:rule $<ruleid>$ . \\
\\
D. ASSERTING A GRAPH PATTERN\\
\# $n > 0$\\
$<$action\=$>$ air:description (list\_of\_var\_and\_str) ; \\
\>    air:assert \{\= $s_1 <p_1> o_1$ . \\
\> \>              $\ldots$ \\
\> \>              $s_n <p_n> o_n$ . \} .
\end{tabbing}
}
\end{center}
\caption{{\bf Template for defining AIR-program}}
\label{fig:template}
\end{figure}

The rules are of the form \qname{air:if {\it condition}; air:then {\it
    then-actions}; air:else {\it else-actions}}. The condition is
specified as a graph pattern, similar to the Basic Graph Pattern 
of SPARQL queries, which may be pattern matched against N3
graphs. Whenever the condition matches the current state of the world,
i.e. the facts known or inferred so far, variables may acquire
bindings and all the \qname{then-action}s are fired. Otherwise all the
\qname{else-action}s are fired.
 
The rules are grouped under rule-sets. The rules nested directly under
the \qname{RuleSet} are referred to as the {\bf top rule}s of the
rule-set. A rule ({\bf child rule}) nested under another rule ({\bf
  parent rule}) via \qname{air:then.air:rule} is said to be positively
nested and a rule nested via \qname{air:else.air:rule} is said to be
negatively nested. A {\bf 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. \qname{t\_action$_i$}s and
\qname{e\_action$_i$}s, in Figure~\ref{fig:template}, are the
\qname{then-action}s and \qname{else-action}s, respectively. Together
they are referred to as \qname{action}s. The actions can be annotated
with natural language description through the \qname{air:description}
property. Note that the description can be defined using variables.

The existentially quantified variables may be declared within the
condition.  The universally quantified variables are declared outside
of the rule. The scope of existentially quantified variable is the
condition where it's declared, and of 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
\qname{air:assert}, and the nested rule is declared using
\qname{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 with an \qname{air:else}
property \comment{can we rephrase "rule with an air:else property"?
  -AK} is activated, its condition cannot contain unbounded
universally quantified variables.

\begin{figure}[!t]
\begin{center}
\begin{VerbatimN3}
@prefix air:<http://dig.csail.mit.edu/TAMI/2007/amord/air#>. 
@prefix conf:<http://www.conf.org/ontology#>.
@prefix pol:<http://www.conf.org/policies/publication#>. 
@prefix:<http://www.conf.org/policies/publication#>.

pol:PubInProcPolicy a air:RuleSet ;
    air:rule pol:CheckPub .

@forAll :PUBL .
pol:CheckPub a air:BeliefRule ; 
    air:if { @forSome :PROC . <http://www.conf.org> conf:hasProceedings :PROC . 
             :PROC conf:hasPaper :PUBL . } ; 
    air:then [ air:description (:PUBL " published in this conference") ;  
               air:rule pol:ChkNonCompl ],
             [air:rule pol:CheckAuth], [air:rule pol:CheckExempt]. 

pol:ChkNonCompl a air:BeliefRule ; 
    air:if { :PUBL air:compliant-with pol:PubInProcPolicy . } ; 
    air:else [ air:description ("the publication of " :PUBL " is questionable as 
                                      it did not meet any of the two criteria") ; 
               air:assert { :PUBL air:non-compliant-with pol:PubInProcPolicy } ] . 

@forAll :AUTH .
pol:CheckAuth a air:BeliefRule ;
    air:if {:PUBL conf:hasAuthor :AUTH.<http://www.conf.org> conf:registeredBy :AUTH.}; 
    air:then [ air:description ("Author," :AUTH " registered for the conference"); 
               air:assert { :PUBL air:compliant-with pol:PubInProcPolicy } ] .

@forAll :REASON .
pol:CheckExempt a air:BeliefRule ; 
    air:if { @forSome :COCHAIR, :EXEMPTION . 
             :COCHAIR a conf:Co-Chair . :PUBL conf:hasFirstAuthor :AUTH .
             :EXEMPTION a conf:PublicationExemption ; conf:exemptedBy :COCHAIR ; 
                   conf:exemptee :AUTH ; conf:reason :REASON . } ; 
    air:then [ air:description ("the first author " :AUTH " was exempted by one of the 
                                                         cochairs, because " :REASON); 
               air:assert { :PUBL air:compliant-with pol:PubInProcPolicy } ] .
\end{VerbatimN3}
\end{center}
\caption{{\bf Example AIR-program, describing the publication policy}}
\label{fig:example}
\end{figure}
Traditionally, rule languages have been designed assuming that all
rules will apply on all input data. However, this is not desirable for
a web rule language \cite{N3Logic,PFH2006}, and therefore AIR supports
SCR. The matching of a condition pattern can be scoped to web
documents, RDF-stores with SPARQL end-points, or to the AIR-closure of
some facts and AIR-programs using the
\qname{log:semantics.log:includes},
\qname{sparql:queryEndPoints.log:semantics.log:includes} and
\qname{air:justifies} built-ins respectively. Note that by using
\qname{air:justifies}, a subset of rules can be applied to a subset of
data, if desired, without risking the application of those rules to
the entire input data.  \comment{One of the reviewers had requested
  for examples showing contextualized reasoning.  Should we show it
  here? Or should we leave it to the user to refer other AIR
  references for the example? - AK Show it here - lk} In addition to
the built-ins for scoped reasoning, AIR supports most of the N3Logic
built-ins\footnote{http://www.w3.org/2000/10/swap/doc/CwmBuiltins}
for cryptographic, math, string, list and time functions.

\begin{figure}[t]
\begin{center}\scriptsize
\begin{tabular}{|p{5.9cm} | p{5.9cm}|}
%{fontsize=\scriptsize, xleftmargin=0.25in}
\hline
\parbox{5.9cm}{
{\bf A. Data Structures} \\
rule = (ruleid, condition, success, then-actions, else-actions) \\
then(else)-actions = list of child rules to be activated and graphs  to be asserted \\
RB = set of active rules\\
FB = set of facts\\
SRF = queue of (rule, bindings) tuples\\
FRF = queue of rules\\
\\
{\bf B. COMP-CLOSURE}\\
INPUT : AIR-program, facts\\
OUTPUT : Closure of facts w.r.t. the AIR-program in FB\\
1. Initialize the data-structures\\
1.1. FB = facts\\
1.2. RB = $\phi$\\
1.3. SRF = empty queue\\
1.4. FRF = empty queue\\ 
1.5. FRF' = empty queue\\
2. For each top rule, of all \qname{RuleSet}s in AIR-program\\
2.1. add-to-rulebase(R)\\
3. while SRF and FRF is non empty\\
3.1. while SRF is non empty\\
3.1.1. f = SRF.dequeue(), i.e. remove first queue element and assign it to f\\
3.1.2. rule-fire(f.rule.then-actions, f.bindings)\\
3.2. while FRF is non empty\\
3.2.1. f = FRF.dequeue()\\
3.2.2. if f.rule.success is false\\
3.2.2.1. FRF'.enqueue(f)\\
3.3. while FRF' is non empty\\
3.3.1. f = FRF'.dequeue()\\
3.3.2. rule-fire(f.rule.else-action, \{\})\\
}
&
\parbox{5.9cm}{
{\bf C. RULE-FIRE}\\
INPUT : actions, bindings bndgs\\
OUTPUT : updated RB and FB\\
1. for action in actions :\\
1.1. substitute all variables in action which have bindings with bound values from bndgs\\
1.2. if action is a rule\\
1.2.1. add-to-rulebase(action)\\
1.3. if action is a graph\\
1.3.1. add-to-factbase(action)\\
\\
{\bf D. ADD-TO-RULEBASE}\\
INPUT : rule\\
OUTPUT : updated RB and (SRF or FRF)\\
1. if rule not in RB\\
1.1. add rule to RB \\
1.2. R.success = False\\
1.3. pattern match rule.condition against FB\\
1.4. If rule.condition matched a sub-graph\\
1.4.1. R.success = True\\
1.4.2. for each sub-graph that matched rule.condition\\
1.4.2.1. SRF.enqueue((rule, bindings))\\
1.5. If rule.condition did not match any sub-graph\\
1.5.1. FRF.enqueue(rule)\\
\\
{\bf E. ADD-TO-FACTBASE}\\
INPUT : graph (grounded graph pattern)\\
OUTPUT : updated FB, RB and SRF\\
1. let graph' = graph $\setminus$ FB\\
2. if $graph' \ne \phi$\\
2.1. add triples in graph' to FB\\
2.2. for each rule in RB\\
2.2.1. pattern match rule.condition against FB\\
2.2.2. If rule.condition matched a sub-graph {\it g} s.t. that {\it g} $\cap$ graph' $\ne \phi $\\
2.2.2.1. rule.success = True\\
2.2.2.2. for each sub-graph {\it g} that matches the rule.condition and {\it g} $\cap$ graph' $\ne \phi $\\
2.2.2.2.1. SRF.enqueue((rule, bindings))
}\\
\hline
\end{tabular}
\end{center}
\caption{{\bf The \air{COMP-CLOSURE} algorithm, and related data-structures and algorithms.}}
\label{fig:algorithm}
\end{figure}

Figure~\ref{fig:example} shows an example AIR-program. It expresses
the conference policy: any paper accepted in the conference
should be published in the proceedings only if one
of the authors has presented it in the conference
(\qname{pol:CheckAuth}), or the first author has received an exemption
from one of the co-chairs (\qname{pol:CheckExempt}). The former
condition is interpreted in practice by checking to see if one of the
co-authors has registered for the conference. It is assumed that the
conference activities are logged using the same vocabulary as that
used in the rules. \qname{pol:CheckPub} is the only top rule, and the
three rules, \qname{pol:ChkNonCompl}, \qname{pol:CheckAuth}, and
\qname{pol:CheckExempt} are its child rules.

\subsection{AIR Reasoning (The Procedural Semantics) }
\label{sec:algorithm}

The AIR reasoner employs a RETE~\cite{F1982} based forward-chaining
approach to compute the AIR-closure. Figure~\ref{fig:algorithm}
describes the \air{COMP-CLOSURE} algorithm used for computing the
AIR-closure.  The data structures and algorithms described here are
abstractions of the actual implementation~\cite{kagal10gasping}. 
For instance \air{FB} (Fact Base), which is shown to be a set of facts, 
is actually an efficiently indexed triple store, and \air{RB} 
(Rules Base), the set of active rules, is compiled into the RETE 
framework. The abstraction is sufficient for analyzing the language.

One cycle of step 3 of \air{COMP-CLOSURE} is referred to as a {\bf
  stage}, i.e. steps 3.1 to 3.3 (3.3.1 and 3.3.2 included) constitute
one stage of the algorithm. Furthermore, step 3.1 is referred to as a
positive stage, denoted by {\bf stage$^{+}$} and steps 3.2 and 3.3
constitute a negative stage, denoted by {\bf stage$^{-}$}. We will be
using stage$_i$, stage$_i^{+}$ and stage$_{i}^{-}$ to refer to
i$^{\textrm th}$ stage, stage$^{+}$ and stage$^{-}$, respectively.

In any given stage, successful rules are given priority over failed
rules, and their \qname{then-action}s are effected in
stage$^{\textrm{+}}$ before failed rules fire. When all successful
rules have fired, the world is temporarily closed and the
\qname{else-action}s of all the failed rules are fired in stage$^{-}$
with the belief that the conditions of all the failed rules are
false. AIR reasoning enters the next stage once the failed rules have
all fired. The \air{COMP-CLOSURE} algorithm computes the next stage
until the fixpoint is reached, i.e. when both the \air{SRF} and
\air{FRF} are empty.

\comment{This figure must be centered, verbatim can not be -AK}
\begin{figure} [t]
\begin{center}%\scriptsize
%\parbox{10cm}{
\begin{VerbatimN3} 
@prefix colog:<http://www.conf.org/log#>. @prefix conf:<http://www.conf.org/ontology#>.
<http://www.conf.org>   conf:hasProceedings   colog:proc .
colog:proc              conf:hasPaper         colog:pub1 .
colog:pub1              conf:hasAuthor        colog:auth1 .
<http://www.conf.org>   conf:registeredBy     colog:auth1 .
\end{VerbatimN3}
\end{center}
\caption{{\bf Example of input facts:} sub-graph from log of conference activities.}
\label{fig:log}
\end{figure}

Consider the input facts in Figure~\ref{fig:log} and the example
AIR-program from Figure~\ref{fig:example}. The AIR-closure contains
one additional triple \qname{colog:pub1 air:compliant-with
  pol:PubInProcPolicy}. In order to compute the closure, \air{FB} is
initialized by triples in the input and \qname{pol:CheckPub} is added
to the \air{RB}. When the rule is added, its condition matches and it
is added to the \air{SRF} with \qname{pol:PUBL} bound to
\qname{colog:pub1}.  When it fires, the three child rules are added to
the \air{RB}. Only \qname{pol:CheckAuth} succeeds and other rules are
added to the \air{FRF}. The \qname{pol:CheckAuth} is added to the
\air{SRF} with \qname{:AUTH} bound to \qname{colog:auth1}. It fires
next, and asserts the triple \qname{colog:publ1 air:compliant-with
  pol:PubInProcPolicy}. When that triple is added, it satisfies the
\qname{pol:ChkNonCompl}'s condition and the rule's success attribute
is set to true. \air{SRF} is now empty and \qname{pol:ChkNonCompl} is
removed from \air{FRF}. \qname{pol:CheckExempt} is then added to
\air{FRF}. However, it doesn't have an \qname{air:else} property. The
fixpoint is reached at the end of first stage.

\section{Positively Stratified Negatively Hierarchical Logic Programs}
\label{sec:PSNHLP}

We will review definitions of {\it Ground}$(R)$, the {\it $T_P$
  operator} and the {\it perfect model} semantics for stratified LPs, before
defining PSNHLPs. {\it Ground}$(R)$ refers to the set of all possible
ground instances of $R$, with respect to given universe of constant
symbols $U$, where $R$ is a rule or an LP. $T_P$ is the one-step
induction operator \cite{A1990} associated with an LP $P$, defined by
:
\begin{quote}
\begin{tabbing}
$T_P(I)$ = \{ $A_0 \mid P$ \= contains a rule whose instantiation is 
$A_0 \leftarrow A_1, \ldots, A_n$ \\ \>such that $\{A_1, \ldots, A_n\} \subseteq I$ holds \}
\end{tabbing}
\end{quote}
where $I$ is the given set of atoms that are true. $T_P^{\omega}$ is the 
fix-point operator, i.e. $T_P$ is applied repeatedly until the fix-point
is reached.

The semantics of a (locally) stratified LP, $P$, is defined in terms
of its {\it perfect model}, which we refer to by {\it PM}$(P)$. $P$
entails a ground atom $A$ iff $A$ belongs to {\it PM}$(P)$.  Let $P_1
\cup \ldots \cup P_n$ be the (local) stratification of $P$ ({\it
  Ground}$(P)$). We can choose a stratification and assignment of 
levels to predicates such that the rule $A~ \leftarrow~ L_1,~ \ldots,~ L_m$ in P is in P$_i$ iff the level 
assigned to $A$ is $i$, and we will assume that to be the case in rest
of the paper. {\it PM}$(P)$ = $M_n$ \cite{P1988}, which is
defined by :
\begin{quote}
$M_1 = T_{P_1}^{\omega}(\phi)$, $M_2 = T_{P_2}^{\omega}(M_1)$, $\ldots$, $M_n = T_{P_n}^{\omega}(M_{n-1})$
\end{quote}

When a rule contains a negative literal in the body, we will refer it
as {\bf negative rule}.  All other rules are thus {\bf positive
  rules}. An LP $P$ is {\bf PSNHLP} if there is an assignment 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, an LP $P$ is locally PSNHLP
if such an assignment of ordinal levels is possible over ground atoms
for {\it Ground}$(P)$. Every hierarchical LP is PSNHLP, and every
PSNHLP is stratified LP. This doesn't hold in opposite direction.

Let $P_1 \cup \ldots \cup P_n$ be the stratification of a PSNHLP $P$, 
and let $P_i^+ \cup P_i^-$ is the partition of P$_i$ such that a 
rule from P$_i$ is in P$_i^+$ if it is positive and in $P_i^-$ 
otherwise. Then, the {\bf PSNH-stratification} of $P$ is defined 
as $P = P_1^+ \cup P_1^- \cup \ldots \cup P_n^+ \cup P_n^-$. 
The predicates in the body of a rule in $P_i^-$ have levels strictly 
smaller than $i$. The {\it PM}(P) = M$_n$, where 
M$_n$ is defined by:
\begin{quote}
$M_1 = T_{P_1}^{\omega}(\phi)$,\\
$M_2' = T_{P_2^-}(M_1)$, $M_2 = T_{P_2^+}^{\omega}(M_2')$,\\
$\ldots$\\
$M_n' = T_{P_n^-}(M_{n-1})$, $M_n = T_{P_n^+}^{\omega}(M_n')$
\end{quote}
such that $M_1 = T_{P_1}^{\omega}(\phi)$, and $M_i = T_{P_i}^{\omega}(M_{i-1})$ for $i > 1$.  The former 
holds because $P_1 = P_1^+$ (i.e. $P_1^- = \phi$). The latter follows from following claim.\\

\noindent
{\bf Claim 1}: $T_{P_i}^{\omega}(M_{i-1}) = T_{P_i^+}^{\omega}(T_{P_i^-}(M_{i-1}))$

\section{Declarative Semantics}
\label{sec:declarative}
\comment{using \Delta instead of \Alpha. using \kappa in place \fnof. need better symbols. -AK}

The declarative semantics of AIR-program can be defined in terms of a
semantically equivalent PSNHLP. We will first define $\tau$, that translates
AIR-program  $\Delta$ to LP $\wp$. We will then show that $\wp$ is PSNHLP and that the 
AIR-closure of $\Delta$ and input facts $\kappa$, mapped as ground facts in $\wp$, 
is same as {\it PM}$(\wp)$. $\wp$ contains rules for predicates \lp{t}, \lp{t$_s$}, 
\lp{active\_rule} and \lp{cond}, with following meanings :

\begin{itemize}%{$\bullet$}
\item \lp{t(s, p, o)} represents N3 triple \qname{\{s p o\}}.
\item \lp{t$_s$(s, p, o, c, n)} represents true N3 triple \qname{\{s
  p o\}}, in the \lp{n}$^{\textrm{th}}$ stage of reasoning, in context \lp{c}. 
\item \lp{active\_rule(ruleid, ?v$_1$, $\ldots$, ?v$_m$, c, n)} represents
	active AIR-rule, \lp{ruleid}, in the \lp{n}$^{\textrm{th}}$ stage, in
    context \lp{c}. The exact instance of the rule is determined by the partial
  bindings of \lp{?v$_i$}'s.  \lp{?v$_i$}'s are the universally
  quantified variables used in the chain of rules to which \lp{ruleid}
  belongs. For example, the rule \qname{pol:CheckAuth} has two
  variables \lp{?PUBL} and
  \lp{?AUTH}. \\ If, for example, \lp{active\_rule(pol:CheckAuth, colog:pub1, ?AUTH, c,
    1)} atom is true, then an instance of the rule \qname{pol:CheckAuth} is
  active at the 1$^{\textrm{st}}$ stage with \lp{?PUBL} bound to
  \qname{colog:pub1} in the context \lp{c}. Here \lp{?AUTH} is unbound
  and can be bound by any constant from U.
\item \lp{cond(ruleid, ?cv$_1$, $\ldots$, ?cv$_m$, c, n)} represents a 
  satisfied condition of the AIR-rule, \lp{ruleid}, in the
  \lp{n}$^{\textrm{th}}$ stage, in context \lp{c}. The \lp{?cv$_i$}'s are universally or existentially
  quantified variables occurring in the rule's condition.  The
  \func{VAR\_IN\_COND} function returns all these
  variables for given rule. If, for example, \lp{cond(pol:CheckAuth,
    colog:pub1, colog:auth1, c, 1)} atom is true then the condition of \qname{pol:CheckAuth}
  rule is true in 1$^{\textrm{st}}$ stage, in context c, when \lp{?PUBL} and \lp{?AUTH} are bound to
  \qname{colog:pub1} and \qname{colog:auth1} respectively.
\item \lp{succ} (successor) and \lp{=} predicates are used with their
  usual meanings.
\end{itemize}
The {\bf context} may be defined by a collection of N3 and/or AIR-program 
sources, and is identified with an ID. We must use unique predicate 
symbols to distinguish \lp{active\_rule} and \lp{cond} predicates for 
same rule in different rule chains.
\begin{figure}[t]
\begin{center}\footnotesize
\parbox{12.5cm}{
\begin{tabbing}
A. \func{TRANS}(setid), where setid is a RULE-SET\\
1. ruleset(setid, c) .\\
2. for \= i in 1 to m$_2$\\
\> active\_rule(ruleid$_i$, ?u\_var$_1$, $\ldots$, ?u\_var$_{m_1}$, ?c, 1) $\leftarrow$ ruleset(setid, ?c) .\\
B. \func{TRANS}(ruleid), where ruleid is a RULE\\
3. cond(ruleid, \= \func{VAR\_IN\_COND}(ruleid), ?c, ?n) $\leftarrow$ t$_s$(\func{MAP}(s$_1$), \func{MAP}(p$_1$), \func{MAP}(o$_1$), \\\>?c, ?n),
$\ldots$, t$_s$(\func{MAP}(s$_{n_2}$), \func{MAP}(p$_{n_2}$), \func{MAP}(o$_{n_2}$), ?c, ?n), ?n $\le$ UB .\\
4. for \= i in 1 to n$_3$\\
\> \func{TRANS}(t\_action$_i$, \= ?n) $\leftarrow$ active\_rule(ruleid, ?u\_var$_1$, $\ldots$, ?u\_var$_{m_1}$, ?c, ?n), \\
\>\> cond(ruleid, \func{VAR\_IN\_COND}(ruleid), ?c, ?n), ?n $\le$ UB .\\
5. for \= i in 1 to n$_4$\\
\>\func{TRANS}\= (e\_action$_i$, ?m) $\leftarrow$ active\_rule(ruleid, ?u\_var$_1$, $\ldots$, ?u\_var$_{m_1}$, ?c, ?n), \\
\>\> \textit{not}(cond(ruleid, \func{VAR\_IN\_COND}(ruleid), ?c, ?n)), succ(?m, ?n), ?n$\le$UB.\\
C. \func{TRANS}(action, ?n), where action is ACTIVATING NEW RULE\\
6.  active\_rule(ruleid, ?u\_var$_1$, $\ldots$, ?u\_var$_{m_1}$, ?c, ?n)\\
\\
D. \func{TRANS}(action, ?n), where action is ASSERTING A GRAPH PATTERN\\
7. t$_s$(\func{MAP}(s$_1$),\func{MAP}(p$_1$),\func{MAP}(o$_1$), ?c, ?n), $\ldots$, t$_s$(\func{MAP}(s$_n$),\func{MAP}(p$_n$),\func{MAP}(o$_n$),?c,?n)\\
\\
E. \func{TRANS}(\{s p o\}), where \{s p o\} is INPUT FACT\\
8. t$_s$(s, p, o, c, 1) .
\end{tabbing}
}
\end{center}
\caption{{\bf \lp{\func{TRANS}(ele, ?n)} definition,} where \lp{ele} is defined according to the template in Figure~\ref{fig:template}}
\label{fig:trans}
\end{figure}

$\tau(\Delta)$ is defined by conjunction of the rules returned from \func{TRANS}\lp{(setid)} 
and \func{TRANS}\lp{(ruleid)}, for every rule set and production rule in $\Delta$, respectively. 
Figure~\ref{fig:trans} gives the definition of {\bf \func{TRANS}\lp{(ele, ?n)}} function, for  \lp{ele}'s
in a built-in-free AIR-program. The \lp{ele}s are described as per the template in Figure~\ref{fig:template}, 
and \lp{?n} is optional argument.

The {\bf \func{MAP}\lp{(val)}} function maps \lp{val} to \lp{?val} or
\lp{val} depending on whether \lp{val} is declared as a variable or
not. \lp{UB} is the upper bound on number of stages required for
computing the fix-point for given AIR-program and initial
facts. \lp{UB} is finite because assertions can use
only fixed IRIs (i.e. no blank nodes are allowed in the asserted
graph), and every fact and rule instance is asserted at most
once. \lp{UB} is polynomial in the size of input facts and the maximum 
depth of nesting in input AIR-program~\cite{KBKJDH2010}. \lp{?n $\le$ UB} ensures 
that the closure for $\wp$ is finite. 
Additional rules that hold in every $\wp$ are shown in Figure~\ref{fig:transconst}.

The triples in $\kappa$ are translated as facts into $\wp$, in 
translation step (TS) 8. The triples asserted and the rules 
activated when the rule condition is satisfied are true from the 
same stage (TS-4), whereas they are true only from next stage 
when the rule condition failed (TS-5). The definition in 
Figure~\ref{fig:trans} can be extended to handle the built-ins for SCR, namely
\qname{air:justifies}, \qname{log:includes}, and \qname{log:notIncludes}~\cite{KBKJDH2010}.

For example, \func{TRANS}(\qname{pol:ChkNonCompl}) yields following rules :
\begin{itemize}\footnotesize
%{$\bullet$}
\item {\begin{tabbing}t$_s$(?P\= UBL , \qname{air:non-compliant-with}, \qname{pol:PubInProcPolicy}, ?c, ?m)
$\leftarrow$\\ \> active\_rule(\qname{pol:ChkNonCompl}, ?PUBL, ?c, ?m), succ(?n, ?m), ?n $\le$ UB, \\ 
\>\textit{not}(cond(\qname{pol:ChkNonCompl}, ?PUBL, ?c, ?n)) .\end{tabbing}}
\item {\begin{tabbing}cond(\= \qname{pol:ChkNonCompl}, ?PUBL, ?c, ?n) $\leftarrow $ \\ \>
t$_s$(?PUBL,\qname{air:compliant-with}, \qname{pol:PubInProcPolicy}, ?c, ?n) .\end{tabbing}}
\end{itemize}

\begin{figure}[t]
\begin{center}\footnotesize
\parbox{12.5cm}{
9. active\_rule(?x$_1$,$\ldots$,?x$_m$, ?c, ?n)$\leftarrow$active\_rule(?x$_1$,$\ldots$,?x$_m$, ?c,?m), ?m$\le$?n, ?n$\le$UB.\\
10. t$_s$(?s, ?p, ?o, ?c, ?n) $\leftarrow$ t$_s$(?s, ?p, ?o, ?c, ?m), ?m $\le$ ?n, ?n $\le$ UB .\\
11. t(?s, ?p, ?o) $\leftarrow$ t$_s$(?s, ?p, ?o, c, ?n), ?n $\le$ UB .
}
\end{center}
\caption{{\bf Additional rules that hold in every $\wp$. }}
\label{fig:transconst}
\end{figure}

\noindent
{\bf Claim 2}: $\wp$ is locally PSNHLP.\\
{\it Proof.} Let the assignment of levels to ground atoms for all predicates 
except \lp{t}, \lp{succ}, and \lp{$=$} be equal to the value of their last term. For example 
\lp{t$_s$(s, p, o, c, n)} is assigned level \lp{n}. Let predicates \lp{t}, \lp{succ}, and \lp{=}
be assigned levels \lp{UB}, $1$, and $1$, respectively. This assignment gives a local 
PSNH-stratification of $\wp$. $\qed$

We can replace the atom \lp{t$_s$(s, p, o, c, n)} by \lp{t$_{s_n}$(s,
  p, o, c)}. We can do so for other atoms with \lp{t$_s$},
\lp{active\_rule} and \lp{cond} predicate symbols, by introducing
\lp{t$_{s_n}$}, \lp{active\_rule$_n$} and \lp{cond$_n$} predicate
symbols, for all $n \le$ \lp{UB}.  Although the TS-9, TS-10 and TS-11
rules will expand O(\lp{UB}$^2$) times and the rest O(\lp{UB}) times,
changes to TSs in Figures~\ref{fig:trans} and \ref{fig:transconst} are
straightforward. Then the resulting $\wp$, say $\wp'$, is a PSNHLP as against
being just locally PSNHLP.

Let, {\it Ground}($\wp$) = $\wp_1^+ \cup \wp_1^- \cup \ldots \cup \wp_{\textrm{UB}}^+ \cup \wp_{\textrm{UB}}^-$,
be the local PSNH-stratification of $\wp$. We can show semantic equivalence, 
denoted by $\sim$, between the steps for computation of {\it PM}($\wp$) and the AIR-closure of $\Delta$ and
$\kappa$. {\bf $T \sim s$} is used to denote the direct
correspondence between extensions of predicates \lp{active\_rule} and \lp{t$_s$},
inferred after the application of \textit{T} operator during the
computation of {\it PM}($\wp$), and the rules activated and triples
asserted after completion of stage \textit{s} of \air{COMP-CLOSURE}
execution. \\

\noindent
{\bf Claim 3}: $T_{\wp_1^+}^{\omega} \sim stage_1^+$. For $i > 1$, 
$T_{\wp_i^-} \sim stage_{i-1}^-$ \textit{and} $T_{\wp_i^+}^{\omega} \sim stage_i^+$.

Let $\aleph$ be the N3 graph obtained by taking the N3 representation
of extensions of the predicate \lp{t} in {\it PM}($\wp$).\\

\noindent
{\bf Claim 4}: The AIR-closure of $\Delta$ and $\kappa$ is same as $\aleph$. \\
{\it Proof.} From claim 3 it follows that for all i $\ge$ 1, $M_i \cap \aleph$ and the triples 
in \air{FB} after the completion of $stage_i^+$ are the same. Since the fix-point 
is reached by the end of \lp{UB}$^{\textrm{th}}$ stage, $M_{UB} \cap \aleph$ 
and the triples in the AIR-closure of $\Delta$ and $\kappa$ are the same. However, 
{\it PM}($\wp$)~ =~ $M_{UB}$. $\qed$

The above results (claims 3 and 4) hold for $\wp'$ as well~\cite{KBKJDH2010}. 
We have seen that $\wp$ can be viewed as a stratified LP (PSNHLP), and
we have shown above the direct correspondence between the steps for
computing {\it PM}($\wp$) (equivalently {\it PM}($\wp'$)) and those 
for computing AIR-closure of $\Delta$ and $\kappa$. Therefore, 
complexity results for AIR follow from those for stratified programs~\cite{DEGV1997}. 
The {\bf data complexity} is the complexity of computing the model when the
rules-base is fixed and the fact-base is an input. The {\bf program
  complexity} is the complexity of computing the model when the
fact-base is fixed but the rules-base is an input.\\
\\
\noindent
{\bf Claim 5}: AIR-closure computation is PTime-complete in data-complexity and ExpTime-complete in program-complexity.

\section{AIR and Logic Programming}
\label{sec:logicprogramming}
Logic programming is a very popular declarative method of knowledge
representation and programming. Like LPs, we define rules in
AIR. However, AIR rules have different semantics from the LP rules,
and they can be nested under one another. Different nesting of the
same rules may yield (semantically) different AIR programs. In this
section we investigate logic programming through AIR.

An LP rule is said to be {\bf safe} if every variable occurring in the head of the
rule or in a negative literal in the body also occurs in a positive
literal in the body. We can encode any safe LP rule $A~ \leftarrow~ A_1,~ \ldots,~
A_n,$ ~\textit{not}($B_1$),~ $\ldots$,~ \textit{not}($B_m$) in AIR by rewriting 
it as:
\begin{quote}
\lp{$A \leftarrow A_1, \ldots, A_n,$ {\it not}(Aux) .\\
$Aux \leftarrow B_1$ .\\
$\ldots$\\
$Aux \leftarrow B_m$ .}
\end{quote}
{\it Aux} is a new predicate and its arguments are all the
variable terms that appear in the literals of the rule's body. For example following rule
: \lp{good-conn(?X, ?Y) $\leftarrow$ conn(?X, ?Y), {\it not}(infected(?X)), {\it not}(infected(?Y)).}, can be
expressed as AIR rule as shown in Figure~\ref{fig:lprule}. Note that
the predicate symbol \lp{S} is translated to \qname{:S}, and variable
symbol \lp{?S} is translated to \qname{:S}, as quantified by an
\qname{@forAll} directive. We have translated binary predicates to property
assertions, and the unary predicate to type assertion. \comment{For the
representation of general N-ary relations on the Semantic Web, there
are two popular approaches\comment{\footnote{http://www.w3.org/TR/swbp-n-aryRelations/}}:
1) Representing relations as OWL classes (i.e., reification); or 2)
using RDF lists for arguments of relations.  When a fact is deduced, a
fresh ID is required for either an instance of some OWL class or an
RDF list for assertion of the fact.  Although asserting with fresh IDs
(or blank nodes) is not supported in AIR,} Higher arity N-ary predicate 
$p(t_1, \ldots, t_n)$ can be encoded in N3 as \qname{\{( $t_1 \ldots t_n$)
  p true\}}.

\begin{figure}[t]
\begin{center}\scriptsize
\begin{tabular}{p{6.3cm} p{6.3cm}}
\parbox{6.3cm}{
\begin{tabbing}
@forAll :X, :Y .\\
:r a \= air:BeliefRule ; \\
\>     air:if \{ :X :conn :Y .\} ;\\
\>     air:then [ air:rule :b$_1$ ], [air:rule :b$_2$ ] ; \\
\>     air:then [ air:rule :r$_{Aux}$ ] . \\
\\
:r$_{Aux}$ a air:BeliefRule ; \\
\>     air:if \{ :X :aux :Y \} ; \\
\>     air:else [ air:assert \{ :X :good-conn :Y . \} ] . 
\end{tabbing} }
&
\parbox{6.3cm}{
\begin{tabbing}
:b$_1$ \= a air:BeliefRule ; \\
\>     air:if \{ :X a :Infected . \} ; \\
\>     air:then [ air:assert \{ :X :aux :Y \} ] . \\
\\
:b$_2$ \= a air:BeliefRule ; \\
\>     air:if \{ :Y a :Infected . \} ; \\
\>     air:then [ air:assert \{ :X :aux :Y \} ] .
\end{tabbing} } 
\end{tabular}
\end{center}
\caption{{\bf Rewriting an example LP rule, in AIR :} Connection between X and Y is good
if both X and Y are not infected.} 
\label{fig:lprule}
\end{figure}

\comment{
\begin{figure}
\begin{center}\footnotesize
\begin{tabular}{|p{6.5cm} p{6cm}|}
\hline
\parbox{6cm}{
\begin{tabbing}
\textit{when $m > 0$}: \\
:r a \= air:BeliefRule ; \\
\>     air:if \{ \= PRED\_IN\_N3(A$_1$) .\\
\>\>	   $\ldots$ \\
\>\>   	   PRED\_IN\_N3(A$_n$) . \} ; \\
\>     air:then [ air:rule :b$_1$ ] , $\ldots$, [air:rule :b$_m$ ] ; \\
\>     air:then [ air:rule :r$_{Aux}$ ] . \\
\\
:b$_i$ \= a air:BeliefRule ; \\
\>     air:if \{ PRED\_IN\_N3(B$_i$) . \} ; \\
\>     air\= :then  [ \\
\>\>   		air:assert \{ PRED\_IN\_N3(Aux) \} ] . \\
\\
:r$_{Aux}$ \= a air:BeliefRule ; \\
\>     air:if \{ PRED\_IN\_N3(Aux) \} ; \\
\>     air\= :else [ \\
\>\>     	air:assert \{ PRED\_IN\_N3(A) \} ] .\\
\end{tabbing}}
&
\parbox{6cm}{
\begin{tabbing}
\textit{when $m = 0$}:\\
\\
:r a \= air:BeliefRule ; \\
\>     air:if \{ \= PRED\_IN\_N3(A$_1$), \\
\>\>         $\ldots$ \\
\>\>         PRED\_IN\_N3(A$_n$) . \} ; \\
\>     air \= :then [\\ 
\>\>   		air:assert \{ PRED\_IN\_N3(A) \} ] .
\end{tabbing}}\\
\hline
\end{tabular}
\end{center}
\caption{{\bf Rewriting an LP rule in AIR.}}
\label{fig:lprule}
\end{figure}
} 

The nesting of rules impacts the order in which the rules are fired, 
and they may be nested properly to get the desired semantics. Since for 
Positive LPs (PLPs) the order in which the rules fire does not
matter, the rules in PLP can be translated into AIR and included as
top rules in an AIR program to get a semantically equivalent AIR program.
When a logic language (e.g., LP) can be encoded in AIR with unchanged semantics, 
we will say that it can be {\bf losslessly rewritten} into AIR. 

We have seen that PLPs can be 
losslessly rewritten into AIR. OWL 2 RL\footnote{http://www.w3.org/TR/owl2-profiles/\#OWL\_2\_RL}
inference rules are all positive, and therefore they can be encoded in
AIR and used concurrently with other AIR rules. Next we show that PSNHLPs
can be losslessly rewritten into AIR.\\

  \comment{Next we show that {\footnotesize PLP},
{\footnotesize PSNHLP} and {\footnotesize SPARQL} can be losslessly
rewritten into AIR. One of the advantages of encoding these in AIR is
that then we can leverage AIR justifications to better understand the
conclusions made by these programs.} 

\comment{
\noindent
{\bf Claim 6}: Positive LPs (PLPs) can be losslessly rewritten into
AIR. \\ {\it Proof.} Computation of the closure for PLPs is not
affected by the order in which rules are fired. Therefore all rules in
the PLP can be translated into AIR and included as top rules in an AIR
program. $\qed$\\

\noindent
{\bf Corollary 1}: OWL 2 RL\footnote{http://www.w3.org/TR/owl2-profiles/\#OWL\_2\_RL}
inference rules can be encoded in AIR, and used concurrently with
other AIR rules.\\}

\noindent
{\bf Claim 6}: PSNHLPs can be losslessly rewritten into AIR.\\
{\it Proof.} Let $P = P_1^+ \cup P_1^- \cup \ldots \cup P_n^+ \cup 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^{\textrm{th}}$ rule in 
stratums $P_i^+$ and $P_i^-$ be encoded in AIR with IDs \qname{:$r_{i_k}^+$}
and \qname{:$r_{i_k}^-$} respectively. Then the nesting of rules shown in 
Figure~\ref{fig:psnhlp} yields a lossless translation of $P$. This nesting 
can be generated programmatically for any PSNHLP $P$. 
\qname{owl:Thing rdfs:subClassOf owl:Nothing} is a tautologically 
false statement.

The rules in $P_{i+1}^-$ and $P_i^+$ are activated after $stage_{i-1}$. 
Since all the ground facts for predicates of level less than $\overline{i+1}$
in {\it PM}$(P)$ are inferred before $stage_i^-$, rules in $P_{i+1}^-$ 
do not fire incorrectly in $stage_i^-$. $\qed$

Since non-recursive datalogs are PSNHLPs, they can be losslessly
rewritten into AIR. The same can be said about SPARQL queries.\\

\begin{figure} [t]
\begin{center}\scriptsize
\parbox{7cm}{
\begin{tabbing}
:rs a a\= ir:RuleSet ; \\
\>      air:rule $:r_{1_1}^+, \ldots, :r_{1_{n_1}}^+$ ; \\
\>      air:rule $:r_{2_1}^-, \ldots, :r_{2_{n_2^-}}^-$ ; \\
\>      \func{GET\_RULE\_PROPERTY}(2) . \\
\\
, where \func{GET\_RULE\_PROPERTY}(j) function is defined recursively as: \\
\textit{when} \= \textit{$j < n$}:\\
\> air:ru\= le [ \\
\>\>       air:if \{ owl:Thing rdfs:subClassOf owl:Nothing . \} ; \\
\>\>       air:else [ air:rule $:r_{j_1}^+$ ], $\ldots$, [ air:rule $:r_{j_{n_j^+}}^+$ ] ; \\
\>\>       air:else [ air:rule $:r_{{j+1}_1}^-$ ], $\ldots$, [ air:rule $:r_{{j+1}_{n_{j+1}^-}}^-$ ] ; \\
\>\>       air:else [ \func{GET\_RULE\_PROPERTY}($j+1$) ] ] 
\\
\textit{when} \= \textit{$j = n$} :\\
\> air:ru\= le [ \\
\>\>       air:if \{ owl:Thing rdfs:subClassOf owl:Nothing . \} ; \\
\>\>       air:else [ air:rule $:r_{j_1}^+$ ], $\ldots$, [ air:rule $:r_{j_{n_j^+}}^+$ ] ]
\end{tabbing}}
\end{center}
\caption{{\bf Rewriting PSNHLP in AIR.}}
\label{fig:psnhlp}
\end{figure}

\comment{
\noindent
{\bf Corollary 2}: Non-recursive datalogs can be losslessly rewritten into AIR.\\}

\noindent
{\bf Claim 7}: {\small SPARQL SELECT} \textit{and} {\small CONSTRUCT} queries, 
without the query modifiers like {\small ORDER BY} and {\small LIMIT}, can be losslessly 
rewritten into AIR, and executed by the AIR reasoner.\\
{\it Proof sketch.} {\small SPARQL SELECT} \textit{and} {\small CONSTRUCT} 
queries, without the query modifiers, can be 
translated to a non-recursive Datalog, $\Pi_Q$, with NAF under the answer set semantics~\cite{P2007}. 
Using claim 6 we can say that $\Pi_Q$ can be losslessly rewritten into AIR.
\comment{{\small SPARQL CONSTRUCT} queries can similarly be lossly rewritten into AIR.} $\qed$

We have seen that PSNHLPs can be losslessly rewritten into AIR. However,
more general stratified LPs cannot be translated into AIR. For example, the
\comment{{\bf Claim 8}: Not all stratified LPs can be losslessly rewritten into AIR. \\
{\it Proof.} We prove by a counter-example. The} following rules cannot be 
losslessly rewritten into AIR for arbitrary facts of predicates P, Q, and S:\begin{quote}
P(x, z) $\leftarrow$ P(x, y), P(y, z), \textit{not}(Q(x, z)) .\\
R(x, y) $\leftarrow$ S(x, y), not(P(x, y)) . 
\end{quote}

However, that can be resolved through a simple extension of AIR, whereby \air{RuleSet}s
can be nested -- \qname{:rs$_1$ air:hasHigherPriority :rs$_2$} -- with the following meaning: 
the rules nested under \air{RuleSet} \qname{:rs$_2$} are activated only after the fixpoint 
is reached for the rules under \qname{:rs$_1$}. Note that the rules under \qname{:rs$_1$} remain active.
The corresponding change in reasoning 
algorithm is straightforward. \comment{(The \air{COMP-CLOSURE} procedure is executed first with only 
the rules under \qname{:rs$_1$} and after the fix-point is reached with the rules under \qname{:rs$_2$} 
and \qname{:rs$_1$}.)} This extension has some similarity with salience in Jess.\comment{, where 
rules are assigned priorities using integer value, and the rules are fired in order of their priorities.}\\

\noindent
{\bf Claim 8}: Stratified LPs can be losslessly rewritten into AIR extended with the nesting of \air{RuleSet}s.

\comment{{\it Proof.}  Let $P = P_1 \cup \ldots \cup P_n$ be the stratification of 
stratified LP $P$, and each $P_i$ has $n_i$ rules. Let the $k^\textrm{th}$ rule in stratum $P_i$ be 
encoded in AIR with ID \qname{:r$_{i_k}$}. Then the nesting of
rules shown in Figure~\ref{fig:stratified} yields a lossless translation. $\qed$\\

\begin{figure} [t]
\begin{center}\scriptsize
\begin{tabular}{p{6cm} p{6cm}}
\parbox{6cm}{
\begin{tabbing}
\textit{when} \textit{$i < n$}:\\
:rs$_i$ \= a air:RuleSet ; \\
\>       air:rule $:r_{i_1}, \ldots, :r_{i_{n_i}}$ ; \\
\>       air:hasHigherPriority :rs$_{i+1}$ .
\end{tabbing}} & 
\parbox{6cm}{ 
\begin{tabbing}
\textit{when} \textit{$i = n$}:\\
:rs$_i$ \= a air:RuleSet ;\\ 
\>      air:rule $:r_{i_1}, \ldots, :r_{i_{n_i}}$ .
\end{tabbing}
}
\end{tabular}
\end{center}
\caption{{\bf Rewriting Stratified LP in AIR.}}
\label{fig:stratified}
\end{figure}
%\end{quote}
}

\section{Conclusions and Future Work}
\label{sec:conclusion}

In this paper we have analyzed AIR, a rule 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 (SCR) make it sufficiently unique and
useful for Web reasoning. As AIR is a language for the Web, SCR 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. Stratified LPs can be 
encoded in AIR with an incremental modification to AIR. 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 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.

\comment{
\section*{Acknowledgements}
We would like to thank Joe Pato, Mike Speciner and other members of
the Decentralized Information Group at MIT as well as Li Ding, Jie
Bao, and the members of Tetherless Constellation Group at RPI for
their advice and contributions to this project.  This work was
supported in part by NSF Cybertrust award number 04281, IARPA award
number FA8750-07-2-0031, and AFOSR award number 6921570.  }

\bibliographystyle{abbrv}
\bibliography{paper}

%\pagebreak
\comment{
\appendix
\section{APPENDIX: Logic Program Terminologies}

We will review some standard terminologies of logic programs. A {\bf
  term} is either a variable or a constant symbol. We assume that
finite universe {\bf U} of constant symbols is given. $p(t_1, \ldots,
t_n)$ is an {\bf atom}, where $t_i$s are terms and p is an N-ary
predicate symbol. A {\bf literal} is either an atom or a negated atom,
negated using the negation as failure (NAF) operator {\bf not}. A {\bf
  normal logic program} (NLP) is a finite set of {\bf rule}s of the
form : $A \leftarrow L_1, \ldots, L_n$, where A is an atom, and $L_i$s
are literals. A and $L_1, \ldots, L_n$ are called the {\bf head} and
the {\bf body} of the rule. We prefix all variable names by '?'. By
{\bf instantiated atoms \& rules} we mean that values from U are
substituted for all variables in the atoms and rules,
respectively. 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. An LP is {\bf range
  restricted} (alternatively {\bf 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 {\bf positive logic program} (PLP)
is a NLP that has no rule with negative literals.  An LP is {\bf
  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. An LP is
{\bf locally stratified} if similar ordinal level assignments can be
made for {\it Ground}(P). A {\bf stratification} of startified LP P is
a partition of P given by : $P = P_1 \cup \ldots \cup P_n$, such that
each rule $A \leftarrow L_1, \ldots, L_m$ in P is in P$_i$ iff ordinal
level assigned to A is i. An LP is {\bf 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.  A stratified LP is locally
stratified.}

\comment{
\section{APPENDIX: T$_P$ operation $\sim$ stage of COMP\_CLOSURE}
{\bf Claim}: $T_{\wp_1^+}^{\omega} \sim stage_1^+$. For $i > 1$, $T_{\wp_i^-} \sim stage_{i-1}^-$ \textit{and} $T_{\wp_i^+}^{\omega} \sim stage_i^+$\\
Proof sketch: Semantic equivalence follows from these observations:
\begin{itemize}%{$\bullet$}
\item \lp{active\_rule} ground fact belongs to 
$T_{P_i^+}^{\omega}(M_i')$ (= $M_i$) iff corresponding rule 
instance is in \air{RB} after stage$_i^+$. 
\item \lp{t$_s$} ground fact is in M$_i$ iff corresponding triple is in 
\air{FB} after stage$_i^+$. 
\item \lp{active\_rule} ground fact belongs to $T_{P_i^-}(M_{i-1})$ (= $M_i'$)
iff corresponding rule instance is in \air{RB} after $stage_{i-1}^-$. 
\item \lp{t$_s$} ground fact is in M$_i$' iff corresponding triple is in \air{FB} 
after $stage_{i-1}^-$.
\end{itemize}
}
\comment{
\section{APPENDIX: Namespaces}
\comment{In this paper, we refer to the namespaces defined in Figure~\ref{fig:namespaces}.}
\comment{This figure must be centered -AK}
\begin{figure}
\begin{center}
\begin{VerbatimScript}
\end{VerbatimScript}
\caption{{\bf Namespaces Used}}
\label{fig:namespaces}
\end{center}
\end{figure}}

\end{document}
