English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

A classical question of propositional logic is one of the shortest proof of atautology. A related fundamental problem is to determine the relativeefficiency of standard proof systems, where the relative complexity is measuredusing the notion of polynomial simulation.  Presently, the state-of-the-art satisfiability algorithms are based onresolution in combination with search. An Ordered Binary Decision Diagram(OBDD) is a data structure that is used to represent Boolean functions.  Groote and Zantema have proved that there is exponential separation betweenresolution and a proof system based on limited OBDD derivations. However,formal comparison of these methods is not straightforward because OBDDs work onarbitrary formulas, whereas resolution can only be applied to formulas inConjunctive Normal Form (CNFs).  Contrary to popular belief, we argue that resolution simulates OBDDspolynomially if we limit both to CNFs and thus answer negatively the openquestion of Groote and Zantema whether there exist unsatisfiable CNFs havingpolynomial OBDD refutations and requiring exponentially long resolutionrefutations.

Resolution Simulates Ordered Binary Decision Diagrams for Formulas in Conjunctive Normal Form