This module defines a class hyper_c. It has no instances, only static member functions (class methods) that implement the hyperresolution method for deriving implied conditional facts.
For instance,
if a rule is
p | q <- r & s not a
and there are conditional facts for the two body literals
r <- not b & not c,
t | s | u <.,
p | q | | t | u
<-
not a & not b & not c .
So for each positive body literal,
there must be a conditional fact
that has a matching head literal.
The remaining head literals and the head literals of the rule
form the head of the resulting conditional fact.
The condition consists of the conditions in the rule
plus the conditions of the conditional facts that were resolved
with the body literals.
Of course, the same also works with variables. The allowedness/safety/range restriction condition requires that all variables of the rule appear in positive body literals. Then the variables get instantiated when the positive body literals are matched with conditional facts (that are already ground).
Besides doing the hyperresolution, this module also manages the set of rules that are used for the hyperresolution.
static void store(rule_t rule);static void print_rules(void);static void compute_implied(void);