Represents the set of atoms in the heads of clauses and in the bodies (formulas) of clauses.
Tracks proven atoms in the reverse order they were proved.
Applies known facts to
clauses, deriving a new, possibly empty list of clauses.
Computes the set of all atoms in
Computes the atoms in the heads and bodies of the clauses in
Computes the set of atoms in
clauses that directly or transitively take a negated atom as input.
Computes the variables in the unique stable model for the program represented by
Derives the formula that results from substituting