Spencer, BruceHorton, J., D.2023-03-012023-03-01https://unbscholar.lib.unb.ca/handle/1882/14700In a binary tree representation of a binary resolution proof, rotating some tree edge reorders two adjacent resolution steps. When rotation is not permitted to disturb factoring, and thus does not change the size of the tree, it is invertible and defines an equivalence relation on proof trees. When one resolution step is performed later than another after every sequence of such rotations, we say that resolution supports the other. For a given ordering on atoms, or on atom occurrences, a support ordered proof orders its resolution steps so that the atoms are resolved consistently with the given order without violating the support relation between nodes. Any proof, including the smallest proof tree, can be converted to a support ordered proof by rotations. For a total order, the support ordered proof is unique, up to rotation equivalence. The support ordered proof is also a rank/activity proof where atom occurrences are ranked in the given order. Procedures intermediate between ordered resolution and support ordered resolution are considered. One of these, 1-weak support ordered resolution, allows a resolution on a non-maximal literal only if it is immediately followed by both a factoring and a resolution on some greater literal. In a constrained experiment where ordered resolution solves only six of 408 TPTP problems with difficultly between 0.11 and 0.56, 1-weak support ordered resolution solves 75.http://purl.org/coar/access_right/c_abf2technical reportComputer Science