AIR Language Formalization
From TAMI
Contents |
Introduction
While there is explicit notion of rule ordering in AIR in form of rule-nesting, there is an implicit ordering derived from the way Negation as Failure (NAF) is handled. At any stage of reasoning when one else rule is fired, all (active and fresh!) else rules are fired in parallel. Further, a false statement (statement is not believed) can become true (statement is believed) in later rule applications, as in {if P else Q. if Q then P}.
Although AIR supports NAF and allows recursions involving negation, AIR rules always have deterministic total model. While this is achieved by the ordering in which rules are fired, there are also some restrictions on rules that can be defined in AIR. A variable occurring only in negative literals of the body can not occur in the head literal, i.e. all variables of the predicate in the head of the rule must also occur in one or more positive literals of the body.
AIR reasoning is performed in stages. In every stage some set of rules are active. During the rule applications, new predicates are inferred and nested rules are activated. Rules once active remain so through-out the reasoning process. The predicates inferred from positive rules ([ air:then air:Assertion]) are considered true in the current stage, but those inferred from negative rules ([ air:else air:Assertion]) are not considered true until the next stage. Similarly, the nested rules that are activated from positive rules ([ air:then air:Trigger-rule]) are added to the active rules set of the current stage, however, nested rules activated from negative rules become active only in the next stage.
The declarative semantics of AIR rules are defined by transforming AIR rules into LP rules. We introduce an integer argument for each predicate that captures the notion of stages described above. The translations, below, of a sample set of AIR rules exemplifies the notion.
Examples
Example 1
AIR Rules
:rule1 - if P1(x), P2(x) then Q(x) else R
:rule2 - if S1(x), S2(x) else :rule3
:rule3 - if T1(x), T2(x) then U1(x) else U2
Data
V(a).
Translation to LP
First approach. Straight forward translation
1.1. rule1-condn(x, n) <- n > 0, P1(x, n), P2(x, n) . 1.2. Q(x, n) <- rule1-condn(x, n) . 1.3. R(n + 1) <- n > 0, not rule1-condn(x, n) . 2.1. rule2-condn(x, n) <- n > 0, S1(x, n), S2(x, n) . 2.2. rule3-fired(n + 1) <- n > 0, not rule2-condn(x, n) . 3.1. rule3-condn(x, n) <- n > 0, T1(x, n), T2(x, n) . 3.2. U1(x, n) <- rule3-fired(m), m > 0, m <= n, rule3-condn(x, n) . 3.3. U2(n + 1) <- rule3-fired(m), m > 0, m <= n, not rule3-condn(x, n) . 4.1. V(a, 1) . 5.1. Q(x) <- Q(x, m), m > 0 . 5.2. R <- R(m), m > 0 . 5.3. U <- U(m), m > 0 . 5.4. V(x) <- V(x, m), m > 0 . 6.1. Q(x, n) <- Q(x, m), m < n . 6.2. R(n) <- R(m), m < n . 6.3. U1(x, n) <- U1(x, m), m < n . 6.4. U2(n) <- U2(m), m < n . 6.5. V(x, n) <- V(x, m), m < n .
NOTE: Predicates of type rule3-fired are generally of higher arity with variable arguments that are bound before :rule3 is fired.
Second approach. Stricter conditions on 'n'
Logic of rules 6.1 to 6.5 can be incorporated in rest of the rules. Consequently rules 6.1 to 6.5 are not required.
1.1. rule1-condn(x, n) <- n > 0, P1(x, m1), P2(x, m2), m1 <= n, m2 <= n . 1.2. Q(x, n) <- rule1-condn(x, n) . 1.3. R(n + 1) <- n > 0, not rule1-condn(x, n) . 2.1. rule2-condn(x, n) <- n > 0, S1(x, m1), S2(x, m2), m1 <= n, m2 <= n . 2.2. rule3-fired(n + 1) <- n > 0, not rule2-condn(x, n) . 3.1. rule3-condn(x, n) <- n > 0, T1(x, m1), T2(x, m2), m1 <= n, m2 <= n . 3.2. U1(x, n) <- rule3-fired(m), m > 0, m <= n, rule3-condn(x, n) . 3.3. U2(n + 1) <- rule3-fired(m), m > 0, m <= n, not rule3-condn(x, n) . 4.1. V(a, 1) . 5.1. Q(x) <- Q(x, m), m > 0 . 5.2. R <- R(m), m > 0 . 5.3. U <- U(m), m > 0 . 5.4. V(x) <- V(x, m), m > 0 .
Third approach. Finite number of inferred true predicates, from the LP rules
In the 1st and 2nd approaches the closure is infinite. In this approach each rule is fired successfully at-most once for a given set of arguments (arguments other than 'n'), i.e. each rule is fired only for one value of n, for fixed values of rest of the arguments.
1.1. rule1-condn(x, n) <- n > 0, P1(x, m1), P2(x, m2), m1 <= n, m2 <= n, check-if-some-equals-last(m1, m2, n) . 1.2. Q(x, n) <- rule1-condn(x, n) . 1.3. R(n + 1) <- n = 1, not rule1-condn(x, n) . 2.1. rule2-condn(x, n) <- n > 0, S1(x, m1), S2(x, m2), m1 <= n, m2 <= n, check-if-some-equals-last(m1, m2, n) . 2.2. rule3-fired(n + 1) <- n = 1, not rule2-condn(x, n) . 3.1. rule3-condn(x, n) <- n > 0, T1(x, m1), T2(x, m2), m1 <= n, m2 <= n, check-if-some-equals-last(m1, m2, n) . 3.2. U1(x, n) <- rule3-fired(m), m > 0, m <= n, rule3-condn(x, n) . 3.3. U2(n + 1) <- rule3-fired(n), not rule3-condn(x, n) . 4.1. V(a, 1) . 5.1. Q(x) <- Q(x, m), m > 0 . 5.2. R <- R(m), m > 0 . 5.3. U <- U(m), m > 0 . 5.4. V(x) <- V(x, m), m > 0 . 6.1. check-if-some-equals-last(m1, m2, n) <- m1 = n. 6.2. check-if-some-equals-last(m1, m2, n) <- m2 = n.
Example 2
AIR Rules
:rule2 - if S1(x), S2(x) else :rule3
:rule3 - if T1(x), T2(x) then :rule4 else :rule5
:rule4 - if W(x) then A(x)
:rule5 - if B(x) then C(x)
Translation to LP
Straight-forward translation
1.1. rule2-condn(x, n) <- n > 0, S1(x, n), S2(x, n) . 1.2. rule3-fired(n + 1) <- n > 0, not rule2-condn(x, n) . 2.1. rule3-condn(x, n) <- n > 0, T1(x, n), T2(x, n) . 2.2. rule4-fired(x, n) <- rule3-fired(m), m > 0, m <= n, rule3-condn(x, n) . 2.3. rule5-fired(n + 1) <- rule3-fired(m), m > 0, m <= n, not rule3-condn(x, n) . 3.1. rule4-condn(x, n) <- n > 0, W(x, n) . 3.2. A(x, n) <- rule4-fired(x, m), m > 0, m <= n, rule4-condn(x, n) . 4.1. rule5-condn(x, n) <- n > 0, B(x, n) . 4.2. C(x, n) <- rule5-fired(m), m > 0, m <= n, rule5-condn(x, n) . 5.1. A(x) <- A(x, n), n > 0 . 5.2. B(x) <- B(x, n), n > 0 .
Stricter conditions on 'n'
1.1. rule2-condn(x, n) <- n > 0, S1(x, m1), S2(x, m2), m1 <= n, m2 <= n . 1.2. rule3-fired(n + 1) <- n > 0, not rule2-condn(x, n) . 2.1. rule3-condn(x, n) <- n > 0, T1(x, m1), T2(x, m2), m1 <= n, m2 <= n . 2.2. rule4-fired(x, n) <- rule3-fired(m), m > 0, m <= n, rule3-condn(x, n) . 2.3. rule5-fired(n + 1) <- rule3-fired(m), m > 0, m <= n, not rule3-condn(x, n) . 3.1. rule4-condn(x, n) <- n > 0, W(x, m), m <= n . 3.2. A(x, n) <- rule4-fired(x, m), m > 0, m <= n, rule4-condn(x, n) . 4.1. rule5-condn(x, n) <- n > 0, B(x, m), m <= n . 4.2. C(x, n) <- rule5-fired(m), m > 0, m <= n, rule5-condn(x, n) . 5.1. A(x) <- A(x, n), n > 0 . 5.2. B(x) <- B(x, n), n > 0 .
Finite number of inferred true predicates, from the LP rules
1.1. rule2-condn(x, n) <- n > 0, S1(x, m1), S2(x, m2), m1 <= n, m2 <= n, check-if-some-equals-last(m1, m2, n) . 1.2. rule3-fired(n + 1) <- n = 1, not rule2-condn(x, n) . 2.1. rule3-condn(x, n) <- n > 0, T1(x, m1), T2(x, m2), m1 <= n, m2 <= n, check-if-some-equals-last(m1, m2, n) . 2.2. rule4-fired(x, n) <- rule3-fired(m), m > 0, m <= n, rule3-condn(x, n) . 2.3. rule5-fired(n + 1) <- rule3-fired(n), not rule3-condn(x, n) . 3.1. rule4-condn(x, n) <- n > 0, W(x, m), m <= n, check-if-some-equals-last(m, n) . 3.2. A(x, n) <- rule4-fired(x, m), m > 0, m <= n, rule4-condn(x, n) . 4.1. rule5-condn(x, n) <- n > 0, B(x, m), m <= n, check-if-some-equals-last(m, n) . 4.2. C(x, n) <- rule5-fired(m), m > 0, m <= n, rule5-condn(x, n) . 5.1. A(x) <- A(x, n), n > 0 . 5.2. B(x) <- B(x, n), n > 0 . 6.1. check-if-some-equals-last(m, n) <- m = n . 6.2. check-if-some-equals-last(m1, m2, n) <- m1 = n . 6.3. check-if-some-equals-last(m1, m2, n) <- m2 = n .
