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