[SLP-Homepage]
[Source Modules]
[Manual]
[Run]
[Examples]
Rules
This module defines a class rule_c.
Its objects represent rules used during hyperresolution.
They consist of:
- A disjunction of literals (positive literals: atomic formulas)
in the head, which can be empty (interpreted as FALSE),
- A conjunction of literals (positive literals: atomic formulas)
in the body, which cannot be emply,
or else this would be a conditional fact, not a rule,
- A conjunction of default negations in the body,
which can be empty.
This would normally be the list of negative body literals,
but SLP allows default negations of conjunctions of atomic formulas,
so the structure is a bit more complicated.
For the hyperresolution step,
the real body is the conjunction of positive literals.
The default negations are not evaluated at this point.
Their instances are added as conditions to the resulting
conditional fact.
In addition,
the rule also contains the list of variables that appear in the rule
(the literals themselves contain only offsets,
i.e. variable numbers).
Construction:
- rule_c:
-
rule_c(rvars_t vars, rlits_t head, rlits_t body, rnegs_t cond);
This method creates a new rule_c object
from its components.
head and cond can be NIL,
but vars and body must be not NIL.
However,
the rvars_c object can state
that there are 0 variables.
Object Methods:
- get_vars:
-
rvars_t get_vars(void) const;
This method returns the list of variables
that appear in the rule.
- get_head:
-
rlits_t get_head(void) const;
This method returns the list of head literals
of the rule.
- get_body:
-
rlits_t get_body(void) const;
This method returns the list of positive body literals
of the rule.
- get_cond:
-
rnegs_t get_cond(void) const;
This method returns the set of default negations
in the body of the rule.
- print:
-
void print(rvars_t vars) const;
This method prints the rule.
Implementation:
Stefan Brass
(sbrass@sis.pitt.edu),
October 3, 2001.
[HTML 3.2 Checked]