COLLOQUIUM
Department of Computer Science and Engineering
University of South Carolina
 
Constructive Logic

John Rogers
College of Computing and Digital Media
DePaul University


Date: March 26, 2010 (Friday)
Time: 1430-1520 (2:30-3:20pm)
Place: 300 Main B102

Abstract Mathematical logic is one of the foundations of computer
science and a thorough understanding of that foundation is necessary
to carrying out research in many areas.  Most in CS are familiar with
classical propositional logic, where the truth value of a formula is
determined by the truth values assigned to the atomic propositions. 
But there are other logics, one could argue, that more closely follow
the approach CS uses to tackle problems.  One such is constructive
logic, also known as intuitionistic logic.  In classical logic,
showing that a formula is valid is done by showing that it’s true
under all truth  assignments.  In constructive logic, showing that a
formula is valid means providing a proof.  For example, classically we
say that either P = NP or that P != NP.  But because we don’t have
a proof of either assertion, constructive logic maintains that the
disjunction is not valid.  In fact, no formula of the form p v ~p is
valid.  This notion of requiring a proof and then constructing proofs
of compound formulas is defined for each of the connectives.  The idea
can be carried over to the typed lambda calculus and from there to
strongly-typed functional languages like ML and Haskell.    In this
talk, I will present the fundamentals of constructive propositional
logic, discuss its application to CS, and end with an open problem.


John Rogers is is currently an Associate Professor of Computer Science
in the College of Computing and Digital Media at DePaul University,
where he has been since earning his Ph.D. in 1995 at the University of
Chicago.  His main area of interest is computational complexity theory
and, from that perspective, has investigated aspects of quantum
computing, applications of Kolmogorov complexity, poset game theory,
and various non-classical logics.  He is the publicity chair for the
annual Conference of Computational Complexity and chief organizer of
the semi-annual Midwest Theory Day.