Setup¶

The setup is constructed from the reification of a tagged program and contains all the information needed to find the explanations (foils).

Program graph¶

The basis of every explanation is the program graph, a directed graph that fully encodes a ground logic program. It contains a node for every atom and every rule of the program:

Atom nodes represent the atoms of the program.
Rule nodes represent the rules and are typed as either choice or disjunction rules. Facts and integrity constraints are special cases of disjunctive rules.

The edges connect rules with the atoms they depend on and derive:

An edge from an atom to a rule means the atom appears in the rule's body. The edge is positive for positive body literals and negative for negative ones (not a).
An edge from a rule to an atom means the atom appears in the rule's head.

As a consequence, facts appear as rule nodes without incoming edges, while integrity constraints appear as rule nodes without outgoing edges.

Reference program vs foil program¶

To use the same program graph for both the reference and foil program, the setup construction uses a single program graph that contains all rules and atoms of both programs. The membership of each rule and atom in the reference and foil program is encoded via predicate program(R, W), where R is a rule and W is either ref or foil. For the setup we only use ref and foil is introduced later during foil finding.

Removable and addable rules¶

The setup construction also identifies the rules that can be removed from the reference program and those that can be added to it. This is indicated via predicate optional(C, R), where C is either add or remove and R is a rule. Those atoms are extracted from the tagged program and are used to generate the set of candidate foils during foil finding.

Query¶

The query (set of literals) is represented as a set of atoms with their expected truth value, which is indicated via predicate query(A, V), where A is an atom and V is either 1 (true) or 0 (false).

Implementation¶

In the implementation the setup is generated using the reification of a tagged program.

Predicate Summary ¶

Name	Definition	Type
`atom_tuple/2`
`literal_tuple/2`
`rule/2`
`show/0`
`show_atom/2`
`show_term/2`
`symbol_literal/2`
`edge/2`
`node/2`
`optional/2`
`program/2`
`tag/2`
`error/1`
`label/2`
`original_tag/1`
`show/2`

Encodings ¶

`reify-to-pg.lp` ¶

Encoding

#script (python)
from clingo import Number
ids = {}
def label(rule):
    if str(rule) in ids:
        n= ids[str(rule)]
    else:
        id = len(ids) + 1
        ids[str(rule)] = id
        n = id
    return Number(n)
#end.

Error occurs when a sum is encountered in the input (unsupported)

error("Sum not supported") :- rule(H,sum(B)).

Gather all rules and atoms

label(rule(H,B), @label(rule(H,B))) :- rule(H,B).

label(rule(H,B), ID) :- tag(rule(H,B),rule_id(ID)). % <-------- HACK just for the paper

node(A,atom) :- symbol_literal(A,L).
node(R,rule(disjunction)) :- label(rule(disjunction(H),B), R).
node(R,rule(choice)) :- label(rule(choice(H),B), R).

Gather all edges

edge((A, R),1):-
    label(rule(H, normal(B)), R),
    literal_tuple(B,E), E>0, symbol_literal(A,E).
edge((A, R),0):-
    label(rule(H, normal(B)), R),
    literal_tuple(B,E), E<0, symbol_literal(A,-E).
edge((R, A),1):-
    label(rule(disjunction(H), B), R),
    atom_tuple(H,E), symbol_literal(A,E).
edge((R, A),1):-
    label(rule(choice(H), B), R),
    atom_tuple(H,E), symbol_literal(A,E).
#show node/2.
#show edge/2.

Program membership for reference

program(N, ref):-node(N,_), not optional(add, N).
#show program/2.

Tags into reference graph

original_tag(tag(rule(H,B),T)):-tag(rule(H,B),T).
original_tag(tag(atom(E),T)):-tag(atom(E),T).
tag(R,T):-tag(rule(H,B),T), label(rule(H,B),R).
tag(A,T):-tag(atom(E),T), symbol_literal(A,E).

Tag comes from dynamic tags asplain_tag(X,T):-tag(X,T), not original_tag(tag(X,T)).

#show tag(N,T): tag(N,T), not original_tag(tag(N,T)).

Optional to remove

optional(remove, R):-tag(R, removable), not original_tag(tag(R,removable)).

For now dynamic tags are not added here optional(remove, rule(disjunction(H),B)):- tag(G, rule(disjunction(H),B),fact), %is a fact removable_if_fact(A), %flagged as removable if A atom_tuple(H,E), %the head atom is A symbol_literal(A,E). Optional to add also includes the edges that would be added

optional(add, R):-tag(R, addable), not original_tag(tag(R,addable)).
#show optional/2.
#include "utils-tags.lp".

`utils-tags.lp` ¶

Encoding

Extra tags Note that it uses the original tag/2 and the the other file is the one that creates the asplain_tag/2

tag(rule(disjunction(H),B), constraint):- rule(disjunction(H),B), not atom_tuple(H,_).
tag(rule(disjunction(H),normal(B)), fact):- rule(disjunction(H),normal(B)),
    #count{E:atom_tuple(H,E)}=1,
    not literal_tuple(B,_).

Labels without vars

tag(R, label(L,())):-tag(R, label(L)).
show(A,L):-show_atom(A,L).
show(A,L):-show_term(A,L).
tag(atom(E), shown):- show(A,L), symbol_literal(A,E).

Show all explicit

tag(atom(E), shown):-symbol_literal(A,E), not show, not show_atom(_,_).

Show all unless hide or show signature

#defined show_atom/2.
#defined show_term/2.
#defined show/0.