start | find | index | login or register | edit | ||
Resolution
by earl, 6936 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 L ⊆ C, M ⊆ D are two singletons (unit sets) whose respective members form a complementary pair, then the ground clause: (C − L) ∪ (D − M) is called a ground resolvent of C and D." |
search 4 active users
backlinks (more) recent stores (more) echo earlZstrainYat|tr ZY @. |
|
earl.strain.at • esa3 • online for 8701 days • c'est un vanilla site |