Ancestor Reduction in Binary Resolution Trees

Simple item page
dc.contributor.authorSpencer, Bruce
dc.contributor.authorHorton, Joseph, D.
dc.date.accessioned2023-03-01T18:31:04Z
dc.date.available2023-03-01T18:31:04Z
dc.description.abstractIt is shown how the operation of ancestor reduction, found in tableaux calculi, can be applied to the resolution calculus. An efficient algorithm tells how to reorder some of the previous resolution steps in a binary resolution tree, and thus enables an additional factoring step that removes a literal from a clause. This ancestor reduction operation has a small search space, constrained by the size of the proof tree. If the additional search is successful, the new operation can eliminate literals and reduce the overall time to find a proof. A calculus is defined combining atom (literal) ordered resolution and ancestor reduction. Atom ordered resolution restricts search, but may generate large proofs for some atom orderings. This proposed theorem prover is slightly less restrictive in that an additional search for some ancestor reductions is required, but it generates smaller proof trees under many atom orderings.
dc.description.copyrightCopyright @ Bruce Spencer and Joseph D. Horton.
dc.identifier.urihttps://unbscholar.lib.unb.ca/handle/1882/15030
dc.rightshttp://purl.org/coar/access_right/c_abf2
dc.subject.disciplineComputer Science
dc.titleAncestor Reduction in Binary Resolution Trees
dc.typetechnical report

Files

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

Collections

Research Reports