up | previous | next | detailed contents | brief contents

Reflexive property of equality

The reflexive axiom for equality must be present in order to get refutations using paramodulation.
list(usable).
x=x.
end_of_list.

up | previous | next | detailed contents | brief contents