Counting the number of equivalent binary resolution proofs

dc.contributor.authorHorton, Joseph, D.
dc.date.accessioned2023-03-01T18:28:35Z
dc.date.available2023-03-01T18:28:35Z
dc.description.abstractA binary resolution proof is represented by a binary resolution tree (brt) with clauses at the nodes and resolutions being performed at the internal nodes. A rotation in a brt can be performed on two adjacent internal nodes if the result of reversing the order of the resolutions does not affect the clause recorded at the node closer to the root. Two brt's are said to be rotationally equivalent if one can be obtained from the other by a sequence of rotations. Let c(T) be the number of brt's rotationally equivalent to T. It is shown that if T has n resolutions, all on distinct atoms, and m merges or factors between literals, then c(T) > 22n-O(m log(n)). Moreover c(T) can be as large as n! / (m + 1). A dynamic programming polynomial-time algorithm is also given to calculate c(T) if T has no merges or factors.
dc.description.copyrightCopyright © Joseph D. Horton.
dc.identifier.urihttps://unbscholar.lib.unb.ca/handle/1882/14859
dc.rightshttp://purl.org/coar/access_right/c_abf2
dc.subject.disciplineComputer Science
dc.titleCounting the number of equivalent binary resolution proofs
dc.typetechnical report

Files

Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
item.pdf
Size:
219.35 KB
Format:
Adobe Portable Document Format

Collections