29 May 2009, Computational Social Choice Seminar, Daniele Porello

Linear logic is a resource-sensitive logic that provides tools to describe when the availability of hypotheses matters in a derivation. In this talk, I will present an application of linear logic as a language for multi-unit combinatorial auctions, in which the number of indistinguishable goods is relevant for the allocation procedure. Simple bids will be interpreted as formulas of linear logic stating, intuitively, that a bidder is disposed to pay a certain amount of money for certain bundles of goods. Then, we will see types of bidding languages to define complex bids, using linear logic connectives, that resemble the usual languages for combinatorial auctions (OR and XOR language). The syntax of linear logic allows, for example, to express in a precise way some interesting distinctions between types of goods, such as reusable and non-reusable goods or sharable and non-sharable goods. Moreover, we will interpret the procedure of allocation, and the winner determination problem, by means of proof search in a sequent calculus for linear logic. In particular, we use Horn fragments of linear logic in order to have proof search in NP. This is joint work with Ulle Endriss.

For more information, see http://www.illc.uva.nl/~ulle/seminar/, or contact Ulle Endriss (ulle at illc.uva.nl).