Obvious logical inferences
Martin D. Davis · 1981
A precise definition is given of a class of inferences in predicate logic which it la proposed to Identify with the class of "obvious " Inferences. A mechanism for Implementing "obvious inference " as a rule of Inference in proof checking systems is discussed. I.