start | find | index | login or register | edit
by earl, 5683 days ago
From Alan Robinson's original text describing the resolution principle:

"2.19 Ground resolvents. If C and D are two ground clauses, and LC, MD are two singletons (unit sets) whose respective members form a complementary pair, then the ground clause: (CL) ∪ (DM) is called a ground resolvent of C and D."

Robinson, J. A. (1965), 'A Machine-Oriented Logic Based on the Resolution Principle', Journal of the ACM (JACM), v.12 n.1, p.26
powered by vanilla
echo earlZstrainYat|tr ZY @. • esa3 • online for 7448 days • c'est un vanilla site