%Use LaTeX to process this file.

\documentclass[11pt]{article}

\textwidth 6.5in
\oddsidemargin -0.0in
\textheight 9.0in
\topmargin -0.7in

\begin{document}

\date{}

\baselineskip=12pt

\vspace*{3cm}

\begin{center}
{\Large {\bf The Interdisciplinary Ph.D. Program\\\vspace*{3mm} in Pure 
and
Applied Logic\\\vspace*{5mm} at\\\vspace*{5mm} Carnegie Mellon 
University}}\\

\vspace*{3mm} {\large {\bf July 2000}}
\end{center}

\vspace*{1.5cm}

\section{{\protect\large {\bf Nature and aims of the program}}}

\noindent
Carnegie Mellon's Ph.D. Program in Pure and Applied Logic is an
interdisciplinary venture, jointly sponsored by the Departments of
Mathematical Sciences, Philosophy, and Computer Science. Each of these
three departments administers a {\it track} of the Program.

Carnegie Mellon a large and active group of faculty in Pure and
Applied Logic, with a particularly strong concentration in
foundational aspects of Computing. This Logic Community has an
established record of collaborations in pursuing theoretical research,
conducting major implementation projects, and running colloquia and
workshops. The Program builds on these strengths to educate new
generations of scientists who will pursue research in Pure and/or
Applied Logic.


The PAL World-Wide Web home page is at 
\newline 
http://www.cs.cmu.edu/afs/cs/project/pal/www/pal.html

\newpage

\section{{\protect\large {\bf The faculty}}}

\vspace{.15in}

As of Fall 2000, the Program faculty consists of:

\vspace{.15in}

\begin{itemize}
\item  {\it Clark Glymour,} Alumni University Professor of Philosophy;
\item  {\it Dana Scott,} Hillman University Professor of Computer Science, 
 Philosophy, and Mathematical Logic;
\item  {\it Teddy Seidenfeld,} Herbert A. Simon Professor of Philosophy 
and Statistics;
\item  {\it Peter Andrews,} Professor of Mathematics;
\item  {\it Cristina Bicchieri,} Professor of Philosophy and
Social and Decision Sciences;
\item  {\it Edmund Clarke,} FORE Systems Professor of Computer Science;
\item  {\it John Reynolds,} Professor of Computer Science;
\item  {\it Wilfried Sieg,} Professor of Philosophy, Head of the Philosophy
Department;
\item  {\it Peter Spirtes,} Professor of Philosophy;
\item  {\it Richard Statman,} Professor of Mathematics and Computer 
Science;
\item  {\it Stephen Brookes,} Associate Professor of Computer Science;
\item  {\it Rami Grossberg,} Associate Professor of Mathematics;
\item  {\it Robert Harper,} Associate Professor of Computer Science;
\item  {\it Kevin Kelly,} Associate Professor of Philosophy;
\item  {\it Peter Lee,} Associate Professor of Computer Science;
\item  {\it Frank Pfenning,} Senior Research Computer Scientist;
\item  {\it Richard Scheines,} Associate Professor of Philosophy;
\item {\it Horacio Arlo-Costa,} Assistant Professor  of Philosophy;
\item {\it Jeremy Avigad,} Assistant Professor of Philosophy;
\item {\it Steve Awodey,} Assistant Professor of Philosophy;
\item  {\it James Cummings,} Assistant Professor of Mathematics;
\item {\it Peter Vanderschraaf,} Assistant Professor of Philosophy;
\item {\it Ernest Schimmerling}, Assistant Professor of 
Mathematics.
\item {\it Mandy Simons}, Visiting Assistant Professor of Philosophy and 
Linguistics;
\end{itemize}

%In addition, the Carnegie Mellon Logic Community regularly hosts 
%prominent
%visitors. Long term visitors in the recent past 
%include W.\ Buchholz, M.\ Coppo, T.\ Coquand, P.\ Freyd, J.\ Gray,
%D.\ Harel, K.\ Holland, G.\ Huet, B.\ Kushner, Ph.\ Le Chenadec, 
%G.\ Longo, H.\ Schwichtenberg, J.\ Siekmann, B.\ Trakhtenbrot, and S. 
%Wainer.

Logicians at the adjacent University of Pittsburgh include N.\ Belnap, R.\
Daley, K.\ Manders, and R.\ Thomason.

Current research interests of the Program's faculty include: {\it 
Automated
Theorem Proving, Category Theory, Constructive and Feasible Mathematics,
Decision Theory, Foundations of Programming Languages, Game Theory, Logics
of Programs, Lambda Calculus, Learning Theory, Model Theory, Proof Theory,
Set Theory, Set-theoretic Algebra, Temporal and Modal Logics, Theory of
 Computing, and Type Theory}.

The Program is further strengthened by major research and educational
activities at Carnegie Mellon in related fields, such as {\it Algorithms,
Artificial Intelligence, Combinatorial Optimization, Computational
Complexity, Computational Linguistics, Operations Research,} and {\it %
Programming Systems.}

\vspace{.10in}

Here is a brief description of the research interests of the Program 
faculty.

\vspace{.10in}

\begin{itemize}
\item  {\bf Clark Glymour, Alumni University Professor of Philosophy}

Professor Glymour has worked in several areas of philosophy of science,
including the philosophy of physics, theories of scientific explanation 
and
confirmation, philosophy of psychology, and topics in philosophical logic.
His present research interests include computational learning theory,
methodological issues in artificial intelligence, formal methods in
automated causal inference, and methodological issues in cognitive
psychology. He is now at work on a book on Freud and Cognitive Science.

\item  {\bf Dana Scott,} {\bf Hillman University Professor of Computer 
Science,} \newline
\makebox[23mm]{} {\bf Philosophy, and Mathematical Logic}

Professor Scott's work in logic has concerned the theories of models,
automata and sets; modal and intuitionistic logic, constructive 
mathematics,
and connections between category theory and logic. His interests in
Philosophy concern the foundation and philosophy of logic and mathematics
and the semantical analysis of natural language. His work in computer
science has been principally directed toward the development of 
denotational
semantics of programming languages and mathematical foundations for
computability. Currently he aims at unifying the semantical approach with
constructive logical formalisms to be able to give rigorous and machine
implementable proof methods and development tools for the construction of
correct programs.  He also has a strong interest in promoting the use of 
computer-algebra systems in teaching and research.

\item  {\bf Teddy Seidenfeld, Herbert A. Simon Professor of Philosophy and 
Statistics}

Professor Seidenfeld is interested in statistical inference that
attend the use of merely finitely additive probabilities, and their
surprising effect on statistical decision theory. He is also
interested in the general question of whether the norms of Bayesian
statistics can be extended from individuals acting alone to
cooperative groups. The aim is to provide a unified treatment of group
probabilities and group decisions. The strategy which he employs in
joint research with a few colleagues of his from the Statistics
department is to relax a central assumption of Bayesian, expected
utility theory, the ``ordering'' postulate.

\item  {\bf Peter Andrews, Professor of Mathematics}\\

Professor Andrews' interests center on automated theorem proving,
especially for theorems of type theory (higher-order logic). Research
is based on an approach to automated theorem proving involving
expansion trees and matings, which represent the essential
combinatorial structure inherent in proofs of theorems. They can be
found by heuristic search, and natural deduction proofs can be
constructed from them without further search. A computer system called
TPS implementing these ideas in Common Lisp has been developed. It can
be used in automatic or interactive mode, or a combination of these,
to construct proofs and to translate proofs from one format to
another. A fragment of TPS called ETPS is used as an interactive aid
by students in logic courses.

\item  {\bf Cristina Bicchieri, Professor of Philosophy and Social
and Decision Sciences}

Professor Bicchieri's research centers around two main topics: game
theory and philosophy of social science. Her work on game theory
includes the logical foundations of equilibrium, belief revision
models, applications of epistemic logic and nonmonotonic logics to
game modeling and applications of game theory to distributed AI. Her
work in the philosophy of social science is primarily on the emergence
and evolutionary dynamics of social norms.

\item  {\bf Edmund Clarke, FORE Systems Professor of Computer Science}

Professor Clarke works on the boundary between theoretical computer
science and programming systems. He is particularly interested in the
use of formal methods for constructing correct and reliable hardware
and software. His research group has developed a temporal logic based
verifier for finite state systems that can automatically check
properties of sequential circuits with more than $10^{20}$ reachable
states and has been used to find subtle errors in hardware
controllers. He is also interested in developing powerful theorem
provers that are able to handle theorems with significant complexity.

\item  {\bf John Reynolds, Professor of Computer Science}

Professor Reynolds is interested in the design of programming
languages and languages for program specification, mathematical tools
for defining the semantics of such languages, and methods for proving
that programs satisfy their specifications. His current goals
are (1) to understand and unify the rich variety of type systems, including
polymorphic types, intersection types, and the types of linear logic,
that have proliferated in recent years and (2) to extend strong typing and
proof systems to low-level languages that give the user control over data
representation and storage allocation.

\item  {\bf Wilfried Sieg, Professor of Philosophy, Head of the Philosophy
Department}

Professor Sieg's main research area is in Mathematical Logic and
Philosophy of Mathematics. He has done mathematical work in proof
theory, and has also given philosophical analyses of foundational
approaches in the 19th and 20th century. His interests include closely
related issues in the foundations of Cognitive Science (Church-Turing
thesis), applications of logic to automated proof search, and the
educational use of sophisticated (machine) tutors.

\item  {\bf Peter Spirtes, Professor of Philosophy}

Professor Spirtes (in collaboration with Clark Glymour and Richard
Scheines) has been investigating how to reliably infer causal
relations from statistical data, given various kinds of background
information. By connecting causal hypotheses with statistical
hypotheses of conditional independence and graphical representations
of statistical models, we can precisely delineate what background
knowledge is required in order to reliably infer various features of
the causal relations between random variables. We have developed,
proved the correctness of, and implemented a number of algorithms for
reliable causal inference that can be run on as many as a hundred
variables, as long as the causal relations between the variables are
sparse. We are currently turning these algorithms into a practical
tool (TETRAD II) that will be useful to statisticians and in the
development of expert systems.

\item  {\bf Richard Statman, Professor of Mathematics and Computer 
Science}

Professor Statman's interests include mathematical logic ($\lambda $
-calculus, proof theory, constructivity, theory of computation),
combinatorics and graph theory (especially topological graph theory,
well partial orderings, coin weighing problems and combinatorial
algorithms), as well as theoretical computer science (complexity
theory, denotational semantics, theorem proving, foundations, logic of
programs).

\item  {\bf Stephen Brookes, Associate Professor of Computer Science}

Professor Brookes works generally on issues related to the semantics
of programming languages, including the development of new semantic
models and semantically based techniques for reasoning about program
behavior. His current focus is on intensional semantics: models of
programs which permit reasoning about efficiency as well as
correctness. He is particularly interested in developing compositional
proof methods for reasoning about parallel programs.

\item  {\bf Rami Grossberg, Associate Professor of Mathematics}

Professor Grossberg's research interests are concentrated in pure and
applied model theory, especially in classification theory of the model
theory of infinitary logics, related problems in combinatorial set theory,
and applications of these to algebra.


\item  {\bf Robert Harper, Associate Professor of Computer Science}

Professor Harper's research activities center around two main topics:
programming languages and computer-assisted formal reasoning. His work
in programming languages focuses primarily on the role of type
structure in language design, and on the use of operational semantics
as the basis for the definition and implementation of programming
languages. His work in computer-assisted formal reasoning is concerned
with the development of the theory and practice of general logical
frameworks as the basis for implementing formal systems on a computer.

\item  {\bf Kevin Kelly, Associate Professor of Philosophy}

Professor Kelly's interests lie primarily in the area of epistemology
and the philosophy of science. His current research interests focus on
computational learning theory as a response to the problem of
induction and as a tool to discern the scientific limitations of
computation.

\item  {\bf Peter Lee, Associate Professor of Computer Science}

Professor Lee's research interests lie in the area of semantics-based
analysis and implementation of programming languages. He is particularly
interested in the use of logic and semantics to specify optimizing 
compilers.

\item  {\bf Frank Pfenning, Senior Research Computer Scientist}

Dr. Pfenning's research interests include logic programming and
functional programming and the application of methods from
mathematical logic and type theory to the problem of programming
language description and implementation. In particular, he has been
working on a logical framework, that is, a language for the definition
and manipulation of formal systems such as various logics, type
systems or operational semantics. He is also interested in theorem
proving in higher-order logics.

\item  {\bf Richard Scheines, Associate Professor of Philosophy}

Dr. Scheines mostly works on two research projects. The first is an
intelligent computer tutor for logic. The tutor, now used by approximately
40 students each term, provides strategic help based on a complete but
natural algorithm for proof search in natural deduction developed by
Scheines and Sieg. The project combines issues from logic, educational
computing, and cognitive psychology. The second project involves inferring
causal explanations of statistical data. It involves the philosophical
foundations of causality and probability and the design and study of
algorithms for discovering causal structure from statistical data.

\item {\bf Horacio Arlo-Costa, Assistant Professor of Philosophy}

Professor Arlo-Costa's interests have focused on epistemology and
knowledge representation (in AI and economic modelling).  This work
has been motivated by an interest in understanding and clarifying the
nature of rationality.  Recent research centered around methodological
problems in AI and conditional logic.  Current research includes work
in the foundations of cognitive science, causal modelling, and models
of bounded rational agents.


\item {\bf Jeremy Avigad, Assistant Professor of Philosophy}

Professor Avigad studies mathematical logic.  His particular research 
interests include proof theory, constructive mathematics, proof complexity,
and the history and philosophy of mathematics.  He is especially interested
in understanding the relationship between classical and constructive
aspects of mathematical practice.


\item {\bf Steve Awodey, Assistant Professor of Philosophy}

Professor Awodey's interests are in logic, its relationship to
mathematics and computer science, and the surrounding philosophical
issues.  The focus of his current research is topos theory and 
higher-order logic.  His technical work is mainly in the areas of
type theory, categorical logic, and sheaf theory.  Category theory is 
his chief technical tool; it also informs his perspective on 
philosophical issues in mathematics.


\item {\bf James Cummings, Assistant Professor of Mathematics}

Professor Cummings' research interests are centered in set theory,
especially the areas of large cardinals, forcing and inner models. His
recent work includes results on stationary reflection, combinatorial
principles at successors of singulars, and $\aleph_2$-Souslin trees.
He is also interested in dynamical systems, and in the application of
logic to computer science.


\item {\bf Peter Vanderschraaf, Assistant Professor of Philosophy}

Professor Vanderschraaf is working on the development of a 
general theory of convention, and proposes to use this theory to
address longstanding difficulties in ethics and political 
philosophy.  As part of his overall project, he is attempting to
fully integrate the insights into the nature of convention of 
both the philosophical and the social science traditions.


\item {\bf Ernest Schimmerling, Assistant Professor of 
Mathematics}

Professor Schimmerling's work has been in set theory, with an emphasis
on core models and their connections to other areas such as
descriptive set theory and infinitary combinatorics.  He has
collaborated on projects with James Cummings, William Mitchell, John
Steel, and Hugh Woodin.

The simplest core model is $L$, Kurt G\"{o}del's Constructive
Universe.  G\"{o}del showed that the Continuum Hypothesis holds in
$L$.  Soon thereafter, the importance of $L$ to the theory of
Sigma-1-2 definable sets of reals was realized.  It has been seen that
other core models play roles analogous to that of $L$ at higher levels
of definability.

Ronald Jensen later isolated some key combinatorial principles and
proved that they hold in $L$.  These include the widely applied
Diamond, Square, and Morass principles.  His method of proof, known as
``fine structure'', also lead him to discover his famous Covering
Lemma, with its far reaching consequences, especially in the theory of
large cardinals below O$^{\#}$ .  (If O$^{\#}$ does not exist, then
some of the combinatorial principles which hold in $L$ really hold!)
Core models, in general, have a fine structure which has been used to
prove that they satisfy some of the same combinatorial principles as
$L$ does.  In addition, there is a particular core model, called $K$,
which satisfies some of the consequences of the Covering Lemma under
more relaxed hypotheses.  It has been seen that $K$ plays roles
analogous to that of $L$ at (some) higher levels of the large cardinal
hierarchy.

\item {\bf Mandy Simons, Visiting Assistant Professor of Philosophy and 
Linguistics}

Professor Simons' research deals with the formal semantics and
pragmatics of natural language.  She is particularly interested in
phenomena which show the interaction of compositional semantics with
general conversational principles.  To date, her work has examined
linguistic expressions whose interpretation requires a
cross-sentential perspective, or reference to context: pronouns,
definite descriptions, and presupposition-inducing expressions.
Currently, she is working on the semantics and pragmatics of natural
language disjunction.

\end{itemize}

\section{{\protect\large {\bf Courses, colloquia, and conferences}}}

\noindent
The following graduate courses and seminars were offered by the
Carnegie Mellon Logic faculty in the recent past or are planned for
the next academic year. Courses with prefix 15 are offered by the
Computer Science Department, those with prefix 21 are offered by the
Department of Mathematical Sciences, and those with prefix 80 are
offered by the Philosophy Department.

%In general courses and seminars should be listed only
%if they have been given in the past three years, 
%or we have plans to give them in the current or next year.
%Comments should show who gave each course and when.


\begin{itemize}
\item  {\normalsize 80-320 Topics in Philosophy of Science} 
%Clark Glymour
%TR 3:00 - 4:20
%Units:
%(F 95)


{\footnotesize A more detailed examination of some issue in the philosophy 
of science, such as the nature of scientific progress, the nature of 
evidence, or the theory of explanation. The topic may also be an in-depth 
examination of some philosophical issues raised by a particular science 
(e.g., conventionalism in space-time physics or the role of adaptation in 
evolutionary theory).  }

\item  {\normalsize 21-600 Mathematical Logic I }
%Instructor: Peter Andrews
%MWF 11:30 - 12:20 pm
%Scaife Hall 212 
%Units: 12 
%(F95, F96, F97, F98, F99, F00)


{\footnotesize The study of formal logical systems which model the 
reasoning of mathematics, scientific disciplines, and everyday discourse.
Propositional calculus and first-order logic. Syntax, axiomatic treatment,
derived rules of inference, proof techniques, computer-assisted formal
proofs, normal forms, consistency, independence, semantics, soundness,
completeness, the L\"{o}wenheim-Skolem Theorem, compactness, equality. 
Offered every fall. }

\item {\normalsize 80-600 Minds, Machines, \& Knowledge}
%Instructor: Teddy Seidenfeld
%TuTh - 1:30 - 2:50 
%DH 1209
%Units: 9 - 12
%(F96, F98, F00)

{\footnotesize We examine important presuppositions in several 
contemporary essays that debate the scope and limits of artificial 
intelligence. Specifically, the class will discuss contemporary views on 
foundational versus coherence models of human knowledge. (Does human 
knowledge have a secure basis or is it a mere "web of beliefs"?) These 
questions about the organization of knowledge are contrasted with 
objections raised, for example, by Searle and Dreyfus against the "strong 
AI" thesis of Newell and Simon. Also, we consider several current models 
of knowledge which incorporate probability and other measures of 
uncertainty, including some recent work on "parallel" systems. 

Prerequisite:  80-100 or some equivalent introduction to Philosophy.}

\item {\normalsize 21-602 Introduction to Set Theory}
%Instructor: Ernest Schimmerling
%TuTh 3:30 - 4:50
%PH A22
%12 units
%(F00)

{\footnotesize This is a standard first graduate course in set theory.
The two main topics are constructibility and forcing.  We will cover
chapters I and III-VII of the textbook in order, and refer back to
chapter II as needed.  Our primary goal is the independence of the
continuum hypothesis.

\noindent Textbook.  Kenneth Kunen {\it Set Theory: An
Introduction to Independence Proofs}

\noindent  Prerequisites.  Students should have a background in
undergraduate level set theory (cf. 21-229 and the textbook by Hrbacek
\& Jech) and logic (cf. what I covered in 21-700 or the logic
textbooks by Goldstern \& Judah or Enderton), which includes a working
knowledge of basic ordinal and cardinal arithmetic, G\"{o}del's
completeness theorem, and the downward L\"{o}wenheim-Skolen theorem.
An understanding of the statement of G\"{o}del's theorem on
consistency proofs will also be assumed.}


%\item  {\normalsize 21-602 Introduction to Set Theory }
%Instructor: James Cummings
%MWF 1:30 - 2:20 
%DH 2105
%12 units
%(S97)


%{\footnotesize The material to be covered: First order definability, the
%axioms of Zermelo Fraenkel. Cardinal arithmetic, ordered sets, well 
%ordered
%sets (axiom of choice), transfinite induction, the filter of closed
%unbounded sets (Fodor, Ulm, and Solovay's theorems), results of Erdos and
%Rado on $\Delta $-systems, some basic results in partition calculus - like
%Ramsey's theorem and the Erdos-Rado theorem. Small to medium size large
%cardinals (including measurable) introduced. Some applications to general
%topology, like solution to Alexandroff's conjecture, and the basic ideas 
%of
%descriptive set theory are presented. The independence of Suslin 
%conjecture
%from the usual axioms is presented using the diamond, and Martin's axiom.
%G\"{o}del's axiom of constructiblity V=3DL will be discussed. If time will
%permit the Galvin-Hajnal-Shelah inequality will be proved. }



\item  {\normalsize 21-603 Model Theory I} 
%Instructor: Rami Grossberg (rami@cmu.edu)
%MWF 2:30
%(S95, F96, F97, F98)
%(Rami Grossberg)

{\footnotesize Contents include: Similarity types, structures. Downward
L\"{o}wenheim-Skolem theorem. Construction of models from constants, 
Henkin's
omitting types theorem, prime models. Elementary chains of models, some
basic two-cardinal theorems, saturated models, basic results on countable
models including Ryll-Nardzewski's theorem. Indiscernible sequences,
Ehrenfeucht-Mostowski models. Introduction to stability, various rank
functions, primary models, and a proof of Morley's categoricity theorem.
Basic facts about infinitary languages, computation of Hanf-Morley 
numbers. }

{\footnotesize Prerequisite:  Elementary logic or permission of the 
instructor}

{\footnotesize Text: Lecture notes by the instructor}
%{\footnotesize Offered at least once every two years.}


\item{\normalsize 80-605 Rational Choice}
%Peter Vanderschraaf
%TuTh 3:00 - 4:20)
%DH 2122
%No prerequisites
%9 - 12 units
%(F98, F00)

{\footnotesize This course will cover selected topics in rational choice theory, which
informally is the analysis of how to make correct decision in a given
context. Possible topics may include, and are not limited to: individual
decision making under uncertainty, problems of public choice in which a
group of individuals must collectively make a decision, game-theoretic
problems of conflict and coordination, and alternative approaches to the
problem of fair division of goods.  This course will stress the role that
formal methods can play in the analysis of decisions and alternative
applications of decision theory to issues in philosophy and social science.}

\item {\normalsize 80-610 Logic and Computation}
%Instructor: Jeremy Avigad
%MW 10:30 - 11:50
%(F 96, F97, F98, F00)
%12 units
%Texts: TBA

{\footnotesize Among the most significant developments in logic in the
twentieth century is the formal analysis of the notions of provability
and semantic consequence. For first-order logic, the two are related
by the soundness and completeness theorems: a sentence is provable if
and only if it is true in every interpretation. This course begins
with a formal description of first-order logic, and proofs of the
soundness and completeness theorems.

Other topics may include: compactness, the L�wenheim-Skolem theorems,
nonstandard models of arithmetic, definability, other logics, and
automated deduction. 

Prerequisites: 80-210 or 80-211, or an equivalent
course in Mathematics or Computer Science.}


%{\footnotesize An introduction to computability theory and G\"{o}del's 
%incompleteness theorems. Topics include formal models of computation 
%Turing machines, the lambda calculus, and the recursive functions), r.e 
%and universal r.e. sets, undecidability, formal systems, coding and 
%self-reference, incompleteness, and the undefinability of truth. }


\item {\normalsize 80-612 Philosophy of Mathematics}
%Instructor: Wilfried Sieg
%TR 1:30 - 2:50
%Room: BH 150
%12 units 
%(S 98)

{\footnotesize Problems in the foundations of mathematical analysis prompted, around the
turn of the century, renewed philosophical reflection on mathematics and
related mathematical and logical work.  Set theoretic and constructivist
foundations for analysis are described; Hilberts program is analyzed in
detail.  Finally, a structuralist position is defended: this position is
philosophically  influenced by the work of Bernays and mathematically by
developments in mathematics (as reflected in Bourbaki's treatises and
category theory); it incorporates important insights from the main
foundational schools.}

%\item  {\normalsize 80-613 Arguments \& Inquiry }
%(Wilfried Sieg)
%(F95)


%{\footnotesize This course is an introduction to (mathematical) logic.
%It aims at characterizing general strategies for rational
%argumentation and putting them to work in a systematic inquiry --
%elementary set theory. We start out with a preliminary analysis of the
%axiomatic method and the concept of formality. Then we pursue in
%parallel the two main topics. On the other hand, we develop the
%general framework for making inferences. That involves , first, the
%construction of a symbolic language in which a large part of ordinary
%English can be expressed; second, an analysis of forms of arguments
%and their representation in a logical calculus; third, a detailed
%discussion of the concept of computability (via Turing machines). On
%the other hand, we explore systematically and at first quite
%informally the theory of sets. That involves, first, introducing
%relations and functions; second, a discussion of the so-called
%paradoxes; third, the formulation of the axioms for set theory
%introduced by Zermelo and Fraenkel. The course presents basic concepts
%and their history, so that students are in a position to understand
%central methodological issues; but it also introduces and familiarizes
%with basic logical, set theoretic, and recursion theoretic techniques
%-- techniques that are used extensively in mathematics, computer
%science, linguistics, and cognitive science. }

%{\footnotesize Books: (i) J. Barwise and J. Etchemendy, Tarkski's
%World; CSLI Lecture Notes \# 25, Stanford, 1993. (ii) J. Barwise and
%J.  Etchemendy, Turing's World; CSLI Lecture Notes \# 35, Stanford,
%1993. (iii) R. L.  Causey, Logic, Sets, and Recursion; Jones and
%Bartlett Publishers, Boston, 1994. }

\item{\normalsize 80-614 Logic in Artificial Intelligence}
%Alternate years (Spring) 
%9-12 units

{\footnotesize An introduction to several formalisms used in knowledge
representation and database theory. The emphasis is placed on
nonmonotonic logic, conditional logic and belief revision methods. We
will also study recent issues in the logics of knowledge and belief
and consider applications in distributed AI.  Several methodological
problems in AI are discussed.  Prerequisites: A basic course in logic
is recommended but not required.}

\item{\normalsize 80-615 Modal Logic}

{\footnotesize An introduction to first-order modal logic. The course considers several
modalities aside from the so-called alethic ones (necessity, possibility).
Epistemic, temporal or deontic modalities are studied, as well as
computationally motivated modals (like 'after the computation terminates').
Several conceptual problems in formal ontology that motivated the field are
reviewed, as well as more recent applications in computer science and
linguistics. Kripke models are used throughout the course, but we also
study recent Kripkean-style systematizations of the modals without using
possible worlds. Special attention is devoted to Scott-Montague models of
the so-called `classical' modalities.

Prerequisites:  80-210, or 80-211, or instructor's permission. }

\item {\normalsize 80-616 Probability \& Artificial Intelligence}
%Instructor: Peter Spirtes
%TR 12:00-1:20
%Room: SH 224
%Variable 9-12 units 
%(S 98)

{\footnotesize In this course we will examine foundational questions about the concepts of
causality and probability, how artificial intelligence techniques can be
used to solve some of the computational problems presented by the use of
probabilities and representations of causal relations, and how
probabilities and representations of causal relations have been
incorporated into recently developed expert systems. The foundational
questions we will examine are: What do causal and probabilistic statements
mean? How can probabilities and causal relations be inferred? Are there any
axioms relating causal relations to probability distributions? What are the
advantages and disadvantages of using probabilities as compared to
alternative representations of uncertainty? We will then discuss recent
developments in Artificial Intelligence (e.g. Bayesian networks) which have
solved some of the long-standing computational problems associated with the
use of probabilities and statements about causal relations. Finally, we
will study in detail some expert systems, such as QMR and Pathfinder, which
have incorporated these new techniques in order to perform medical
diagnosis.}

\item{\normalsize 80-617 Constructive Logic}
%Alternate Years Fall
%9-12 units

{\footnotesize This multidisciplinary junior-level course is designed to provide a
thorough introduction to modern constructive logic, its roots in
philosophy, its numerous applications in computer science, and its
mathematical properties. Some of the topics to be covered are
intuitionistic logic, inductive definitions, functional programming, type
theory, realizability, connections between classical and constructive
logic, decidable classes. 

Prerequisites: 80-210 or 80-211 and a programming course}


\item {\normalsize  80-620 Philosophy of Physics (Topics in the Philosophy 
of Science)}
%David Malament
%TR 9:00 - 10:20
%BH 150
% 9 units
%(F98)

{\footnotesize The course will not presuppose any particular course
work in physics, but will require a knowledge of basic undergraduate
mathematics (at least calculus and elementary linear algebra) and
formal logic.  Some class time will be devoted to background
exposition of needed mathematics and physics. The course will sample a
number of topics concerning the foundations and philosophical
implications of modern physics.  These will include: (1) probability
and determinism in classical mechanics; (2) probability and
indeterminism in quantum mechanics (and Bell's Theorem); (3) ``quantum
logic''; (4) Euclidean and non-Euclidean geometry; (5) Minkowski
spacetime geometry and the foundations of (special) relativity theory;
(6) debate over the ``conventionality of simultaneity''.  For information 
contact D-malament@uchicago.edu.}

{\footnotesize Prerequisites: Advanced undergraduate course; also
suitable for graduate students looking for a first course in the
subject.}

{\footnotesize Texts:  Readings on reserve in library TBA.}



\item {\normalsize 21-624 Selected topics:  Differential equations, groups 
and Galois theory}
% Rami Grossberg (rami@cmu.edu)
%MWF 12:30
%PHA19D
%12 units
%(F98)

{\footnotesize The fundamental question: ``Why the integral $\int
e^{-x^2}\ dx$ cannot be expressed in terms of elementary functions?''
lead Picard and Vessiot (in the 19th century) to develop an algebraic
theory of ordinary differential equations that is analogous to
classical Galois theory.  This theory was continued in this century by
Ritt and Kolchin.  In the sixties the theory was connected to the
theory of algebraic groups and number-theoretic questions.  My
interest in the field is motivated by some recent applications of
model theory to arithmetical geometry (by Hrushovski) and the
importance of the field to model theorists.  The course will be an
introduction to the basic classical results.}

{\footnotesize Prerequisites: No knowledge of logic is assumed, it is
desirable that the students have had an introductory course in algebra
covering Galois theory 21-610 or 21-374 (field theory).}


\item  {\normalsize 21-700 Mathematical Logic II} 
%(S95, S96, S97, S98)
%(Peter Andrews)

{\footnotesize Introduction to higher-order logic (type theory) with
primary emphasis on the typed lambda-calculus. Syntax and semantics,
lambda-notation, axiomatic treatment, axioms of Descriptions, Choice
and Infinity, weak completeness, weak compactness, standard and
non-standard models; computer-assisted formal proofs; formalization of
mathematics, definability of natural numbers, representability of
recursive functions, Church's Thesis; G\"{o}del's Incompleteness
Theorems, undecidability, undefinability. }

{\footnotesize Prerequisite: An introductory logic course such as 21-600 
or 80-610. }

\item {\normalsize 21-703 Model Theory II -- The spectrum function}
%Instructor: Rami Grossberg
%MWF 2:30
%PH A19
%12 units
%(F00)

{\footnotesize Part of the course will be set in theoretic in nature:  The fundamentals of Shelah ``non-structure'' theory will be presented, which are also the roots of proper forcing and pcf theory.  The other part is structure theory (more like commutative algebra):  The main results to be discussed are othoganality calculus, and the structure of regular types.  This will be used to prove to Shelah's ``Main Gap Theorem'' for countable theories.  If time will permit I will discuss also the solution to Morley's conjecture (i.e., the mapping $\lambda \mapsto I(\lambda , T)$  is a weakly monotonic).  Probably will also make comments on the lower part of the spectrum function.

It is expected that the students know elementary set theory as well as the fundamentals of classification theory (including various equivalent properties to superstability, forking calculus, and the stability spectrum theorem).

\noindent Prerequisites: Little more than an elementary course in model theory (21-603) and a graduate course in algebra or permission of the instructor.  The most basic parts of {\it www.math.cmu.edu/~rami/simple.dvi} and {\it www.math.cmu.edu/~rami/DR.dvi}.

\noindent Books:  There is no official text.  The following is the most relevant:  Saharon Shelah, {\it Classification Theory and the Number of Nonisomorphic Models}, Rev. Eed., North Holland, 1990, Amsterdam.}



%\item  {\normalsize 21-703 Model Theory II} 
%(F95, S97, S98, F99)
%Instructor: Rami Grossberg
%MWF 2:30-3:20
%Room: HBH 1003
%12 Units
%new course description forthcoming.

%{\footnotesize Most of the course I will concentrate in what is
%considered now ``main-stream model theory'' which is Shelah's
%classification theory (known also as Stability).  I will present the
%basic ideas of the theory in a more concrete approach than Shelah
%does.  Among the topics to be presented will be stability,
%superstability, several rank functions, tree-indiscernibles,
%construction of many-models (for unsuperstable theories), the theory
%of various notions of primeness and forking calculus, if time will
%permit I will present some of the theory of stable groups (up to and
%including the Macintyre-Cherline-Shelah theorem on super-stable
%fields).}

%{\footnotesize Prerequisites: An introductory course to model theory,
%like 21-603 and naive set-theory (elementary cardinal arithmetic, transfinite 
%induction, etc.).}

%{\footnotesize Recommended Text: Much of the material can be found in:
%S. Shelah, Classification Theory, North-Holland 1991. (There are
%several books in the field, among them books by: Baldwin, Buechler,
%Lascar, Pillay, Poizat.)  You are not expected to buy any of the above
%books.}

%{\footnotesize Method of Evaluation:  A 3-hour in-class final and a 
%midterm.}

\item { \normalsize 80-705 Game Theory}
%Instructors: Christina Bicchieri/Robin Dawes
%Cross-listed with SDS 88-706
%Wednesdays 4:00 - 6:00 pm
%Room:  BH 150
%Variable Units 9 - 18
%(S95, Spring)


{\footnotesize The first part of course will be a standard
introduction to noncooperative games. The second part will cover
special topics such as signaling and reputation effects, evolution and
learning, formal models of players reasoning, and applications of game
theory to artificial intelligence.}

{%\footnotesize Prerequisites: None.}



\item {\normalsize 80-710 Recursion and Hierarchies}
%Instructor: Jeremy Avigad
%MW 10:30-11:50
%Room: CFA 212
%Variable Units 9-18
%(S97, S98)

{\footnotesize Alternate Years (Spring): 9-12 units
An advanced course in computability theory and recursion theoretic
hierarchies.  Topics include finite-injury priority arguments, the
arithmetical and Borel hierarchies, and the projective and analytical
hierarchies.}


\item {\normalsize 15-711 Programming Languages}
%Stephen Brooks
%MF 10:00 - 12:20
%WeH 5409 A\& B
%12 units
%(F98)
%Details on schedule and course descriptions are available on-line via the C.S.
%web page (http://www.cs.cmu.edu).

{\footnotesize This course introduces and motivates foundational ideas
of programming language semantics to first- and second-year Ph.D.
students in computer science. The main focus is on the principles of
programming languages, their application in program analysis and
synthesis, and their relevance in the design and implementation of
programming languages. We aim to bring out the key concepts and
techniques, building in a modest amount of necessary mathematics and
logic as we go, at the same time as allowing students to see these
concepts in settings that involve real programming languages. We aim
to demonstrate that there is a scientific approach to programming
language theory, and that such an approach is vital in attempting to
answer questions about the pro's and con's of various languages, about
compiler correctness, and for many other practical purposes.}


%\item {\normalsize 15-711A Programming Languages}
%Instructor: John Reynolds
%TuTh
%Loc: tba
%Units: 1 Core Unit
%(F96)

%{\footnotesize  A survey of programming languages, semantics,
%and formalisms for specifying programs and proving their correctness.}

%{\footnotesize Topics include:}

%{\footnotesize Imperative programming: abstract syntax, denotational 
%semantics, partial and total correctness logics, arrays, continuations,
%operational semantics. Concurrency:  nondeterminism, powerdomains, 
%shared-variable concurrency, communicating sequential processes, deadlock,
%fairness, transition-trace semantics.}

%{\footnotesize Functional Programming: Lambda calculus, combinators,
%tupling, and alternative constructions, eager and normal-order
%evaluation, direct and continuation semantics, operational semantics,
%catch and throw, streams, backtracking, interpreters, graph
%reduction.}

%{\footnotesize Type systems: simple types, recursive types, subtypes, 
%polymorphism, module systems, semantical and ontological models, 
%parametricity, the Hindley-Milner algorithm, types as specifications.}

%{\footnotesize Combining functional and imperative programming: Iswim-like
%and Algol-like languages, references, aliasing and interference.}


%{\footnotesize Prerequisites: A knowledge of a variety of programming
%languages. Students other than postdoctoral students in computer science
%and pure and applied logic need instructor's permission.}

%{\footnotesize EVALUATION: Grades are computed in two ways: as an equally
%weighted average of the homework, the midterm, and the final, and as an 
%equally weighted average of just the midterm and the final. The actual 
%course grade is the higher of the two.}

%{\footnotesize Note: No enrollment limit, no instructor permission 
%required to enroll.}

\item{\normalsize 80-711 Proof Theory}
%Alternate years
%9 - 12 units

{\footnotesize An introduction to proof theory that addresses
philosophical, mathematical, and computational aspects of the
subject. Topics may include: the emergence of Hilbert's program, and
proof theory's more general reductive goals; deductive systems,
double-negation translations, cut elimination, and normalization; the
ordinal analysis of arithmetic; functional interpretation and the
extraction of computational information from proofs; and subsystems of
second-order arithmetic.  Ideally, students taking this course should
be familiar with the syntax and semantics of first-order logic
(covered in 80-310/610), and the basics of computability and coding of
syntax (covered in 80-311/611). Students should have taken at least
one of the two courses just mentioned, or the equivalent.}

\item{\normalsize 80-712  Intuitionism \& Constructive Mathematics}

%Offered intermittently: 9-12 units

{\footnotesize The course first presents basic principles of
constructive mathematics (as formulated e.g. by Kronecker, Hilbert,
Bishop) and the distinctive features of Brouwers intuitionistic
analysis.  Then intuitionistic logic and a variety of semantics are
investigated.  Finally, we discuss the fundamental difference between
a constructivist and realist position in the foundations of
mathematics.}

\item {\normalsize 80-713 Category Theory}
%Alternate years Fall(F97, S98)
%9-12 units

{\footnotesize Category theory, a branch of abstract algebra, has
found many applications in mathematics, logic, and computer
science. Like such fields as elementary logic and set theory, category
theory provides a basic conceptual apparatus and a collection of
formal methods useful for addressing certain kinds of commonly
occurring formal and informal problems, particularly those involving
structural and functional considerations.  This course is intended to
acquaint students with these methods, and also to encourage them to
reflect on the interrelations between category theory and the other
basic formal disciplines.

Prerequisites: one course in logic or algebra}


\item {\normalsize 80-717 Constructive Logic}
%Instructor: S. Awodey and Frank Pfenning
%TuTh 10:30 - 11:50
%PH 125C
%Wed Recitations
%9 units

{\footnotesize This multidisciplinary junior-level course is designed to provide a thorough introduction to modern constructive logic, its roots in philosophy, its numerous applications in computer science, and its mathematical properties.  Some of the topics to be covered are intuitionistic logic, inductive definitions, functional programming, type theory, realizability, connections between classical and constructive logic, decidable classes.

\noindent Prerequisites:  15-129 or equivalent and 15-212 for CS majors, a programming course and either 80-210 or 80-211 for Philosophy majors, 21-127 and one of 21-228, 21-484, 21-373, 21-132 for Mathematics majors.

\noindent Comment:  Design of this course is joint effort between Jeremy Avigad, Steve Awodey and Frank Pfenning with support by a grant for multidisciplinary course development from the University Education Council.}

\item{\normalsize 80-780  Linguistic Theory}
%Alternate Years (Spring): 9-12 units

{\footnotesize At this point in time, linguistic theory is diverse,
highly technical, and often rather abstruse. The goal of this course
is not to develop technical ability in any one theoretical approach to
language, but rather to reach an understanding of the philosophical
and theoretical underpinnings of different approaches. We will begin
by identifying the kinds of questions which linguistic theory seeks to
answer, and will go on to examine the fundamental assumptions which
underlie some of the theories which have been proposed to answer
them. The course will be based primarily on readings from the
linguistic and philosophical literature, through which we will examine
foundational issues in generative grammar, functional grammar,and
formal semantics. The course is appropriate for graduate students and
for advanced undergraduates with a significant background in
linguistics or in philosophy.}


\item{\normalsize 80-781  Formal Semantics}
%Alternate Years (Spring): 9-12 units

{\footnotesize This course is a high level introduction to the theory
of lingustic meaning and interpretation. When we look at how language
is used in communication, we see two interacting systems of
knowledge. On the one hand is the purely linguistic, or semantic,
information: the meanings of words and morphemes, and the linguistic
rules which govern how these meanings are combined to give the literal
meanings of larger expressions in which they occur. On the other hand
is knowledge of the context of utterance and of the rational
principles which govern language use. Hearers use this pragmatic
knowledge in conjunction with their semantic knowledge to determine
the communicative intentions of speakers. This course will introduce
students to explicit theoretical treatments of both the semantic and
pragmatic components of the linguistic system. }


\item {\normalsize 21-800(A)  Advanced Topics in Logic: Set Theory}
%Instructor: James Cummings
%MWF 1:30-2:20
%Room: PH A19D
%Units: 12
%(S96, S98, F99)

{\footnotesize This course is intended to be accessible to anyone who
has taken the beginning graduate course ``Introduction to Set Theory''
or an equivalent course.  I will assume knowledge of the rudiments of
forcing and constructibility (essentially the material of Chapter I-VII in 
Kunen's book). }

{\footnotesize There will be little or no overlap with the content of
my previous ``Topics in Set Theory'' course from Spring, 1998.  The
course will be divided into a series of three or four ``minicourses''
on different topics in set theory.  The topics are negotiable and I
welcome any reasonable suggestions.  Some of the topics that I am
considering are: An introduction to Shelah's pcf theory and its
combinatorial applications; The axiom of determinacy and its
consequences; Forcing Axioms: from Martin's Axiom to Marin's Maximum;
Proving consistency results from large cardinal hypotheses using
forcing; Reflection and compactness phenomena in set theory.}

{\footnotesize REFERENCES:  Kunen, ``Set theory'', North-HollandD; Kanamori,
``The higher infinite'', Springer-Verlag; Shelah, ``Proper and improper 
forcing'', Springer-Verlag; Shelah ``Cardinal arithmetic'' OUP; Moschovakis
``Descruotuve set theory'', North-Holland; Jech, ``Set theory'', 
Springer-Verlag}


\item {\normalsize  21-800(B) Advanced Topics in Logic: Recursion
 Theory}
%Instructor: Statman
%MWF  3:30 - 4:20 pm
%BH 231A
%Units: 12
%(S97, F99)

%updated description forthcoming.

{\footnotesize This is a graduate recursion theory course with no 
prerequisite except a course in logic.  Topics will include:}

\begin{itemize}
\item {\footnotesize Effective computation and Church's thesis}
\item {\footnotesize Hilbert's 10th problem and other unsolvable problems}
\item {\footnotesize Recursive functions and relations}
\item {\footnotesize Recursively enumerable sets and relations}
\item {\footnotesize The recursion theory}
\item {\footnotesize Reducibilities among sets}
\item {\footnotesize Post's problem and finite injury priority proofs}
\item {\footnotesize Degrees of solvability}
\item {\footnotesize The lattice of RE sets}
\item {\footnotesize The arithmetic, hyperarithmetic, and analytic 
hierarchy}
\end{itemize}

{\footnotesize Reference:  Rogers'  Theory of Recursive Functions and 
Effective Computability. }

\item  {\normalsize 21-803 Model Theory III }
% Grossberg
%MWF 2:30
%DH 2105
%12 units
% (F97, F98)

{\footnotesize I will introduce Shelah's notion of dependence in model
theory, namely forking relation.  It will be developed in the most
general context in simple theories.  It will be used to prove
uniqueness of prime models for stable theories, thus answering a 30
year old conjecture of Ritt concerning the uniqueness of differential
closure.  The finite equivalence relation theorem, the stability
spectrum theorem, unions of saturated models is saturated (under
sufficient stability).  Several extensions of these ideas will be
discussed.}


\item  {\normalsize 21-804 Mathematical Logic Seminar}
%Instructor: Rami Grossberg
%Time:  Mondays 4:30 - 6:00 pm 
%SHall 24 
% 12 units
%(F96, S97, F97, S98, F99, F00)


{\footnotesize The purpose of the seminar is to offer a forum for
discussion of some recent developments in mathematical logic. We will
concentrate in the areas of Model Theory and Set Theory. We will have
weekly two hour meetings where faculty and students present papers
(typically not authored by local people) at the level which will be
appropriate to the of participants (assume not much more than a first
graduate course in mathematical logic). It is possible to take this
seminar for credit, and in order to get a grade you will have to
present at least one paper (usually 3 - 5 lectures). You may also be
interested in participating passively (without giving a talk - not for
credit).   The structure is like a sequence of several mini-courses.  Every few
weeks the topic will be changed, and often the subjects of discussion are 
independent.}


\item {\normalsize 15-810(A) Verification of Concurrent, Reactive, and 
Real-Time Programs}
%Instructor Edmund M. Clarke (S 98)
%Time: TBA
%Room: TBA
%Units: 6

{\footnotesize This course is a graduate level research seminar on
automatic verification techniques for concurrent, reactive, and
real-time programs.  It was last taught in the fall of 1996, but
different topics will be covered this semester.  }

{\footnotesize The prerequisites for the course are minimal-basic
knowledge of elementary logic and automata theory.  Students taking
the class for graduate credit will be asked to prepare a short project
and give one or two lectures.  Auditors are also welcomed.}

{\footnotesize Logical errors in hardware controllers, communication
protocols, and real-time programs are becoming an increasingly
important problem.  They can delay getting a new production the market
or cause the failure of some critical device that is already in use.
The most widely used method for verifying such systems is based on
extensive simulation and can easily miss significant errors when the
program is very complicated.  Many of these programs can be viewed as
having only a finite number of states.  When this is the case, an
alternative verification technique called ``model checking'' may be
used.  In this approach specifications are expressed by automata or
temporal logic formulas, and programs are modeled as state transition
systems.  An efficient search procedure is used to determine
automatically if the specifications are satisfied by the transition
system.  The technique has been used in the past to find subtle errors
in a number of non-trivial designs.  Recently, the size of the state
transition systems that can be verified by model checking methods has
increased dramatically.  By representing transition relations
implicitly using Binary Decision Diagrams (BBDs), it has become
possible to check some examples with more than $10^{100}$ states! }

\noindent {\footnotesize Possible topics to be covered:}

\begin{enumerate}
\item {\footnotesize Modeling concurrent programs with state transition 
systems}
\item {\footnotesize Temporal logics}
\item {\footnotesize The mu-calculus and fixpoint theory}
\item {\footnotesize The basic model checking algorithm}
\item {\footnotesize Binary decision graphs and symbolic model checking}
\item {\footnotesize Using Omega-automata to specify properties of 
concurrent systems}
\item {\footnotesize Using Omega-automata to specify properties of
concurrent systems}
\item {\footnotesize Notions of equivalence for concurrent systems 
(observational equivalence, etc.)}
\item {\footnotesize Compositional reasoning techniques (e.g., the
 ``assume-guarantee'' paradigm)}
\item {\footnotesize Exploiting abstraction and symmetry}
\item {\footnotesize Using induction to reason about systems with many 
similar processes}
\item {\footnotesize True concurrency and models based on partial orders }
\item {\footnotesize Extending model checking techniques to handle 
real-time programs}
\item {\footnotesize Model checking techniques for the mu-calculus}
\item {\footnotesize Model checking for security and electronic commerce 
protocols.}
\end{enumerate}


\item  {\normalsize 80-810 Logic and Computation Seminar }
%M. Simons
%Tu 1:30-3:50
%Room TBA
%9 - 12 units
%Texts: TBA
%(F96, F97, F98, F00)

{\footnotesize This seminar is intended for Logic and Computation Majors and 
beginning graduate students. It covers, on the one hand, a particular 
topic in logic, computation, or methodology; on the other hand, it 
introduces students to current work in the department by "guest lectures" 
of faculty members. }

\item{\normalsize 80-811 Thesis Seminar}
%Spring 9-12 units

{\footnotesize This course provides a forum for the presentation and
detailed discussion of research done by students, be they
undergraduates working on their Senior Thesis or graduate students
engaged with their M.S.  Thesis.}

\item {\normalsize 15-812 Semantics of Sequential and Parallel Programs}
%Instructor: Stephen Brookes
%MW 10:30 - 11:50
%Wean 4615A
%12 units
%(F00)

{\footnotesize This course introduces foundational concepts and techniques of programming language semantics.  As a ``starred'' course it can be used by CS graduate students to fulfill their PL core requirement.  We focus on  two of the most successful styles of semantic description:  denotational and operational semantics.  We introduce semantic models chosen to be as simple as possible while supporting compositional (syntax-directed) reasoning about program behavior.  We introduce techniques for reasoning about program correctness, for proving the correctness of a compiler, and we prove general laws of program equivalence.  We apply these techniques to a variety of non-trivial examples.

\noindent Topics:

\begin{enumerate}
\item Introduction
\begin{enumerate}
\item denotational and operational semantics
\item inductive techniques for reasoning about programs
\end{enumerate}

\item Sequential imperative programs
\begin{enumerate}
\item partial and total correctness
\item state transformation semantics
\item jumps and continuations
\item compiling to machine code
\item compiler optimizations
\end{enumerate}

\item Parallel imperative programs
\begin{enumerate}
\item safety, liveness, and deadlock
\item fairness assumptions
\item  shared-variable programs
\item communicating processes and dataflow networks
\item Kahn's Principle for deterministic networks
\item  trace semantics
\end{enumerate}

\item Sequential and parallel functional programs
\begin{enumerate} 
\item domains and continuous functions
\item recursion and fixed point theory
\item direct-style and continuation-style semantics
\item call-by-name and call-by-value
\end{enumerate}
\end{enumerate}

\noindent Requirements:  Grading will be based on homeworks, a midterm examination, and a final examination.  Homeworks will be assigned regularly, with answers made available promptly.

\noindent References:  Lecture Notes will be handed out on a regular basis. 

\noindent Texts:  (suggested background reading)  Reynolds, {\it Theories of Programming Languages}, Cambridge University Press, ISBN 0-521-59414-6 (1998); Winskel, {\it The Formal Semantics of Programming Languages:  An Introduction}, MIT Press, ISBN 0=262-23169-7.}

\item{\normalsize 80-812 Seminar on Causation}
%Offered Intermittently
%9-12 units

{\footnotesize This course explores the foundations of causation. It
examines how causal claims connect to both probability and to
counterfactuals. Under a variety of background assumptions, and a
variety of senses of "reliable", we will examine which causal
inferences can be made reliably. We will also examine recent
developments in statistics and artificial intelligence relating to
causal inference.}

\item  {\normalsize 80-813 Seminar on the Foundations of Mathematics} 
%Instructor:  J. Avigad and J. Cummings
%Room TBA
%9 - 12 units
%(S 97, F00)

{\footnotesize The seminar focuses on mathematical and logical work,
important for foundational issues that may range from the detailed
presentations of ``constructive'' consistency proofs through
conceptual analyses of central mathematical concepts to the discussion
of ontological and epistemological issues.}


\item  {\normalsize 15-814 Type Theory for Programming Languages. }
%formerly 15-834 Semantic Foundations of Functional Programming
%(Robert Harper)
%Time: TR 10:30 - 11:20 am
%Location: Wean Hall 5409A  
%Units: 12
%(F96, F99)


{\footnotesize This is an introductory course on the design and analysis of 
type systems for programming languages.  The focus of the course is on the 
use of typed lambda-calculi and operational semantics as models of programming 
language concepts.  These models are applicable to the design, analysis, and
implementation of programming languages.}

{\footnotesize Prerequisites: The course is appropriate for first- or second-
year graduate students, especially those interested in further research in 
programming languages.  Advanced undergraduates will be admitted of the 
instructor.  Students are assumed to be familiar with ML and Java; 
programming assignments will be carried out in ML.  Background in logic, 
semantics, and compilers is helpful, but not essential to the course.}

{\footnotesize Texts: Readings will be drawn from the following sources.}

{\footnotesize \begin{enumerate}
\item John C. Reynolds, Theories of Programming Languages.  Cambridge Univ.
Press, 1999.
\item Glynn Winskel, The Formal Semantics of Programming Languages, MIT 
Press, 1993.
\item John C. Mitchell, Foundations for Programming Languages, MIT Press, 
1996.
\item Marin Abadi and Luca Cardelli, A Theory of Objects, Springer-Verlag, 
1996.
\item Jean--Yves Girard, Proofs and Types, Cambridge University Press. 1989.
\end{enumerate}}

{\footnotesize Method of Evaluation:  Grades will be assigned on a pass/fail
basis.  Evaluation is based on class participation, bi-weekly homework 
assignments, and a final examination.  Students are expected to participate
in a note-taking cooperative.  }

{\footnotesize Probable Topics:  Inductive definitions; Static and dynamic
semantics; Type safety; Function, product, and sum types; Universal types 
and polymorphism; Existential types and data abstraction; Recursive types;
Object types; Subtyping, Equational reasoning; Type inference and 
unification.}

{\footnotesize This course fulfills the core unit requirement for 
programming languages.}        

\item {\normalsize 80-814 Seminar on the Philosophy of Science}
%Spring 
%9-12 units

{\footnotesize A graduate level, critical review of standard issues in
the philosophy of science Topics will include determinism,
predictability, confirmation, probability, causation, lawlikeness,
explanation, the aims of science, the content of scientific claims,
the rationality of belief in scientific claims.}


\item{\normalsize 80-815 Seminar on the Foundations of Statistics:}
%Spring (S97, S98)
%9-12 units

{\footnotesize The seminar focuses on some single important
foundational work, or body of work, and investigates it and related
research from a contemporary point of view.  For example, when
Savage's Foundations of Statistics is the course's focus, the class
goals include understanding how Bayesian decision theory differs from
its rivals, and understanding where Savages position is located within
the current Bayesian program.  Other seminal thinkers whose writings
have served as the course's focus in different terms include,
R.A.Fisher, Harold Jeffreys, J.Neyman, and A. Wald.  Prerequisities:
This is primarily a graduate level class.  Instructor permission is
required for undergraduates .}

\item {\normalsize 15-816 Linear Logic}
%Frank Pfenning
%Spring 1998
%Units 1 CS core unit
%(S98)

{\footnotesize The course provides an introduction to linear logic
with an emphasis on its applications in computer science.  This
includes the theory of functional, logic and imperative programming
languages.  We will also develop a linear type theory which will serve
as a meta-language in which the theory of programming languages with
state can be formalized effectively.  We hope that an implementation
of the type theory (currently in progress) will be available for
practical experiments.}

{\footnotesize Text:  Course notes will be handed out.}

{\footnotesize Prerequisites:  General familiarity with functional programming
would be helpful.  Interested undergraduates are welcome, but require 
permission by the instructor.}

{\footnotesize Comment:  Course grades will be based on a combination of 
homework and a term project.}

\item{\normalsize 15-819(A) Advanced Topics in Programming Languages:
Functional Languages with Parametric Polymorphism and Linear Typing}
%John Reynolds
%Units: 12
%(F97)

{\footnotesize The course will center around the polymorphic linear
lambda calculus (PLLC), covering: functor-category and relational
models programming in PLLC implementing PLLC translating Algol-like
languages into PLLC parallelism and concurrency in PLLC problems with
passivity.}

{\footnotesize Text or References:  There will be no text, but papers and
course notes will be used extensively.}

{\footnotesize Prerequisite:  CS 711 or equivalent.}

{\footnotesize Comment:  No CS core credit.}

\item{\normalsize 80-819 Seminar on Propositional Attitudes and Dynamic 
Semantics}
%Organizers:  H. Arlo-Costa  and Tim Fernando
%Mondays 4:00-6:00 pm
%Room: SH 422
%Variable Units 9-18
%(S98)

{\footnotesize Bertrand Russell called a variety of verbs like
`think', `doubt', `see', and `hear', propositional attitude verbs,
because they seem to express some attitude that a person might have
with respect to a proposition.  Propositional attitudes provide an
excellent test against the ontological and epistemological limitations
of semantics.  The seminar starts with a review of the treatment of
propositional attitudes in the writings of Frege, the Oxonian school
of `ordinary language', and some members of the post-Carnapian
American tradition like Quine, Davidson, Kaplan and Kripke.  Then we
will focus on two recent semantic theories: Discourse Representation
Theory (DRT) and Update Semantics.  Although these theories seem to
offer an ideal theoretical framework for propositional attitudes (due
to their cognitive nature), they have been only recently applied in
this field.}

{\footnotesize The bulk of the seminar will be devoted to presenting
the theories in a self-contained way, to comparing them with the
approaches defended by Frege and Montague, and to considering how they
can be applied to treat propositional attitudes.  We will compare them
also with other cognitive approaches in semantics.  Although we might
consider other attitudes in passing, we will focus on the analysis of
belief and conditional belief.}

\item {\normalsize 15-820 Categorical Logic Seminar}
%Instructor: Steve Awodey
%W 3:00 - 5:20 pm
%Room TBA
%12 units
%(F00)

{\footnotesize This course focuses on applications of category theory in logic and computer science.  A leading idea is functorial semantics, according to which a model of a logical theory is a set-valued functor on a category determined by the theory.  This gives rise to a syntax-invariant notion of a theory and introduces many algebraic methods into logic, leading naturally to the universal and other general models that distinguish functorial from classical semantics.  Such categorical models occur, for example, in denotational semantics, where the lambda-calculus is treated via the theory of cartesian closed categories.  Similarly, higher-order logic is treated categorically by the theory of topoi.}

{\footnotesize \noindent Prerequisites:  80-413/713 Category Theory or equivalent.}

{\footnotesize \noindent Comment:  The course will begin with a 3 week refresher of basic category theory - CS students can start after Immigration by reviewing on their own.}

\item{\normalsize 80-820 Seminar on Categorical Logic}
%Alternate Years (Fall)
%9-12 units

{\footnotesize This course focuses on applications of category theory
in logic and computer science. A leading idea is functorial semantics,
according to which a model of a logical theory is a set-valued functor
on a category determined by the theory. This gives rise to a
syntax-invariant notion of a theory and introduces many algebraic
methods into logic, leading naturally to the universal and other
general models that distinguish functorial from classical
semantics. Such categorical models occur, for example, in denotational
semantics. e.g. treating the lambda-calculus via the theory of
Cartesian closed categories. Similarly, higher-order logic is treated
categorically by the theory of topoi.  Note: this course will begin
with a 3 week refresher of basic category theory CS students can start
after immigration by reviewing on their own.

Prerequisite: 80-413/713 or equivalent}
 
\item {\normalsize 15-827 Security and Cryptography}
%Doug Tygar and Jeannette Wing
%W 1:00 - 3:20
%WeH 4601A
%12 units
%(S98)

{\footnotesize As use of the Internet has exploded, so
has interest in security. This course will cover a range of topics on
computer security including private and public key cryptography,
authentication protocols, electronic commerce protocols, protocol
design principles, logics of authentication, and security policy. More
advanced topics include elliptic curve cryptography, zero-knowledge
proofs, anonymous cash, electronic voting, electronic auctions,
watermarking, trust management, and formal tools (such as model
checkers and theorem proving) for reasoning about security. We will
look at many of these topics from both a systems viewpoint, e.g.,
identifying typical classes of design flaws in authentication
protocols, and a more formal viewpoint, e.g., verifying that an
authentication protocol satisfies certain desirable properties. If
time, we will look at code-level security issues such as addressed or
raised by Java JDK, Active-X, Active Networks, software
fault-isolation, and proof-carrying code.}

{\footnotesize This course is intended to appeal to a wide range of
students: people interested in state of the art cryptographic
techniques, in designing new applied cryptographic protocols, in
building systems using ``off the shelf'' security protocols, or in
using mechanical tools for reasoning about security protocols.
Students interested in pursuing research in any aspect of security are
especially encouraged to enroll.}

{\footnotesize Prerequisites: There are no formal prerequisites to this
course but we assume students have had the equivalent of an
undergraduate operating systems course, an undergraduate logic and
discrete mathematics course, and some familiarity with distributed
systems.}

{\footnotesize Textbook and Readings: Handbook of Applied Cryptography
by Menzes, Oorschot, Vanstone Papers distributed by instructors}

\item {\normalsize 15-850(B) Advanced Topics in Theory: Domain Theory}
%Instructor: Dana Scott
%Time: TBA
%(F96)

{\footnotesize The theory of domains has many applications in
programming-language semantics, computability theory, and recently in
measure theory and chaos. The course will offer a foundational
discussion of the idea building up to the solution of domain equations
and constructions of powerdomains and continuous algebras. Then there
will be a review of applications as time permits.}


\item {\normalsize 15-851 Computation and Deduction} 
%(F96) 
%Frank Pfenning
%Time: tba
%Location: tba
%CS Credit: 1 core unit
%Units: 12

{\footnotesize We will explore the theory of programming languages using
deductive systems. We will use such systems to specify, implement, and
verify properties of functional, logic, and imperative programming
languages. The deductive approach to the specification of programming
languages has become standard practice, and one of the goals of this
course is to provide a good working knowledge of how to engineer such
language descriptions. Throughout the course we will use Elf (and an
extension based on linear logic) as a uniform meta-language in which
we can express specification, implementation, and meta-theory of
the object languages we are considering. An implementation of Elf
and examples will be available on-line for experimentation.}


\item {\normalsize 15-859(A) Complexity Theory}
%Steven Rudich
%MW 1:30 - 2:50
%WeH 4515A
%12 units
%(F98)

{\footnotesize This is a graduate course the study of how much of a
resource (such as time, space, parallelism, or randomness) is required
to perform some of the computations that interest us the most. In a
standard algorithms course, one concentrates on giving resource
efficient methods to solve interesting problems. In this course, we
concentrate on techniques that prove or suggest that there are no
efficient methods to solve many important problems.}

{\footnotesize We will develop the theory of various complexity
classes, such as P, NP, co-NP, PH, \#P, PSPACE, NC, AC, L, NL, UP, RP,
BPP, IP, and PCP. We will study techniques to classify problems
according to our available taxonomy. By developing a subtle pattern of
reductions between classes we will suggest an (as yet unproven!)
picture of how by using limited amounts of various resources, we limit
our computational power.}

{\footnotesize It has become increasingly obvious that proving even a
small part of this world picture true (or false) would be a major
mathematical achievement. For example, one part of this picture is
that P does not equal NP. The question of the equality of these two
classes was originally posed in a letter from Kurt G\"{o}del to J. Von
Neumann; it is one of the most important problem in all of
mathematics. We will study some of the remarkable lower bounds which
have been proved in the hopes of making progress on these central
issues. We will see that the solution to these questions will require
techniques unlike any that are currently known.}

{\footnotesize One especially interesting aspect of our study will be
the variety of roles played by randomness. It helps in all aspects of
complexity theory: finding efficient algorithms, finding reductions
between problems, and proving that certain problems have no efficient
algorithms in restricted models.  Another point worth mentioning is
that this seemingly pessimistic theory of what is impossible is what
makes two highly practical fields of computer science possible at all:
pseudorandom number generation and cryptongraphy. These fields return
the favor by suggesting what is true and what is provable in
complexity theory.}

{\footnotesize Prerequisites: Mathematical maturity. Basic knowledge
of some undergraduate mathematics: Linear Algebra, Probability, and
Number Theory. For example, you should know: (1) what the basis of a
vector space is, (2) that the expectation of random variable is
additive, and (3) $a^{p-1} =3D 1 $ mod $p$, for prime $p$. Familiarity
with the notion of algorithm and big O notation. Knowledge of Turing
machines is helpful.}

\item {\normalsize  15-859(B) Computational Projective Geometry}
%Dana Scott
%TR 9:00 - 10:20
%WeH 4615A
%12 units
%(F98)

{\footnotesize Symbolic mathematical computation has developed to a
stage where algebraic and numerical computation can be combined with
computer-generated graphics to add dynamical depth to the
investigation of many classical topics. This course will treat plane
projective geometry in an algebraic implementation mechanized through
the Mathematica symbolic computation software, with the objective to
end up with the projective classification (over the complex numbers)
of cubic curves.}

{\footnotesize Aside from presenting the necessary theoretical
material, attention will be given to how symbolic algebra is applied
to such topics. Previous familiarity with Mathematica is desirable,
but special help sessions will be arranged for students not yet adept
with the software.}

{\footnotesize There will be two one-and-a-half-hour lectures per week
and two laboratory sessions.}


\item{\normalsize 15-885(A) Advanced Topics in AI/Computational Science: 
Computational Scientific Discovery (Crosslisted as 80-514/814 - Philosophy  
of Science Seminar)}
%Instructor: Valdes-Perez (valdes@cs)
%TR 1:30 - 2:50
%WeH 3412
%Credit: 1 Core unit, 12 Univ. Units
%S97

{\footnotesize This course surveys those tasks of scientific reasoning
that have been automated in computer programs, the general methods
that have been used, and what new analogous tasks in the sciences
might be attempted.  The emphasis is on high-end tasks: tasks that
ordinarily are called creative.}

{\footnotesize As introductory background, we will review (1)
characteristics of scientific research as carried out in practice, (2)
some fundamental concepts and principles of scientific inference, and
(3) methods of AI that have been most applied to scientific
discovery.}

{\footnotesize Then, a series of case studies will be described from a
variety of fields, including biology (cell \& molecular), chemistry,
physics, medicine, and social science.  Discussions will center on (1)
the context of the scientific task, (2) the computational method that
is used, and (3) the role of prior knowledge and how it is handled.}

{\footnotesize Finally, we will cover generalizations from these case
studies, research methodology, the interface between scientist and
discovery programs, and philosophical issues.}

{\footnotesize Course Requirements: If you are taking this course for
credit, you will be expected to (1) do the regular homework
assignments, which will include some hands-on experience with programs
and maybe a little programming, (2) pass a midterm and final exam, and
(3) keep a notebook and record questions that arise during your
reading prior to class sessions. These questions will be raised and
discussed during class.}

{\footnotesize Prerequisites: Graduate student status in SCS,
Philosophy, MCS or consent of the instructor.  Non-CS students should
have some programming experience and appropriate undergraduate
mathematics.  No specific knowledge of the various sciences dealt with
is needed.}

\newpage
{\footnotesize Text:}
\begin{enumerate}
\item[(1)] {\footnotesize J. E. Oliver.  The Incomplete Guide to the Art 
of Discovery.  Columbia University Press, New York, 1991.}
\item[(2)] {\footnotesize W. C. Salmon. The Foundations of Scientific 
Interference. University of Pittsburgh Press, 1996.}
\item[(3)] {\footnotesize P. Langley, H. A. Simon, G. L. Bradshaw, and J. 
M. Zytkow.  Scientific Discovery:  Computational Explorations of the Creative 
Processes.  MIT Press, Cambridge, Mass., 1987.}
\item[(4)] {\footnotesize Other reading will consist of the primary 
literature and shorter selections from books.}
\end{enumerate}

{\footnotesize Tentative Outline of Course:}


{\footnotesize \noindent Introduction (1 day)\\
Background\\
Textbook vs. Frontier Science (2 days)\\
Concepts of Scientific Inference (3 days)\\
Heuristic Search and Representations (3 days)\\
Scientific Discovery Programs\\
Historical modelling (2 days)\\
Early programs (2 days)\\
Midterm Examination (1 day)\\
Recent Programs (14 days)\\
Generalizations, Reserch Methods, etc. (3 days)\\
Final Examination}

\item  {\normalsize 21-905 Seminar on Automated Theorem Proving }
% F96 S94 F94 S98 Peter Andrews and Wilfried Sieg
%Time: TBA
%Variable Units 6-18
%(F95, S98)

{\footnotesize The seminar will probably meet once a week.  The
purpose of this seminar will be to help and encourage the participants
to gain greater familiarity with certain parts of the literature on
automated theorem proving, to become better acquainted with work on
theorem proving at CMU and elsewhere, and to acquire the background on
which future developments may be built.  Choice of topics will be
influenced by the interests of the participants.}
}
\end{itemize}

\noindent The following graduate or general colloquia and seminars were 
conducted in recent years.

\begin{itemize}

\item  Logic Colloquium

\item  Philosophy Colloquium

{\footnotesize The above two colloquia are continuous and often present
internationally renowned invited speakers. }

\item  {\normalsize Seminar on Philosophy of Mathematics }

\item  {\normalsize Seminar on the Foundations of Statistics} %(S 90)  

{\footnotesize We study foundational questions in expected utility
theory -- questions dealing with the axiomatization, representation,
and measurement of probability and utility -- with attention to
applications in statistical decision theory. Also, we contrast several
departures from expected utility.  These include economic and
psychological theories of preference without the ``independence''
(Savage's Sure-Thing) axiom and theories which do not require
comparison (``ordering'') between all pairs of acts. To what extent do
these departures from expected utility theory provide a rationale for
``classical'' (non -- Bayesian) statistical practices? }

\item  {\normalsize Principles of Programming Seminar }

{\footnotesize The POP Seminar is a weekly meeting of the Principles of
Programming group, with presentations from its members or talks given by
visitors. }

\item  {\normalsize Seminar in Logic and Computability I: Formal learning
theory}
%(F 93)
%(Kevin Kelly)
\end{itemize}

\noindent
In the past decade, the Carnegie Mellon Logic Community has organized the
following conferences and workshops:

\begin{itemize}
\item  Mid-Atlantic Mathematical Logic Seminar (Feb 90)
\item  Annual Meeting of the Association for Symbolic Logic (Jan 91)
\item  International Conference on Mathematical Foundations of Programming
Semantics (March 91)
\item  Mid-Atlantic Mathematical Logic Seminar (April 93)
\item  Mid-Atlantic Mathematical Logic Seminar (March 95)
\item  Modern Mathematical Thought, Its History and Philosophy (Joint with
the University of Pittsburgh) (September 95)
\item  Mid-Atlantic Mathematical Logic Seminar (April 97)
\item Modern Mathematical Thought II:  Historical and Philosophical 
Approaches (Joint with the University of Pittsburgh) (May 98)
\item Graduate Conference in Logic \& Philosophy of Science (Joint with  
the University of Pittsburgh) (March 99)
\end{itemize}

%  THE FOLLOWING SECTION IS COMMENTED OUT IN THE PUBLIC
%  VERSION OF THIS DOCUMENT
%
%  \vspace*{1cm}
%  \newpage
%
%  ADMINISTRATIVE SECTION, MOVED TO COVER LETTER
%  {\large\bf
%  \section{Program organization}
%  }
%  
%  The Program is an {\it educational} entity, not an
%  independent academic unit in the university.
%  The Program's faculty affiliation is with
%  one or more of the Mathematics
%  Department, the Philosophy Department, and the
%  School of Computer Science.
%  Faculty's responsibilities, offices, and clerical support
%  are not affected by the program.
%  
%  The degree requirements for each track are determined
%  by the track's home academic unit.  
%  
%  The Program faculty select a {\it Coordinating Committee}, with
%  representatives from all three departments, which has the
%  responsibility of overseeing the program.

\vspace*{1cm}

\newpage

\section{{\protect\large {\bf Degree and requirements}}}

\subsection{General requirements}

\indent
The Program is an {\it educational} entity, not an independent
academic unit in the university. Each student in the program will be
enrolled in the Department of Mathematical Sciences, the Philosophy
Department, or the Computer Science Department, and will be awarded a
degree of {\it Ph.D.\ in Pure and Applied Logic} through this home
academic department upon successful completion of the program.

Each student in the Program will follow a {\it track} corresponding to his
or her home academic department. The degree requirements are generally
determined by the tracks. All tracks require substantial course work in
logic and logic-related subjects, and the completion of a Ph.D.\ thesis
consisting of a scholarly exposition of substantial original research.


The courses required of each student will be determined by her or his
advisor, within the guidelines of the track requirements. Among these
may be courses offered by other Carnegie Mellon departments, or in
some cases by other academic institutions.

The procedure for completing a thesis is determined by the regulations
of the home college for each track. Work on the thesis will be
supervised by the student's advisor, and reviewed by the Logic Program
faculty, as well as by the home department faculty. Progress on a
thesis will follow the milestone and timetable customary for the home
department. (For example, CS students will present a Thesis Proposal,
produced under the supervision of the student's advisor.)

On completion of a thesis, the student will present a Thesis Defense.
The subject of this oral examination is the thesis and related topics.
The examiners are usually, but not necessarily, the members of the
Thesis Committee plus a non-departmental committee member as required
by university regulations. This examination is public and must be
announced throughout the university.

Students are also expected to informally participate in the activities of
the Carnegie Mellon Logic community, such as relevant seminars and 
colloquia.

\newpage

\subsection{Track requirements and evaluation in Computer Science}

The course requirements in the Computer Science track are:

\vspace{.15in}

\begin{enumerate}
%\item  
%\item
%A two semester course, {\it Introduction to Pure and Applied Logic},
%intended to provide an introduction to the fundamental
%issues, results, and techniques in Logic, in a unified perspective.
%The first part, {\it Formal languages and semantics,} is
%offered every Fall, and the second part, {\it Computability and Provability,}
%is offered every Spring.

\item  Five star courses, one from each of these five areas:  \\
Algorithms and Complexity, Artificial Intelligence, Computer Systems,
Programming Languages, and Software Systems.

\item  At least five additional courses or core units in Logic,
Logic-related areas, and other Theoretical Computer Science subjects.
At least two of these should be offered by the Department of Computer
Science.  Since Computer Science Ph.D. students are restricted to
taking the equivalent of at most one elective course (out of the
required three) outside of SCS, in special cases, students may
petition to have a second elective chosen from outside SCS.
\end{enumerate}

Incoming students in the Computer Science track will participate in
the Immigration Course.   Students are expected to begin involvement 
in research during their first year, to complete their course requirements by 
the end of their second year, to satisfy the programming and communications 
skills requirements by the end of their third year, to present a Thesis 
Proposal during the third year, and to satisfy all degree requirements by the 
end of their fifth year.  Students are expected to serve as teaching 
assistants for at least two semesters.    

A student who has completed the course requirements, has completed the skills
requirements, and has finished at least one of the two required teaching 
semesters may petition the faculty for a Master's degree, which may be 
granted at the faculty's discretion.

Computer Science/PAL students will be evaluated each semester at the regular
Computer Science ``Black Friday'' meeting.  Each student's advisor will present
an evaluation of the student's progress at this meeting.

\newpage

\subsection{Track requirements and evaluation in Mathematical Sciences}


The requirements for students in the Mathematical Sciences track (which 
are compatible with the requirements for other Mathematical Sciences
graduate students) are:

\begin{enumerate}
\item  A one or two-semester course in logic including proofs of the
completeness and incompleteness, compactness, and undecidability theorems.
Students may fulfill this requirement by taking Mathematical Logic I \& 
II, or other suitable courses. An appropriate choice will be made in
consultation with the student's advisor. Of course, some students admitted
to the program may already have fulfilled this requirement. They may still
choose to take one or more of these courses to refresh or enhance their
knowledge.
\item  Additional courses in Logic and Logic-related areas. At least five
courses shall be taken at Carnegie Mellon to fulfill requirements 1 and 2.
\item  The following Mathematics courses are required:
 
\begin{tabular}{lll}
21-610 & Algebra I \vspace{2mm} &  \\ 
21-620 & Real Analysis (half-semester)\vspace{2mm} & \\
21-621 & Introduction to Lebesgue Integration (half-semester) \vspace{2mm} 
& 
\\ 
21-640 & Functional Analysis \vspace{2mm} &  \\ 
21-651 & General Topology \vspace{2mm} & 
\end{tabular}

\item  The student will take additional courses to achieve a full course
load of at least three courses per semester. Advanced students often sign 
up for Reading and Research.

\item  Another requirement is the oral Qualifying Examination. 
%(which must be completed by the end of the third semester following
%admission to candidacy) The purpose of this examination is to establish the 
breadth and depth of the student's knowledge, especially in areas related to 
the student's thesis research. The examination will have a major and a
minor topic. The major topic will be the area of logic in which the
student expects to do thesis research, and the minor topic should be a
subject relevant to, but not closely related to, the research area.
The minor topic may be chosen from the fields of mathematics, computer
science, or philosophy, and need not be (but may be) a field of logic.
The format of this examination is determined by the committee; it is
common to have a brief presentation by the student at the beginning of
the examination. The content of the examination must be agreed upon by
the student and the committee not less than two months prior to the
date it is scheduled and a document describing the content submitted
to the Department. The examiners may choose to require the student to
repeat all or part of the examination. An unsatisfactory performance
on the second examination normally leads to dismissal. In exceptional
cases the committee may choose to make part of the examination written
rather than oral.
\end{enumerate}

\newpage

\subsection{Track requirements and evaluation in Philosophy}

The Philosophy Department's Ph.D. program in Logic, Computation, and
Methodology has three distinct emphases:

(1) {\it Specialized Logical Training\/} (with options towards research 
work in Philosophy of Science or in Mathematical Logic);

(2) {\it Broad Philosophical Education\/} (with an option to concentrate
in a particular area -- for students with a substantial background in
Philosophy);

(3) {\it Original Research} (students are encouraged to pursue research
topics as early as possible; an M.S. thesis is required and should be
submitted no later than the end of the second year).

The program requires three years of course work, with an M.S. thesis
at the end of the second year. The normal (full-time) graduate course
load in Philosophy is 4 courses/term.\footnote{ Graduate courses at
CMU typically carry 12 units each. The University requires a minimum
of 36 units/term for status as a full-time graduate student.} Of the
24 courses in the first three years, 12 are constrained (as indicated
below) and 12 are open electives, chosen in consultation with the
Director of Graduate Studies. For good standing in the program, the
student must pass all required courses with a grade of B or better,
achieve mostly grades better than B+, and defend the M.S. thesis
successfully.

Already the second year offers a number of choices and asks the
student to do some original research to be formally presented as an
M.S. thesis at the end of the (second) year. In consultation with the
department and following a comprehensive evaluation at the end of the
second year, the student sets up research plans for the third year.
During the third year, the student undertakes work that is preparatory
for a dissertation and ends in a prospectus for a thesis. A
dissertation committee is set up by the end of that (third) year. The
fourth year extends the thesis research and is devoted solely to that
work.

The 12 Ph.D. required/constrained courses are as follows:

\begin{center}
\begin{tabular}{rll}
 & Logic and Computability & 80--610 \\ 
 & G\"{o}del and Computability & 80--710 \\ 
 & Descriptive Set Theory & 80--711 \\ 
 & Probability and Artificial Intelligence & 80--611 \\ 
 & Minds, Machines, and Knowledge & 80--600 \\ 
 & Logic and Computation Seminar  \footnotemark[2] & 80--810 \\ 
 & Logic and Comp. Research Symposium \footnotemark[3]  & 80--811 \\ 
 & 1 of (Phil. Science/Math./Logic) & 80--620/612/613 \\ 
 & 1 of (Proof Theory; Set Theory/Model Theory; & 80--713; 
21--602/603;**--*** \\ 
& another advanced Logic course) & \\ 
 & 2 other advanced Philosophy courses &  \\ 
 & 1 (graduate level Computer Science, or & 15--*** \\ 
& Computational Linguistics course) & 80--480/481/482/483/484 \\ 
&  & 
\end{tabular}
\end{center}
\footnotetext[2]{To be taken in the Fall of the 1st year.}
\footnotetext[3]{To be taken in the Spring of the  2nd year.}

Logic and Computability and G\"{o}del and Computability can be replaced 
by other courses in Mathematical Logic for sufficiently well-prepared 
students. The advanced Philosophy courses may be taken at the University 
of Pittsburgh---in either the Department of Philosophy or the Department 
of History and Philosophy of Science.

\addtocounter{footnote}{2}

Also, each Ph.D. student is required to serve as a teaching assistant
or instructor for at least two courses. This requirement is important
for students who intend to pursue an academic career; in case the
student serves as an instructor, e.g., for a summer course, there will
be supervision by a faculty member. Foreign students have their
teaching options limited by their English language skills, as assessed
by the ESL Center. Each foreign student whose native language is not
English is required to take a proficiency exam (both written and oral)
run by the ESL Center. \footnote{Students who need additional English writing 
skills should take ``academic writing'' no later than the second year in 
connection with their M.S. thesis.}

Below is a ``typical'' schedule for the first three years, with
several electives taken in \underline{Mathematical}\newline
\underline{Logic}. At the bottom of this chart you will find four
other families of electives, reflecting specializations in:
\underline{Computational Linguistics}; \underline{Statistical Methodology}; 
\underline{Decision, Games, and Learning}
\newline \underline{Theory}; and \underline{Foundations of Cognitive 
Science}. Students are strongly encouraged to pursue an interdisciplinary 
specialization, as these examples point out. The schedule is also flexible 
to allow for differences in the backgrounds and individual needs of students. 


\begin{center}
{\bf FIRST YEAR}

\begin{tabular}{p{1.5in}p{4.5in}}
FALL: & Logic and Computability  \\ 
& Logic and Computation Seminar \\ 
& Minds, Machines, and Knowledge \\ 
& Elective \\[16pt] SPRING: & G\"{o}del and Computability  \\ 
& Probability and Artificial Intelligence \\ 
& Advanced Philosophy Elective \\ 
& Elective \\ 
\end{tabular}
\end{center}

%\vspace*{.25in}

\begin{center}
{\bf SECOND YEAR}

\begin{tabular}{p{1.5in}p{4.5in}}
FALL: & Descriptive Set Theory \\ 
& \underline{Proof Theory}\footnotemark[5] \\ 
& Philosophy of Science/Mathematics/Logic Elective \\ 
& Elective \\[16pt] 
SPRING: & Logic and Computation Research Symposium \\ 
& Directed Research for M.S.-thesis \\ 
& Advanced Philosophy Elective \\ 
& Elective \\ 
& 
\end{tabular}
\end{center}

\footnotetext[5]{Note: Many of the advanced logic 
courses (e.g., Model Theory, Proof Theory, and Set Theory) are offered 
only in a two-year cycle.}

%\vspace*{.25in}

\begin{center}
{\bf THIRD YEAR}

\begin{tabular}{p{1.5in}p{4.5in}}
FALL: & \underline{Set Theory} \\ 
& Computer Science Elective \\ 
& Directed Research towards Ph.D. Prospectus \\ 
& Elective \\[16pt] 
SPRING: & \underline{Model Theory} \\ 
& Directed Research towards Ph.D. Prospectus \\ 
& Elective \\ 
& Elective \\ 
&
\end{tabular}
\end{center}


%\vspace*{.25in}

\newpage

\begin{center}
{ILLUSTRATIVE SPECIALIZATIONS}

\vspace{.15in}

\begin{tabular}{ccc}
\underline{Computational Linguistics} & \phantom{0000000} & \underline{%
Statistical Methodology} \\ 
Ling. Theory & \phantom{0000000000} & Automated Discovery \\ 
Ling. Basis for NLP & \phantom{0000000000} & Foundations of Statistics \\ 
Form. Semantics of NLP & \phantom{0000000000} & Econometrics \\ 
Algorithms for NLP & \phantom{0000000000} & Statistical Modeling \\ 
Information Retrieval & \phantom{0000000000} & Time Series Analysis
\end{tabular}
\end{center}

\vspace*{.3in}

\begin{center}
\begin{tabular}{ccc}
\underline{Decisions, Games \& Learning} & \phantom{0000000} & 
\underline{%
Foundations of Cognitive Science} \\ 
Game Theory & \phantom{0000000} & Psychoanalysis \\ 
Formal Learning Theory & \phantom{0000000} & Philosophy of Mind \\ 
Strategic Games \& Decisions & \phantom{0000000} & Neural Circuits \\ 
Economics of Uncertainty & \phantom{0000000} & Language \& Thought \\ 
Choice \& Decisions & \phantom{0000000} & Brain Development \& Cognition
\end{tabular}
\end{center}

\vspace*{.30in}

\begin{center}
{\large *}\hspace*{.25in}{\large *}\hspace*{.25in}{\large *}
\end{center}

\newpage

%1994-1995 Philosophy requirements
%\indent
%The program has three distinct emphases:
%\begin{enumerate}
%\item Specialized logical training (with options towards research work in
%philosophy of science or in mathematical logic);
%\item Broad philosophical education (with an option to concentrate in a
%particular area -- for students with a substantial background in
%philosophy);
%\item Original research (students are encouraged to pursue research 
%topics
%as early as possible; an MS-thesis is required and should be submitted
%no later than at the end of the second year).
%\end{enumerate}

%The program requires three years of course work.  Already the second
%year offers a number of choices and asks the student to do some original
%research to be formally presented as an M.S. thesis at the end of the
%year.  In consultation with the department and following a comprehensive
%evaluation at the end of the second year, the student sets up research
%plans for the third year.  (For good standing in the program the student
%must pass all required courses with a grade of B or better and must
%defend the M.S. thesis successfully.)   During the third year, the
%student undertakes work that is preparatory for a dissertation and ends
%in a prospectus for a thesis.  A dissertation committee is set up no
%later than the end of that year.  The fourth year extends the thesis
%research and is devoted solely to that work.  

% Each student is required to serve as a teaching assistant or instructor
%for at least two semesters.  This requirement is parti-cularly important
%for students who intend to pursue an academic career; in case the
%student serves as an instructor, e.g., for a summer course, there will
%be close supervision by a faculty member. 
% Below is a "typical" schedule. In particular, the courses of the logic
%core can and, for some students, must be taken in a different order,
%since Model Theory, Proof Theory, and Set Theory are offered only in a
%two year cycle.  The schedule is also flexible to allow for differences
%in the backgrounds and individual needs of students. 

%\begin{center}
%\begin{tabular}{||rl|rl||} \hline
%\multicolumn{4}{||c||}{\raisebox{-1mm}{\Large\bf First Year}}\\ \hline
%\multicolumn{2}{||c|}{\bf Fall} & \multicolumn{2}{|c||}{\bf Spring}\\ \hline
%80-710 & Logic \& computability I &  80-810 & Logic \& computabilty II \\ \hline
%& Logic Core I : & & Logic Core II : \\
%21-602 & Set theory &  80-711 & Recursion Theory \\ \hline
%80-703 & Minds, machines, and knowledge & 80-712 & Probability and artificial intelligence\\ \hline
%& Mathematics elective & & Mathematics or computer science elective\hspace*{-2pt}\\ \hline
%\multicolumn{4}{||c||}{\raisebox{-1mm}{\Large\bf Second Year}}\\ \hline
%\multicolumn{2}{||c|}{\bf Fall} & \multicolumn{2}{|c||}{\bf Spring}\\ \hline
%80-810 & Logic \& computation seminar I & 80-810 & Logic \& computation seminar II \\
%& & & \hspace{4mm}plus research for M.S. thesis\\ \hline
%& Logic Core III : & & Logic Core IV : \\
%80-816 & Proof Theory I  & 80-817 & Proof Theory II \\ \cline{1-2}
%& Philosophy of science, &  \multicolumn{2}{c||}{\it or}\\
%& \hspace{4mm}of mathematics, or of logic & 21-805 & Lambda Calculus \\ \cline{1-2}
%& Logic elective I &  \multicolumn{2}{c||}{\it or}\\ 
%& & & another advanced logic class\\ \hline
%\multicolumn{4}{||c||}{\raisebox{-1mm}{\Large\bf Third Year}}\\ \hline
%\multicolumn{2}{||c|}{\bf Fall} & \multicolumn{2}{|c||}{\bf Spring}\\ \hline
%& Directed research & & Directed research \\ \hline
%& Logic Core V : & & Logic Elective III \\ \cline{3-4}
%21-603 & Model Theory & & Philosophy Elective III \\ \hline
%& Philosophy elective II & & Elective in cognitive science\\ \cline{1-2}
%& Logic elective II & & \hspace{4mm}or linguistics \\ \hline
%\multicolumn{4}{||c||}{\raisebox{-1mm}{\Large\bf Fourth Year}}\\ \hline
%\multicolumn{4}{||c||}{Devoted solely to thesis work}\\ \hline
%\end{tabular}
%\end{center}

%{\bf REMARKS:}
%\begin{enumerate}
%\item Logic and computability I and II can be replaced by other courses in
%mathematical logic for sufficiently well-prepared students.

%\item The logic electives I-III can be taken in any of the departments
%supporting the program (possibly also, e.g., in statistics); they should
%be connected to the student's research interests.  In consultation with
%the department, the electives can be taken in the form of directed
%reading or research courses.

%\item To further advance their research interests students are encouraged
%to do directed reading and research under the guidance of individual
%faculty members; for first and second year students 80-990 is
%appropriate, for second and third year students 80-992.  These classes
%can replace, in consultation with the department, the philosophy
%electives I-III.

%\item Philosophy electives can also be taken at the University of
%Pittsburgh -- in either the Department of Philosophy or the Department
%of History and Philosophy of Science.
%\end{enumerate}

%The program asks for three years of general course work.  Already the
%second year offers a great variety of choices and asks the student to 
%do some original research to be formally presented as an M.S. thesis 
%at the end of the year.  In consultation with the
%department and following a comprehensive evaluation at the end of the
%second year, the student sets up plans for the third year.  (For good
%standing in the program the student must pass all required courses with
%a grade of B or better and defend the M.S. thesis successfully.)   
%During the third year, the student undertakes
%work that is preparatory for a dissertation and ends in a detailed 
%prospectus for a thesis.  A dissertation committee is set up no later
%than  at the end of that year. The fourth year extends the thesis
%research  and is devoted solely to thesis work. Each student is
%required to serve as a teaching assistant or instructor for at least two
%courses.  %%%%%

%The program schedule of courses in pursuing this program is flexible
%and depends on the background and interests of individual students.
%However, every student has to cover through the course work the four
%major areas of mathematical logic: model theory, proof theory,
%recursion theory and set theory. An example of a typical schedule is 
%given below. 
%\vspace{2mm}
%
%\begin{description}
%
%\item[{\it First year:}]  
%Students take (depending on their background) Logic \& Computability I
%and II or two more advanced courses in logic;  they should
%select one (theoretical) Computer Science course and one Mathematics
%course. Required Philosophy courses: (1) Minds, Machines, and Knowledge,
% (2) Probability and Artificial Intelligence, and (3) the Logic and
%Computation seminar.

%\item[{\it Second year:}]  
%Two courses in the major areas and at least two other
%logic-related electives are taken.  Required Philosophy classes: (1)
%Philosophy of Science or Philosophy of Mathematics, and (2) two
%courses in  the History of Philosophy.
%
%\item[{\it Third year:}]  
%Two courses in the remaining major areas are taken, one
%logic-related elective, and a directed reading course.  (The latter
%serves as a preparation for dissertation work and should end with a
%thesis prospectus.)  Required (Philosophy) classes: (1) 
%one course in Linguistics or Cognitive Psychology, (2) two courses in
%Ethics/Values/Decision Theory.
%\end{description}
%
%
%  PREVIOUS PHILOSOPHY TEXT
% \indent
% The program asks for three years of general course work, where
% already the second year offers a great variety of choices.
% In consultation with the department and following a 
% comprehensive evaluation at the end of the second year, the student sets
% up plans for the third year.
% During it, the student undertakes works that is preparatory for
% a dissertation and ends with a prospectus for a thesis.
% A dissertation committee is set up at the end of the third year.
% The fourth year is devoted solely to thesis work.
% 
% Each student is required to serve as a teaching assistant or
% instructor for at least two courses.
% 
% A typical schedule looks like this.
% In the FIRST year a student takes {\it Introduction to Pure and Applied Logic}
% and the {\it Logic and Computation} seminar.
% In addition, a (theoretical) Computer Science course and a Mathematics course
% should be selected.
% Required Philosophy courses are {\it Minds, Machines, and Knowledge} and
% {\it Artificial Intelligence}.
% 
% Two courses in the major area and at least two electives should be taken in 
%the
% SECOND year.  Required Philosophy classes are {\it Probability and Artificial
% Intelligence}, two courses in the History of Philosophy, and a course
% in Philosophical Logic.  
% 
% During the THIRD year students should take courses in the remaining two
% major areas, one additional elective, and a directed reading course.
% (The latter should serve as a preparation for dissertation work.)
% Required Philosophy classes are:
% {\it Philosophy of Science} or {\it philosophy of Mathematics,}
% on course in Linguistics or Cognitive Psychology, and a sequence of
% two courses in Ethics, Values, Decision Theory.

\newpage

\smallskip

\section{{\protect\large {\bf Admission and support}}}

\indent
Applications for admission are directed to the Admission Committee for the
Department of the applicant's preferred track. Applications must be
submitted on the forms supplied and include all the supporting material
indicated in the application package. An application must clearly state
interest in the Program in Pure and Applied Logic, and the Goal Statement
should spell out and explain the candidate's interests in and potential 
for doing research in Logic.

An application should be completed by Feb 1, including all records, GRE
scores, recommendation letters and any other required material, to assure
consideration by the track's Admission Committee.

Only one track should be addressed as a first choice. Applicants who
wish to be considered for a second track should address a letter to
the Admission Committee of their second choice track and mention that
fact in a cover letter with their main application. The second-choice
Admission Committee will consider such applications concurrently with
the main-choice Committee.

Admitted students are supported by their respective department,
and earn this support as required by that academic unit. Students are
treated as full fledged students within their home academic unit,
notwithstanding possible variance of their degree and support requirements
from those of fellow students in that unit.

\vspace{2mm}

Inquiries should be addressed to {\it one} of the following:

\begin{verse}
PhD Program in Pure and Applied Logic \\Graduate Admission Committee \\%
\makebox[1cm]{} Department of Mathematical Sciences \\\makebox[2cm]{} {\sc 
or} \\%
\makebox[1cm]{} Department of Philosophy \\\makebox[2cm]{} {\sc or} \\%
\makebox[1cm]{} Department of Computer Science \\Carnegie Mellon 
University %
\\Pittsburgh, PA 15213-3890 \\{\sc USA}
\end{verse}

E-mail (for any of the three departments) can be addressed to
logic@cs.cmu.edu.

\end{document}




