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 deduction poly-tree definition descendant example factoring G contains graph G graph theory ground hence HOM(R,G homomorphic image Horn clause inference rules inference steps inference system INIT(S initial clause graph intact intersecting isomorphic KjK2 labelled Let G linear walk link removal mapped minimal deduction graph minimal refutation graph nj+j Noetherian opposite shores ordering filter p-equivalent poly-components poly-connected poly-cycle 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