University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Separations in a hierarchy of propositional proof systems related to clause learning

Separations in a hierarchy of propositional proof systems related to clause learning

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Mustapha Amrani.

Semantics and Syntax: A Legacy of Alan Turing

Resolution trees with lemmas (RTL) are a resolution-based propositional proof system that is related to the DLL algorithm with clause learning, with its fragments RTL being related to clause learning algorithms where the width of learned clauses is bounded by k.

For every k up to O(log n), an exponential separation between the proof systems RTL and RTL is shown, indicating that a minimal increase in the width of learned clauses can lead to an exponential speed-up for clause learning algorithms.

This talk is part of the Isaac Newton Institute Seminar Series series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2019 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity