scientific article; zbMATH DE number 2084326

MaRDI QIDQ3043797zbMATH OpenFDO

Authors Jan Friso Groote, Hans Zantema

Publication date 6 August 2004

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2244/22440033.htm

Mathematics Subject Classification ID

Classical propositional logic (03B05) Mechanization of proofs and logical operations (03B35) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• Resolution and binary decision diagrams cannot simulate each other polynomially
• Extended resolution simulates binary decision diagrams
• Extended Resolution Proofs for Conjoining BDDs
• Binary decision diagrams for first-order predicate logic.
• Ordered binary decision diagrams and the Davis-Putnam procedure

Cited in

(4)

• The intractability of resolution
• Resolution and binary decision diagrams cannot simulate each other polynomially
• Extended resolution simulates binary decision diagrams
• Extended Resolution Proofs for Conjoining BDDs

This page was built for publication:

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