| org.mandarax.kernel.SelectionPolicy
All known Subclasses: org.mandarax.reference.RightMostSelectionPolicy, org.mandarax.reference.DefaultSelectionPolicy, org.mandarax.reference.StrictSelectionPolicy, org.mandarax.reference.LeftMostSelectionPolicy,
| SelectionPolicy | | public interface SelectionPolicy (Code) | | Interface for strategies defining the order of literals that is used by
the inference engine when it attempts to unify the literals with a clause.
author:
Jens Dietrich
version:
3.4 <7 March 05>
since:
1.1 |
| Method Summary | |
| int[] | getOrderedPositions(Clause goal, Clause appliedClause)
Return an array of integers specifying in which order the inference engine
should attempt to unify the literals with the candidate.
The order of clauses matters, this order may have an important impact on performance of a proof!
E.g., if {A,B,C} is a goal (all symbols represent negative literals),
then a left most selection rule would mean that we first try to unify A with
appliedClaue, then B and finally C. |
| getOrderedPositions | | int[] getOrderedPositions(Clause goal, Clause appliedClause)(Code) | | Return an array of integers specifying in which order the inference engine
should attempt to unify the literals with the candidate.
The order of clauses matters, this order may have an important impact on performance of a proof!
E.g., if {A,B,C} is a goal (all symbols represent negative literals),
then a left most selection rule would mean that we first try to unify A with
appliedClaue, then B and finally C. The array returned should then be {0,1,2}.
int[] the positions
Parameters:
goal - the goal
Parameters:
appliedClause - the clause that should be used to prove the goal |
|
|