Sciweavers

CADE
1998
Springer

Rank/Activity: A Canonical Form for Binary Resolution

14 years 2 months ago
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.
Joseph Douglas Horton, Bruce Spencer
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 1998
Where CADE
Authors Joseph Douglas Horton, Bruce Spencer
Comments (0)