TCS and PAM seminar
We have a weekly informal seminar of the TCS group,
jointly with the
PAM-seminar from CWI,
often but not always on Fridays 15.30 - 16.30 at the VU.
Femke van Raamsdonk
(e: f.van.raamsdonk at vu.nl) if you wish to give a talk.
2018 08 16 (Thursday)
Michael Faerber (University of Innsbruck)
Nonclausal Connection Proof Search
This talk is about automatic proof search via a connection calculus in first-order logic that does not require clausification, working directly on Skolemised formulas. I will discuss the automated theorem prover *nanoCoP* with a focus on its performance and introduce two of its implementations. For future work, I will talk about performance improvements of nonclausal proof search as well as the formalisation of nonclausal and clausal connection calculi.
2018 08 01 (Wednesday)
Marijn Heule (Texas University)
Computable Short Proofs
The success of satisfiability solving presents us with an interesting
peculiarity: modern solvers can frequently handle gigantic formulas
while failing miserably on supposedly easy problems. Their poor
performance is typically caused by the weakness of their underlying
proof system—resolution. To overcome this obstacle, we need solvers
that are based on stronger proof systems. Unfortunately, existing
strong proof systems—such as extended resolution or Frege systems—do
not seem to lend themselves to mechanization.
We present a new proof system that not only generalizes strong
existing proof systems but that is also well-suited for mechanization.
The proof system is surprisingly strong, even without the introduction
of new variables—a key feature of short proofs presented in the
proof-complexity literature. We demonstrate the strength of the new
proof system on the famous pigeon hole formulas by providing short
proofs without new variables. Moreover, we introduce
satisfaction-driven clause learning, a new decision procedure that
exploits the strengths of our new proof system and can therefore yield
exponential speed-ups compared to state-of-the-art solvers based on
This work is related to the paper
Short Proofs without New Variables by Marijn Heule, Benjamin Kiesl, Armin Biere.
which co-won the CADE 2017 Best Paper Award.
for a list of previous seminars.
Last modified August 2, 2018.