Rank/activity: A canonical form for binary resolution

DOI10.1007/BFB0054275MaRDI QIDQ4249905zbMATH OpenFDO

Authors J. D. Horton, Bruce D. Spencer

Publication date 15 September 1999

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0054275

zbMATH Keywords

automated theorem provingbinary resolutionrank/activity restrictionresolution tree

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Counting the number of equivalent binary resolution proofs
• scientific article; zbMATH DE number 4072434
• Efficient algorithms to detect and restore minimality, an extension of the regular restriction of resolution
• Support ordered resolution

Cited in

(4)

• Efficient algorithms to detect and restore minimality, an extension of the regular restriction of resolution
• Support ordered resolution
• Counting the number of equivalent binary resolution proofs
• scientific article; zbMATH DE number 4072434 (Why is no real title available?)

This page was built for publication: Rank/activity: A canonical form for binary resolution

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4249905)