[UMN logo]

CSci 5980 and 8980, Spring 2022
Topics in Structural Proof Theory

Table of Contents

News Flash: Online discussion using Piazza

New Information

      05/02/2022

      03/23/2022

      03/17/2022

      03/01/2022

      01/17/2022

Contact Information

Brief Course Description

In 1935, Gerhard Gentzen introduced the natural deduction and sequent calculi as means for formalizing logical deduction and for investigating its structure. These calculi have turned out to have many applications in Computer Science: they have been useful in understanding computation based on the connections between proofs and programs; they have provided a foundation for using proof search as a means for computing; and they have constituted a unifying framework for mechanizing and automating theorem proving. The structure constituted by these calculi has also lead to a deeper analysis of logical notions, resulting, for example, in linear logic that encompasses classical and intuitionistic logic. In another direction, the calculi provide a means for studying the organization of deduction, an idea embodied in the notion of focusing. This course will expose the calculi and study some of their properties and applications.

Course Prerequisites

The main requirements for the course are mathematical maturity, an interest in computational issues, a desire to learn about formalized reasoning, and the capability to program in an advanced language like OCaml, Standard ML or Haskell. Prior exposure to deductive calculi will help but is not necessary; the course will discuss such calculi in detail so the main purpose of the prior exposure would be to confirm your interest in such discussions.

Sources for Course Materials

The lambda calculus, in its different varieties, runs a rich vein through any discussion of proof theory. Related to this course, it provides a language of expressions upon which logics are based and it also is a vehicle for representing proofs and proving properties about them. We will begin the course with a discussion of this calculus as a logical formalism. You may supplement my lecture slides with material from Lambda Calculus and Combinators: An Introduction by Hindley and Seldin; I saw a PDF version of the book on the web, but I don't know what the story is behind this. Our focus in the initial discussions will be on the untyped version of the calculus and we won't look at typed varieties in detail. However, for those interested in digging further, a good source may be the paper Lambda Calculus with Types by Barendregt. When I looked last, a couple of figures were not displaying properly in this version of the paper. If you get there and need the figure, let me know and I will provide it to you.

We will start our understanding of deductive calculi by reading Investigations into Logical Deduction, Gentzen's seminal paper on the topic. This paper was reprinted in two parts in the American Philosophical Quarterly, Volume I, Number 4 (1964). You should be able to get the paper through the University library. I will also post the two parts in the papers section of the resources for this course, to make things easier.

We will then read material from the (draft) monograph entitled Proof theory, proof search and logic programming by Dale Miller. There is an intertwining of the idea of logic programming and focusing in deductive calculi that this monograph is a good source for. It will provide an especially useful introduction also to linear logic, all of which constitutes a logic programming language under a suitable interpretation. There are other sources too, such as Girard's original paper and also the Stanford Encyclopedia of Philosophy entry on the topic that we could look at.

There are several other sources for material and, in keeping with the seminar nature of this course, these will evolve as the semester progresses. I expect, in particular, that you all will contribute papers to read, based on what you decide to do for your term paper. I will post links to these papers and, where reasonable, the papers themselves in the papers section of this web page.

One book that I should not fail to mention as an excellent source for many of the undercurrents in the subject is Girard's Proofs and Types.

Required Work and Grade Determination

This course will be run in seminar-style with the usual rules for participation. Regular attendance is expected. If you have to miss a class meeting, make sure to discuss this with me beforehand: absence is quite noticeable in a small class.

You will be required to read material periodically and the discussions in class will often be meaningful only if you have done the reading. This is therefore an important part of the course: non-engagement, resulting from not having done the necessary reading, will be considered bad form.

There will be some assignments in the initial part of the course, intended to ensure assimilation of the basic material. There will be 3 or 4 of these during the term, counting cumulatively for 30% of the credit.

The most important and, hopefully, most exciting, part of the work in the course will be an individualized term paper or project that you will undertake during the semester. In this part of the work, you will have to identify some topic related to deductive calculi, formalized reasoning or computational issues that are relevant to the focus of this course that you want to look at more carefully on your own. You should then identify a few papers to read on the topic, assimilate what you have learnt from them in a way that characterizes your understanding of the topic, present this understanding to the class and also write a term paper that embodies the understanding. The term paper may include original work but it does not have to. For example, it could be mainly an insightful survey of what you have learnt from the papers or it could contain the seeds for something original that you might continue to investigate after the course. The term "paper" may also be the description of a project, such as an implementation or formalization of something that you have learnt that is related to the focus of the course. Note, however, that even in this case, there must be something conceptually interesting in what you have done, it cannot simply be a coding exercise.

Some planning is needed to make sure you use this opportunity well. Towards this end, here is a timetable:

The presentation will count for 25% of the grade and the term paper for 35%. The remaining 10% will be reserved for class participation.

Note that while absence during my lectures may be overlooked on occasion, attendance during the presentations of your colleagues is mandatory.

Policies and Related Information

COVID-19 Specific Policies

The pandemic continues to affect us and there is even a new surge as the term starts. The University has a set of policies related to this that you can read about in the "recommended syllabus language." that has been put together by the Provost's office. Please read this document carefully and assimilate the information it provides.

The key things to note for this course is that the University requires that all students and instructors be vaccinated or have an officially sanctioned exemption, that masks that completely cover the nose and mouth be worn by everyone in any indoor space on campus and that anyone who is experiencing symptoms or has tested positive stay at home till it is deemed safe to interact with others in shared spaces. An issue that wasn't sufficiently emphasized in the early stages of the pandemic, to some extent because it wasn't understood well then, is the importance of using a high quality mask. Make sure to check the information being put out by the University now on this and also learn there how to get a mask of this kind.

Collaboration and Academic Honesty

Discussions are an important part of learning. For a seminar course like this one, they are the lifeblood. I am hoping to see a lot of it this semester and hopefully the availability of a Piazza page will stimulate this significantly. initially.

Even though we will be working together to enhance each other's understanding, and I expect to benefit from this myself, there are still times when the notion of academic honesty is relevant. Specifically, there will be times when you will have to submit work that you claim as your own and that I will need to use to assess your understanding and grasp of the subject matter of the course. This will be the case, for example, with solutions to homework problems and the term paper that you write. You can still discuss the homework problems but when you write up your solutions they must represent your own thinking; to be more blunt about this, the solutions you submit must not be copied from or generated from looking at someone else's solutions. The term paper you write will be based on reading papers that others have written. However, when you write a survey of what you have learnt, an assessment of the existing work and perhaps some new work and suggestions, this must all be reflective of your own thinking and must not be copies of something you have seen somewhere else. Moreover, any source that has influenced your thinking must be explicitly acknowledged; not to do so counts for plagiarism, one of the worst offenses in academice work.

By the time you take a special topics course, you should have all had enough experience with academia to know what is and is not acceptable behavior vis a vis academic honesty. If you have doubts or questions at particular points, you can talk to me about this; I say this because you will be doing some independent work in this course and that could bring up some specific new questions. I hate to have to say this but unfortunately past experience informs me that this is necessary even in a small class of mature graduate students: Violations of academic honesty are serious breach of faith and raise serious questions about suitability for academic work. They will therefore be reported to the Office of Community Standards and the department and they will incur penalties that include a failing grade in this course.

I sincerely hope, therefore, that this is the last time I have to say this kind of stuff in this course and I look forward to a stimulating semester filled with vibrant discussions.

Appropriate Use of Class Notes and Course Materials

Material that is made available to the class during the term, such as notes and videos prepared by the instructor and solutions that may be provided to problems are meant only for the participants in the course and for the purpose of enhancing learning. All these materials remain the intellectual property of the instructor and must not be distributed outside the class without his expressed permission. For the University's stance on this, check out item 6 in its Administrative Policy on Student Responsibilities in Teaching and Learning.

Makeup Work for Legitimate Absences

Students will not be penalized for absence during the semester due to unavoidable or legitimate circumstances. Such circumstances include verified illness, participation in intercollegiate athletic events, subpoenas, jury duty, military service, bereavement, and religious observances. For information on what constitutes a legitimate absence and the attendant policies, please check out the Administrative Policy on Makeup Work for Legitimate Absences .

Equity, Diversity, Equal Opportunity, and Affirmative Action

The University is committed to providing equal access and opportunity to all in its programs and facilities, without regard to race, color, creed, religion, national origin, gender, age, marital status, disability, public assistance status, veteran status, sexual orientation, gender identity, or gender expression. For more information, please consult Board of Regents Policy on Equity, Diversity, Equal Opportunity, and Affirmative Action.

Disability Accommodations

The University of Minnesota views disability as an important aspect of diversity, and is committed to providing equitable access to learning opportunities for all students. The Disability Resource Center (DRC) is the campus office that collaborates with students who have disabilities to provide and/or arrange reasonable accommodations. Additional information is available on the DRC website. Students may also email drc@umn.edu with questions.

Mental Health and Stress Management

As a student you may experience a range of issues that can cause barriers to learning, such as strained relationships, increased anxiety, alcohol/drug problems, feeling down, difficulty concentrating and/or lack of motivation. These mental health concerns or stressful events may lead to diminished academic performance or reduce your ability to participate in daily activities. University of Minnesota services are available to assist you with addressing these and other concerns you may be experiencing. You can learn more about the broad range of confidential mental health services available on campus from the Student Mental Health website.

Sexual Harrassment

Sexual harassment means unwelcome sexual advances, requests for sexual favors, and/or other verbal or physical conduct of a sexual nature. Such conduct has the effect of unreasonably interfering with an individual's work or academic performance or creating an intimidating, hostile, or offensive working or academic environment in any University activity or program. Such behavior is not acceptable in the University setting. For additional information, please consult the Board of Regents Policy on this matter.

Academic Freedom

Academic freedom is a principle that is fundamental to intellectual inquiry. This notion includes the freedom to discuss relevant matters in the classroom, within the scope of the course as defined by the instructor. Students are encouraged to develop the capacity for critical judgment and to engage in a sustained and independent search for truth. Students are free to take reasoned exception to the views offered in any course of study and to reserve judgment about matters of opinion, even while they are responsible for learning the content of any course of study for which they are enrolled. Our University is committed to these ideas and principle. A good place to start towards understanding its position insofar as it impacts you as a student is the page of the Provost's office concerning this matter.

I have a special interest in this topic and I would be happy to discuss it with you if you do too.

Last modified: May 2, 2022. Page maintained by ngopalan atsign umn dot edu.

The views and opinions expressed in this page are strictly those of the page author(s). The contents of this page have not been reviewed or approved by the University of Minnesota.