UNIVERSITY OF HERTFORDSHIRE
             COMPUTER SCIENCE RESEARCH COLLOQUIUM

                            presents

          "Efficiency of Propositional Proof Systems"

                       Dr. Olga Tveretina
      (Compiler Technology and Computer Architecture Group,
     School of Computer Science, University of Hertfordshire)

                     11 February 2015 (Wednesday)
                          1 pm -2 pm

                  Hatfield, College Lane Campus
                       Seminar Room D102

                  Everyone is Welcome to Attend

                  Refreshments will be available

Abstract:

A classical question of propositional logic is one of the shortest proof
of a tautology. There is a related  question of how to construct an
algorithm that produces the shortest proof. Cook and Reckhow  proposed
to  attack the NP versus co-NP problem by  focusing on   lower bounds for
standard proof systems of increasing complexity. A related  fundamental
problem  is to determine the relative efficiency of standard proof
systems.

First we  present an overview of the area paying attention to  the
relative efficiency of  proof systems based on resolution and ordered
binary decision diagrams (OBDDs). Resolution is  very simple, yet forms
the basis of  popular tools for  theorem proving, such as SAT solvers,
that are used in  industrial applications.   An OBDD is a canonical data
structure  for  symbolic representation of Boolean functions which occurs
commonly in formal verification and CAD software for circuit synthesis.

The relative complexity of two proof systems can be measured using the
notion of polynomial simulation. Zantema and Groote proved that resolution
and OBDDs do not simulate each other polynomially on arbitrary inputs for
limited OBDD derivations. However,  formal comparison of these methods
is not straightforward because OBDDs work on arbitrary formulas, whereas
resolution can only be applied to formulas in conjunctive normal form
(CNF). Contrary to popular belief, I will argue that resolution simulates
OBDDs polynomially if we limit both to CNFs.

---------------------------------------------------
Hertfordshire Computer Science Research Colloquium
http://cs-colloq.stca.herts.ac.uk