Skip to content

reify-defined-metasp.lp

Adds defined directives for the reification predicates that are added by metasp to simplify the semantics.

Predicate Summary

Name Definition Type
formula/2

Represents that F is a formula of type T

show/0

This fact is included if `#show

show_atom/2

Represents that the atom S should be shown if the condition B is satisfied

show_term/2

Represents that the term S should be shown if the condition B is satisfied


Glossary

formula(F, T)

Represents that F is a formula of type T. This predicate is generated for every sub-formula found in the input. The type can be any of the base type or one defined in the grammar. A formula might have multiple types.

Parameter Description
F

The symbol representing the formula. It is generated by clingo and corresponds to the literal number of the formula.

T

The type of the formula.


show()

This fact is included if #show. was present in the original input. Meaning that all atoms should be hidden unless explicitly shown.


show_atom(S, B)

Represents that the atom S should be shown if the condition B is satisfied. Comes from a show p/N. statement in the original input.

Parameter Description
S

The symbol to show

B

The condition literal that must be satisfied for S to be shown. It is a conjunction of formulas.


show_term(S, B)

Represents that the term S should be shown if the condition B is satisfied. Comes from a show S:X. statement in the original input.

Parameter Description
S

The term to show

B

The condition literal that must be satisfied for S to be shown. Corresponds to the satisfaction of the conjunction of formulas X.