EVENT ANNOUNCEMENT


TWO SPECIAL SESSIONS

FEDERATED WITH THE MRR CONFERENCE


hosted by the seminar
Foundational Problems of Computer Science and Mathematics
Faculty of Mathematics, Informatics and Mechanics, University of Warsaw, Banacha street 2, room 5440
and
coorganized by the Institute of Computer Science of the Polish Academy of Sciences,
Department of Mathematics, Informatics and Mechanics of the University of Warsaw,
Polish-Japanese Institute of Information Technology
and the Polish Association for Logic and Philosophy of Science


PROGRAM


September 22, 2005 (Thursday)

15:30-16:30     WIKTOR MAREK (USA)
        AUTARKIES, AN APPLICATION OF KLEENE LOGIC IN SAT
16:30-17:00     tea break
17:00-18:00     DANA SCOTT (USA)
        TOPOLOGY, CATEGORIES, and LAMBDA-CALCULUS

September 27, 2005 (Tuesday)

15:30-16:30     DANA SCOTT (USA)
        PARAMETRIC SETS AND VIRTUAL CLASSES

The abstracts are available below.


A get-together dinner (non-sponsored) is being planned for Thursday night, Sept 22,
We are pleased to invite all the participants and the accompanying persons.

Andrzej Grzegorczyk, Andrzej Salwicki, Marian Srebrny



ABSTRACTS

W. MAREK, Sept 22, 05: AUTARKIES, AN APPLICATION OF KLEENE LOGIC IN SAT
ABSTRACT:
 Let F be a collection of clauses. An autarky for F is a partial valuation v of propositional variables such that whenever v touches a clause C in F, then v satisfies C. This concept is related to Kleene three valued logic as presented in "Introduction to Metamathematics", not two-valued logic. Autarkies have appealing properties and lead to better bounds on the complexity of algorithms than ones that are obtained from the most important practical algorithm, DPLL. In our presentation we will introduce autarkies, present their fundamental properties and prove several results. Specifically, that the problem HA (having autarkies) is NP-complete, and that like in the case of satisfiability, search version of HA can be obtained as an iteration of HA. We also show that the problems of testing if a CNF possesses positive autarky (one consisting of positive literals) or negative autarky are polynomial. As an application we find that the existence of autarkies problem for Horn theories, dual-Horn, and renameable Horn theories are all polynomial. We characterize autarkies for Krom theories and for affine theories.The lecture will be self-contained. The properties of autarkies  and all related concepts will be discussed in detail. The reported research is joint with M. Truszczynski of the same department.

DANA SCOTT, Sept 22, 2005: TOPOLOGY, CATEGORIES, and LAMBDA-CALCULUS
ABSTRACT:
 Many categories have injective objects, but their properties depend on what families of subobjects are allowed. In the case of topological T_0-spaces, for example, two alternatives suggest themselves: (1) arbitrary subspaces, and (2) dense subspaces. Both notions are interesting. Thus, a space D is injective in sense (1) iff for any space Y and subspace X and any continuous function f:X->D there is a continuous extension f':Y->D of f. Injective spaces are easily proved to be closed under arbitrary products and continuous retracts, which facts provide many examples once a few such spaces are known. Perhaps it is not so obvious, however, that injective spaces are also closed under the formation of function spaces, once the space of continuous functions is given the right topology; indeed the category of injective spaces and continuous functions is a cartesian closed category. The talk will review old and new results about injective spaces, applications of the results, and a recent use of injectives to define a cartesian closed extension of the category of all T_0-spaces. This topological point of view makes it obvious that (untyped) lambda-calculus models exist in many forms. A suitable choice of an injective space also shows how a notion of computability transfers to many familiar spaces.

DANA SCOTT, Sept 27, 2005:   PARAMETRIC SETS AND VIRTUAL CLASSES
ABSTRACT:
In an axiomatic development of geometry, there is much convenience to be found in treating various loci as sets. Thus, a line corresponds to the set of all points lying on the line; a circle, to the set of all points on the circumference. Moreover, sets of sets are natural, say in considering pencils of lines or circles or conics. And families of pencils are used as well. Does geometry need a full set theory, therefore? In giving a negative answer, we shall consider higher-type sets introduced by parametric definitions with just finite lists of points as parameters. An attempt will be made at axiomatizing such sets together with a notation for virtual classes. The objective is to have the use of set-theoretical notations without the ontology of higher-type logic and Zermelo-Fraenkel set theory.