set(para_ones_rule). set(para_into_units_only). % has been quite useful set(para_from_units_only). set(interactive_given). set(knuth_bendix). assign(max_literals,2). set(hyper_res). set(neg_hyper_res). include(demodulators). include(equadulators).
demodulators was usually included when proving the basic properties of a new definition. It consists of all axioms of TRC that would be considered as reduction rules in combinatory logic. They are as follows. All of them are placed in the demodulators list. The inclusion of these demodulators causes OTTER to perform long chains of reductions in a single proof step, but the proof steps remain easy to verify with the help of a pencil and paper.a(k(x),y) = x. a(p1,pair(x,y)) = x. a(p2,pair(x,y)) = y. a(pair(x,y),z) = pair(a(x,z),a(y,z)). pair(a(p1,x),a(p2,x)) = x. a(a(a(abst,x),y),z) = a(a(x,k(z)),a(y,z)). a(eq,pair(x,x)) = p1.
equadulators came in to play only once. In OTTER, not only terms but also literals (atomic clauses) can be rewritten using demodulators. I called the following equadulators, for equality demodulators. Its contents, in the demodulators list, are as follows:(k(x) = k(y)) = (x = y). (pair(x,y) = pair(x,z)) = (y = z). (pair(x,z) = pair(y,z)) = (x = y). (a(eq,pair(x,y)) = p1) = (x = y).
up | previous | next | detailed contents | brief contents