| para_from_into | para_pos | paramodulate | |
| basic_paramodulation_prunes | para_instance_prunes | para_pos2 |
void paramodulation_options(BOOL ordered_inference, BOOL check_instances, BOOL positive_inference, BOOL basic_paramodulation, BOOL para_from_vars, BOOL para_into_vars, BOOL para_from_small);
int basic_paramodulation_prunes(void);How many paramodulants were killed because they failed the "basic" test.
void para_from_into(Topform from, Context cf, Topform into, Context ci, BOOL check_top, void (*proc_proc) (Topform));Paramodulate from one clause into another (non-backtrack unification version).
For oriented equality atoms, we go from left sides only and into both sides. For nonoriented equality atoms, we go from and into both sides.
int para_instance_prunes();
Topform para_pos(Topform from_clause, Ilist from_pos, Topform into_clause, Ilist into_pos);Construct a paramodulant from the given data. A fatal error occurs if it does not exist. In building the justification, the position vectors are copied.
Topform para_pos2(Topform from, Ilist from_pos, Topform into, Ilist into_pos);Construct a paramodulant from the given data. A fatal error occurs if it does not exist. In building the justification, the position vectors are copied. This is similar to para_pos(), except that it allows the into_term to be a variable.
Topform paramodulate(Literals from_lit, int from_side, Context from_subst, Topform into_clause, Ilist into_pos, Context into_subst);
/* where to paramodulate into */
typedef enum { PARA_ALL,
PARA_ALL_EXCEPT_TOP,
PARA_TOP_ONLY } Para_loc;