Rank/Activity: A Canonical Form for Binary Resolution

Abstract. The rank/activity restriction on binary resolution is introduced. It accepts only a single derivation tree from a large equivalence class of such trees. The equivalence classes capture all trees that are the same size and differ only by reordering the resolution steps. A proof procedure that combines this restriction with the authors' minimal restriction of binary resolution computes each minimal binary resolution tree exactly once.

• Type: Conference
• Year: 1998
• Where: CADE
• Authors: Joseph Douglas Horton, Bruce Spencer
• Keywords: Binary Resolution, Binary Resolution Computes, CADE 1998, Logical Reasoning, Minimal Binary Resolution