“Dynamic” inferencing with generalized resolution
Gordon Beavers, Hal Berghel · 1993
keywordr: infcreocing,automatedreasoning,automated theoremproving l?hmsr!The purpose of thii paper is ~fold.Fnt, wc draw attention to the role that normal forms play in various Automated 'fheorun Proving (ATP) procedures.Second, we expand upon these procedures by introducing complementary normal forms and inferencing techniques which correspond to them.Third, we introduced a generalized form of resolution which offers an alternative to noncausal inferencing.Fwlly, we outline a 'dynamic' ATP environment which seleds from among competing inferencing mechanisms based upon 'best fit' with the probIem domain.Since this role is most easily examined in propositional logic, our discussion will be so limited.However, the procedures discussed below generalize to fmt order logic in a manner analogous to the way propositional resolution and propositional tableau P-U- do.