meta-time.lp

Adds a time argument to the meta predicates in meta.lp. It can be used instead of meta.lp when the encoding requires time support.

Encodings

meta-time.lp

Source

% Adds a time step argument to the normal meta encoding.

%*! time(T)

Represents the time steps in the temporal logic that are between 0 and `horizon`.

Args:
    - T: Numerical identifier for the time step.
*%

time(0..n).

%*! conjunction(B, T)

The set of literals in the conjunction identified by `B` holds since all literals are true or false as specified.

Args:
    - B: Numerical identifier unique within its class.
    - T: Numerical identifier for the time step where the conjunction holds.
*%

conjunction(B,T) :- literal_tuple(B), time(T),
        hold(L,T) : literal_tuple(B, L), L > 0;
    not hold(L,T) : literal_tuple(B,-L), L > 0.

%*! body(BODY, T)

The body used in a rule as `BODY` is true at step `T`.

Args:
        - BODY: One of the following
            `normal(B)`: Normal body with literals (The conjunction of literals is true).
            `sum(B, G)`: Sum body with literals and a threshold (The sum of weights satisfies the upper lower bound).
        - T: Numerical identifier for the time step where the body holds.
*%

body(normal(B),T) :- rule(_,normal(B)), conjunction(B,T), time(T).
body(sum(B,G),T)  :- rule(_,sum(B,G)), time(T),
    #sum { W,L :     hold(L,T), weighted_literal_tuple(B, L,W), L > 0 ;
           W,L : not hold(L,T), weighted_literal_tuple(B,-L,W), L > 0 } >= G.

%*! hold(A, T)

The atom `A` holds at time step `T`.

Args:
    - A: Numerical identifier of the atom.
    - T: Numerical identifier for the time step where the atom holds.
*%

  hold(A,T) : atom_tuple(H,A)   :- rule(disjunction(H),B), body(B,T), time(T).
{ hold(A,T) : atom_tuple(H,A) } :- rule(     choice(H),B), body(B,T), time(T).

%*! true(O, T)

The output `O` is true at time step `T`. It is equivalent to `hold/2`, but this predicate uses the atom and not the literal number.
Therefore it can be used and derived in the semantics encoding to define truth of formulas that use types in the grammar.

Args:
    - O: Value to be output.
    - T: Numerical identifier for the time step where the output is true.
*%



% True if the literal tuple for the output holds
true(O,T) :- output(O,B), time(T), hold(L,T) : literal_tuple(B,L).
% If a formula its true, its literal holds
hold(L,T) :- output(O,B), time(T), true(O,T),  literal_tuple(B,L).

Encoding

Adds a time step argument to the normal meta encoding.

time(0..n).
conjunction(B,T) :- literal_tuple(B), time(T),
        hold(L,T) : literal_tuple(B, L), L > 0;
    not hold(L,T) : literal_tuple(B,-L), L > 0.
body(normal(B),T) :- rule(_,normal(B)), conjunction(B,T), time(T).
body(sum(B,G),T)  :- rule(_,sum(B,G)), time(T),
    #sum { W,L :     hold(L,T), weighted_literal_tuple(B, L,W), L > 0 ;
           W,L : not hold(L,T), weighted_literal_tuple(B,-L,W), L > 0 } >= G.
hold(A,T) : atom_tuple(H,A)   :- rule(disjunction(H),B), body(B,T), time(T).
{ hold(A,T) : atom_tuple(H,A) } :- rule(     choice(H),B), body(B,T), time(T).

True if the literal tuple for the output holds

true(O,T) :- output(O,B), time(T), hold(L,T) : literal_tuple(B,L).

If a formula its true, its literal holds

hold(L,T) :- output(O,B), time(T), true(O,T),  literal_tuple(B,L).

---

Glossary

body(BODY, T)

The body used in a rule as BODY is true at step T.

Parameter	Description
BODY	One of the following normal(B): Normal body with literals (The conjunction of literals is true). sum(B, G): Sum body with literals and a threshold (The sum of weights satisfies the upper lower bound).
T	Numerical identifier for the time step where the body holds.

conjunction(B, T)

The set of literals in the conjunction identified by B holds since all literals are true or false as specified.

Parameter	Description
B	Numerical identifier unique within its class.
T	Numerical identifier for the time step where the conjunction holds.

hold(A, T)

The atom A holds at time step T.

Parameter	Description
A	Numerical identifier of the atom.
T	Numerical identifier for the time step where the atom holds.

time(T)

Represents the time steps in the temporal logic that are between 0 and horizon.

Parameter	Description
T	Numerical identifier for the time step.

true(O, T)

The output O is true at time step T. It is equivalent to hold/2, but this predicate uses the atom and not the literal number. Therefore it can be used and derived in the semantics encoding to define truth of formulas that use types in the grammar.

Parameter	Description
O	Value to be output.
T	Numerical identifier for the time step where the output is true.