What people are saying - Write a review
We haven't found any reviews in the usual places.
Properties of Clause Graph Resolution
6 other sections not shown
Other editions - View all
A-ancestor atoms belongs bijection clause graph homomorphism clause graph lemma clause graph resolution clause set resolution complete and refutation contains the homomorphic control strategies copy rule definition descendant example factoring G contains graph G graph theory ground hence HOM(R,G homomorphic image homomorphically embedded Induction step inference rules inference steps inference system INIT(S initial clause graph intact intersecting isomorphic labelled Let G linear walk link removal mapped merging rule minimal deduction graph minimal refutation graph nj+1 Noetherian opposite shores ordering filter p-equivalent parent clause poly-components poly-connected poly-cycle poly-trail joining polylink compatible proof properties pure literal nodes R-pure R-purity R2-link refutation complete refutation confluent refutation poly-tree refutation tree resolution step resolution tree resolvent restriction filter rm-size s-linear set-of-support shore nodes singleton shore Slu-links strictly unit refutable subgraph of G subset subsumed subsumption tautology link condition theorem unit clause node unit refutable class unsatisfiable variable variant weakly unifiable