Newsgroups: ut.theory
Path: utzoo!utgpu!jarvis.csri.toronto.edu!ai.toronto.edu!toni
From: toni@ai.toronto.edu (Toniann Pitassi)
Subject: student seminar
Message-ID: <8804061649.AA11173@ai.toronto.edu>
Organization: Department of Computer Science, University of Toronto
Date:	Wed, 6 Apr 88 11:29:11 EDT

     
The student seminar will be held as usual on Thursday from 11-12
Toni Pitassi will be speaking.

A proof system P1 is said to "p-simulate" another proof system P2 if
there exists a uniform function computable in polytime which
"translates" a proof in P2 of some formula, f,  to a proof in P1 of the
same formula f.
The simulation is said to be "efficient" if the transformation
produces a proof in P1 that is bounded by a polynomial in the
length of the proof in P2.

I will describe most of the major proof systems for propositional calculus
and then classify them according to known p-simulation results.
Recent lower bound and p-simulation results will then be given for
resolution
(and hopefully at least one proved).