CS/Linguistics Coloquium: Sean Fulop - Wed. 29 November at 2:30

[Margery Ishmael]

CS/Linguistics COLLOQUIUM ANNOUNCEMENT

Wednesday, 29 November at 2:30 in Ryerson 276
(to be followed by refreshments in Ryerson 255)

Sean Fulop, Visiting Assistant Professor with the Department of 
Linguistics, University of Chicago

Title: Toward a unified theory of efficient proof search

Abstract: Applications of logic are generally motivated by the desire to 
prove things, since that is what logics do best. Or do they? It is true 
that a given logic may allow one to find out whether a given expression is 
provable or not, but too often the obvious algorithms for proving that a 
particular expression is a theorem are woefully inefficient.

These poorly performing proof search algorithms are usually based upon some 
standard notion of a proof in some kind of deductive system which can 
derive the logical theorems.
Since the algorithms are based in standard proof theory, the best (if not 
the easiest) way of improving upon them is to improve the underlying proof 
theory. Many logics which are useful for representing grammars of natural 
languages are propositional and decidable, making the
proof of theorems especially straightforward. But if the search for these 
proofs is inefficient, there is still a problem at hand.

In this presentation, I will summarize two distinct past approaches to more 
efficient proof systems in logics, namely the "matrices with connections" 
approach developed for classical and intuitionistic logic, and the "proof 
nets" that were developed for linear logic. Both  techniques derive from 
noticing that standard proof algorithms in a Gentzen-style sequent calculus 
are inefficient because the deductive system is overly redundant, and so 
the search space for proofs becomes bloated. The improved methods can each 
be characterized as successfully eliminating the redundancy by homing in on 
"correctness conditions" that must be met by, in each case, a novel 
representation of a proof structure.

So, efficient proof search is already a solved problem---sort of. The 
trouble is, the successful solutions are "ad hoc" and specific to a couple 
of different logics. No one seems to understand why they work, in a 
sufficiently general sense. In applying logics for grammar and computation, 
we would like to be able to specify an arbitrary propositional logic within 
a broadly defined class, and have an efficient proof search algorithm 
available for every logic in the class. This is as yet an unsolved problem, 
but we are getting close. In this talk I would like to discuss a unified 
and more principled view of new proof representations for efficient proof 
search in a large class of propositional logics, which I believe is the 
latest work in progress on this problem.

====================================================
Margery Ishmael
Department of Computer Science
1100 E. 58th St.
Chicago, IL 60637

tel: 773 834-8977  fax: 773 702-8487

marge at cs.uchicago.edu 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20001120/ed339efc/attachment.htm