Courteous Logic Programs: Priorized Conflict Handling for Rules

by Benjamin N. Grosof IBM Research Report RC 20836

May 8, 1997; revised Dec. 30, 1997

Presented by Stuart C. Shapiro

Department of Computer Science and Engineering April 25, 2002

⟹ Grosof p. 40

My Motivation

Penguins swimming shadows birds flying by inheritance rules in OO programs. But what is the declarative (logical) situation?

Default Logic

\frac{Bird(x) : F lies(x)}{F lies(x)}

Penguin(x) ⇒ Swims(x)

Swims(x) ⇒ ¬Flies(x)

Default rules have a different syntax from “normal” rules, and are even part of the object language.

Basic Idea Grosof: Courteous Logic Programs

In OO hierarchy, Penguins swim overrides or precludes Birds fly.

Why not an Overrides or Precludes meta-predicate that takes “normal” rules?

⟹ Grosof p. 45 Courteous LP Version of Hierarchy

⟨Brd⟩ F ly(x) ← Bird(x).

Bird(x) ← Canary(x). Bird(x) ← P enguin(x).

⟨P eng⟩ ¬F ly(x) ← P enguin(x).

Canary(T weety) ← . P enguin(Opus) ← .

Overrides(P eng, Brd) ← .

⇒  F ly(T weety).
⇒  ¬F ly(Opus).

Courteous LP uses Skeptical Reasoning ⟹ Grosof p. 47

CLP Restrictions

The ground-atom dependency graph of a CLP must be acyclic (no recursion). Overrides atoms are not allowed in the body of any rule, only in positive ground facts. I.e., of the form Overrides(i, j ) ←. where i and j are labels. This is called a prioritization fact. Prioritization facts must form a strict partial order (transitive, antisymmetric, irreflexive) of the labels. A prioritization fact may have a label, but it will be ignored. In the fact Overrides(i, j ) ←., i and j may label rules whose heads have different predicates, but such a fact will be ignored.

Incorrect CLP Version of Hierarchy

¬F ly(x) ← Swim(x).

¬Swim(x) ← F ly(x).  not acyclic
⟨Brd⟩ F ly(x) ← Bird(x).

Bird(x) ← Canary(x). Bird(x) ← P enguin(x).

⟨P eng⟩ Swim(x) ← P enguin(x).

Canary(T weety) ← . P enguin(Opus) ← .

Overrides(P eng, Brd) ← . different heads

Operational Example ⟹ Grosof p. 51

Program w ← ¬u ∧ ∼ p. ¬u ← s ∧ ¬t ∧ ∼ v. q ← p. r ← ¬p. s ← . ¬t ← . p ← . ¬p ← .

As Dependency DAG

w ←¬u ∧ ∼ p.

¬u ← s∧¬t ∧ ∼ v. s ← . ¬t ← .

r ← ¬p. q ← p.

p ← . ¬p ← .

Program as Dependency DAG

w ←¬u ∧ ∼ p.

¬u ← s∧¬t ∧ ∼ v.

s ← .
¬t ← .

r ← ¬p. q ← p.

p ← .

¬p ← .

Sequenced (topologically sorted) & Stratified p ← . ¬p ← . q ← p. r ← ¬p. s ← . ¬t ← . ¬u ← s ∧ ¬t ∧ ∼ v. w ← ¬u ∧ ∼ p.

Finding the Answer Set

AnswerSet

p ← . ¬p ← . q ← p. r ← ¬p. s ← . ¬t ← . ¬u ← s ∧ ¬t ∧ ∼ v. w ← ¬u ∧ ∼ p.

Finding the Answer Set

AnswerSet

p ← .

¬p ← .  0̸

q ← p. r ← ¬p. s ← . ¬t ← . ¬u ← s ∧ ¬t ∧ ∼ v. w ← ¬u ∧ ∼ p.

Finding the Answer Set

AnswerSet

p ← .

¬p ← .  0̸
q ← p.  0̸

r ← ¬p. s ← . ¬t ← . ¬u ← s ∧ ¬t ∧ ∼ v. w ← ¬u ∧ ∼ p.

Finding the Answer Set

AnswerSet

p ← .

¬p ← .  0̸
q ← p.  0̸
r ← ¬p.  0̸

s ← . ¬t ← . ¬u ← s ∧ ¬t ∧ ∼ v. w ← ¬u ∧ ∼ p.

Finding the Answer Set

AnswerSet

p ← .

¬p ← .  0̸
q ← p.  0̸
r ← ¬p.  0̸
s ← .  s

¬t ← . ¬u ← s ∧ ¬t ∧ ∼ v. w ← ¬u ∧ ∼ p.

Finding the Answer Set

AnswerSet

p ← .

¬p ← .  0̸
q ← p.  0̸
r ← ¬p.  0̸
s ← .  s
¬t ← .  ¬t

¬u ← s ∧ ¬t ∧ ∼ v. w ← ¬u ∧ ∼ p.

Finding the Answer Set

AnswerSet

p ← .

¬p ← .  0̸
q ← p.  0̸
r ← ¬p.  0̸
s ← .  s
¬t ← .  ¬t
¬u ← s ∧ ¬t ∧ ∼ v. ¬u

w ← ¬u ∧ ∼ p.

Finding the Answer Set

AnswerSet

p ← .

¬p ← .  0̸
q ← p.  0̸
r ← ¬p.  0̸
s ← .  s
¬t ← .  ¬t
¬u ← s ∧ ¬t ∧ ∼ v. ¬u
w ← ¬u ∧ ∼ p.  w

Finding the Hierarchy Answer Set

AnswerSet

Overrides(P, B) ← . Canary(T) ← . P enguin(O) ← . Bird(T) ← Canary(T). Bird(T) ← P enguin(T). Bird(O) ← Canary(O). Bird(O) ← P enguin(O).

⟨B⟩ F ly(T) ← Bird(T).
⟨P ⟩ ¬F ly(T) ← P enguin(T).
⟨B⟩ F ly(O) ← Bird(O).
⟨P ⟩ ¬F ly(O) ← P enguin(O).

Finding the Hierarchy Answer Set

AnswerSet

Overrides(P, B) ← .  Overrides(P, B)

Canary(T) ← . P enguin(O) ← . Bird(T) ← Canary(T). Bird(T) ← P enguin(T). Bird(O) ← Canary(O). Bird(O) ← P enguin(O).

⟨B⟩ F ly(T) ← Bird(T).
⟨P ⟩ ¬F ly(T) ← P enguin(T).
⟨B⟩ F ly(O) ← Bird(O).
⟨P ⟩ ¬F ly(O) ← P enguin(O).

Finding the Hierarchy Answer Set

AnswerSet

Overrides(P, B) ← .  Overrides(P, B)
Canary(T) ← .  Canary(T)

P enguin(O) ← . Bird(T) ← Canary(T). Bird(T) ← P enguin(T). Bird(O) ← Canary(O). Bird(O) ← P enguin(O).

⟨B⟩ F ly(T) ← Bird(T).
⟨P ⟩ ¬F ly(T) ← P enguin(T).
⟨B⟩ F ly(O) ← Bird(O).
⟨P ⟩ ¬F ly(O) ← P enguin(O).

Finding the Hierarchy Answer Set

AnswerSet

Overrides(P, B) ← .  Overrides(P, B)
Canary(T) ← .  Canary(T)
P enguin(O) ← .  P enguin(O)

Bird(T) ← Canary(T). Bird(T) ← P enguin(T). Bird(O) ← Canary(O). Bird(O) ← P enguin(O).

⟨B⟩ F ly(T) ← Bird(T).
⟨P ⟩ ¬F ly(T) ← P enguin(T).
⟨B⟩ F ly(O) ← Bird(O).
⟨P ⟩ ¬F ly(O) ← P enguin(O).

Finding the Hierarchy Answer Set

AnswerSet

Overrides(P, B) ← .  Overrides(P, B)
Canary(T) ← .  Canary(T)
P enguin(O) ← .  P enguin(O)

Bird(T) ← Canary(T).

Bird(T) ← P enguin(T). Bird(T)

Bird(O) ← Canary(O). Bird(O) ← P enguin(O).

⟨B⟩ F ly(T) ← Bird(T).
⟨P ⟩ ¬F ly(T) ← P enguin(T).
⟨B⟩ F ly(O) ← Bird(O).
⟨P ⟩ ¬F ly(O) ← P enguin(O).

Finding the Hierarchy Answer Set

AnswerSet

Overrides(P, B) ← .  Overrides(P, B)
Canary(T) ← .  Canary(T)
P enguin(O) ← .  P enguin(O)

Bird(T) ← Canary(T).

Bird(T) ← P enguin(T). Bird(T)

Bird(O) ← Canary(O).

Bird(O) ← P enguin(O). Bird(O)
⟨B⟩ F ly(T) ← Bird(T).
⟨P ⟩ ¬F ly(T) ← P enguin(T).
⟨B⟩ F ly(O) ← Bird(O).
⟨P ⟩ ¬F ly(O) ← P enguin(O).

Finding the Hierarchy Answer Set

AnswerSet

Overrides(P, B) ← .  Overrides(P, B)
Canary(T) ← .  Canary(T)
P enguin(O) ← .  P enguin(O)

Bird(T) ← Canary(T).

Bird(T) ← P enguin(T). Bird(T)

Bird(O) ← Canary(O).

Bird(O) ← P enguin(O). Bird(O)
⟨B⟩ F ly(T) ← Bird(T).
⟨P ⟩ ¬F ly(T) ← P enguin(T). F ly(T)
⟨B⟩ F ly(O) ← Bird(O).
⟨P ⟩ ¬F ly(O) ← P enguin(O).

Finding the Hierarchy Answer Set

AnswerSet

Overrides(P, B) ← .  Overrides(P, B)
Canary(T) ← .  Canary(T)
P enguin(O) ← .  P enguin(O)

Bird(T) ← Canary(T).

Bird(T) ← P enguin(T). Bird(T)

Bird(O) ← Canary(O).

Bird(O) ← P enguin(O). Bird(O)
⟨B⟩ F ly(T) ← Bird(T).
⟨P ⟩ ¬F ly(T) ← P enguin(T). F ly(T)
⟨B⟩ F ly(O) ← Bird(O).
⟨P ⟩ ¬F ly(O) ← P enguin(O). ¬F ly(O)

Formal Constructive Definition of Answer Set Let ρ be total (ground) atom stratification of CLP, s.t. prioritization atoms come first. Let p_{i} be i^{th} atom in ρ. Answer set S: S_{0} =0̸ S_{i} = ⋃_{j=1,...,i} T_{j} i ≥ 1 S = ⋃_{i} T_{i} T_{i} = {σp_{i} | Cand_{i}^{σ} ≠0̸ ,

∀k ∈ Cand_{i}^{¬σ}

. ∃j ∈ Cand_{i}^{σ}
. S_{i−1} ⊧ Overrides(j, k)}

Cand_{i}^{σ} = {j | labels(j, r) , Head(r) = σp_{i} ,

S_{i−1} ⊧ Body(r)}

σ is classical sign, either + or - (¬).

[Grosof, p 6–7] Some Results

⟹ Grosof p. 52 CLP Gets Effect of CWA Overrides(sched, cwa)

⟨cwa⟩ ¬flight(S, D, T, A)
⟨sched⟩ flight(miami, detroit, 10am, elysian air) ←
⟨sched⟩ flight(jfk, new orleans, 4am, fountain air) ←
⟨sched⟩ flight(dallas, seattle, 7am, middle air) ←

[Grosof, p. 22]

Preservation in Parallel Merging For example & problem ⟹ Grosof p. 54 CLP solution:

AnswerSet

Overrides(1, 2) ← .

Overrides(4, 3) ← .
⟨1⟩ a ← .
⟨2⟩ b ← .
⟨3⟩ c ← .
⟨4⟩ d ← .
⟨1⟩ p ← a.
⟨4⟩ p ← d.
⟨2⟩ ¬p ← b.
⟨3⟩ ¬p ← c.

Preservation in Parallel Merging For example & problem ⟹ Grosof p. 54 CLP solution:

AnswerSet

Overrides(1, 2) ← . Overrides(1, 2)
Overrides(4, 3) ← . Overrides(4, 3)
⟨1⟩ a ← .
⟨2⟩ b ← .
⟨3⟩ c ← .
⟨4⟩ d ← .
⟨1⟩ p ← a.
⟨4⟩ p ← d.
⟨2⟩ ¬p ← b.
⟨3⟩ ¬p ← c.

Preservation in Parallel Merging For example & problem ⟹ Grosof p. 54 CLP solution:

AnswerSet

Overrides(1, 2) ← . Overrides(1, 2)
Overrides(4, 3) ← . Overrides(4, 3)
⟨1⟩ a ← .  a
⟨2⟩ b ← .  b
⟨3⟩ c ← .  c
⟨4⟩ d ← .  d
⟨1⟩ p ← a.
⟨4⟩ p ← d.
⟨2⟩ ¬p ← b.
⟨3⟩ ¬p ← c.

Preservation in Parallel Merging For example & problem ⟹ Grosof p. 54 CLP solution:

AnswerSet

Overrides(1, 2) ← . Overrides(1, 2)
Overrides(4, 3) ← . Overrides(4, 3)
⟨1⟩ a ← .  a
⟨2⟩ b ← .  b
⟨3⟩ c ← .  c
⟨4⟩ d ← .  d
⟨1⟩ p ← a.
⟨4⟩ p ← d.
⟨2⟩ ¬p ← b.
⟨3⟩ ¬p ← c.  p

Adding Prioritized Conflict Handling to SNePS 2.5

A M.S. thesis project by Bharat Bhushan under the supervision of Stuart C. Shapiro.

SNePS 2.5 is a product of the SNePS Research Group.

SNePS 2.5 Basics

A hypothesis is a proposition asserted to SNePS by the user. A context is a set of hypotheses. There is always a current context, CC. Every proposition, p has a set of origin sets, os(p). An origin set is a set of hypotheses. A proposition, p is asserted in a context, c iff

∃s ∈ os(p)[∀h ∈ s[h ∈ c]] Modifications for Prioritized Conflict Handling

A proposition, p, is derivable in a context, c (Derivable(p, c)), iff

∃s ∈ os(p)[∀h ∈ s[h ∈ c]]

There is a special predicate Precludes(p1 , p2 ) that may hold between two propositions. Precludes predicates may be included in rules, like other predicates.

A proposition, p is asserted in a context, c (Asserted(p, c)), iff

Derivable(p, c)

∧[¬Derivable(¬p, c)

∨Asserted(P recludes(p, ¬p), c)
∨[∃s ∈ os(p)
¬∃s′ ∈ os(¬p)
(∃h ∈ s(∃h′ ∈ s′
Asserted(P recludes(h′, h), c)))]]

A proposition, p, is asserted iff it is asserted in CC.