Lines Matching defs:literal
64 type literal = bool * term;
65 datatype clause = CLAUSE of vars * literal list;
70 vars * literal -> (substitution * vars * literal list * rule) list;
436 val res1 = (pos, rw tm) : literal
874 val _ = assert pos (ERR "pos_resolution_rule" "not a positive literal")
889 assert (not pos) (ERR "neg_resolution_rule" "not a negative literal")
1013 val _ = assert (not pos) (ERR "equality_lrule" "positive literal")
1067 (BUG "paramodulation" "literal length check failed")
1171 type state = literal list * (substitution * fact);