
15317 Constructive Logic

Date  Lecture or Recitation  Reading  Homework Due  



Tue  Aug  27  Overview:
We provide an overview over the course, covering topics, approach, and learning goals. We also outline administrative issues, such as assignments, exams, course policies, and grading. The course is divided into 4 parts.
The constructive nature of our approach to logic is manifest in the central role of proofs, which will be interpreted differently in the different parts of the course. Key concepts: What is Logic? 
01overview.pdf, Classical and Constructive Logic (pp. 14), by Jeremy Avigad 

Wed  Aug  28  No Recitation this week  
Thu  Aug  29  Natural Deduction:
We define the meaning of the usual connectives of propositional logic (conjunction, implication, disjunction) by introduction rules that allow us to infer when they should be true. From these, we derive elimination rules for the use of propositions. The resulting system of natural deduction is the foundation of intuitionistic logic which has direct connections to functional programming and logic programming. Key concepts:

02natded.pdf  


Tue  Sep  3  Harmony:
We elaborate on the verificationist point of view that logical connectives are defined by their introduction rules. We show that the elimination rules of intuitionistic logic are in harmony with the introduction rules in the sense that they are neither too strong nor too weak. We demonstrate this via local reductions and expansions, respectively. Then, we make more precise what a verification is and state, without proof, the global counterparts of the local soundness and completeness properties used to justify the elimination rules. 
03harmony.pdf  
Wed  Sep  4  Tutch  
Thu  Sep  5  Proofs as Programs:
We explore the correspondence between proofs and programs, which mirrors a related correspondence between propositions and types. Then, local reductions correspond to steps of computation. 
04pap.pdf  


Tue  Sep  10 
Quantification:
We introduce universal and existential quantification, making the transition from propositional to firstorder intuitionistic logic. We reason with the quantifiers abstractly, isolating what should be true without regard to any particular domain of quantification. Parametric judgments and the associated substitution principle emerge as a new piece of infrastructure. We then explore the computational meaning of quantifiers and the corresponding programming concepts. Key concepts:

05quant.pdf, Computational Meaning of Quantifiers  
Wed  Sep  11  Quantifier examples  
Thu  Sep  12  Natural Numbers:
We introduce the data type of natural numbers as a prototype for other kinds of data structures. The introduction form let us construct natural numbers from zero and a successor function, the elimination forms model both proof by induction and function definition by primitive recursion. The resulting system is called intuitionistic arithmetic or Heyting arithmetic. Key concepts:

06nat.pdf  Homework 1  


Tue  Sep  17  Classical Logic
We introduce the distinction between classical and constructive reasoning in the context of natural deduction systems. We discuss the equivalence of several principles of classical reasoning. We give several examples of classical proofs, pausing along the way to observe their structure. A common underlying theme is a certain timetravelling mindchanging behavior exhibited by classical proofs, which will become clearer when we look at the computational interpretation of classical logic. We look briefly at a judgmental formulation of classical logic based on proof by contradiction and two new judgments, A false and # (contradiction). Key concepts:

07classical.pdf (lecture notes), Introduction to the philophical issues  
Wed  Sep  18  Arithmetic and classical logic in Tutch  
Thu  Sep  19  Classical Computation:
We explore the correspondence between proofs in classical logic and programs. Adding proof by contradiction to our logic leads to sophisticated control operators in our programs. Key concepts:

08classicalprograms.pdf  Homework 2  


Tue  Sep  24 
Sequent Calculus:
We develop the cutfree sequent calculus as a formal system for proof search in natural deduction that captures the notion of a verification exactly. All rules are applied bottomup, from the conclusion to the premise, unlike the introduction and elimination rules that work bottomup and topdown, respectively. This sequent calculus allows proving important properties about logic. Key concepts:

09seqcalc.pdf  
Wed  Sep  25  Homework 2, Classical Computation  
Thu  Sep  26  Induction over proofs:
We extend the familiar idea of structural induction to induction over formal derivations. We explore a simple example in preparation for the more complex proof of the cut theorem. Key concepts:

03induction.pdf, ruleinduction.pdf  Homework 3  


Tue  Oct  1  Cut Elimination:
We prove one of the central theorems in logic, namely that cut is admissible in the cutfree sequent calculus. This completes the connection between truth (as defined by natural deduction) and sequent calculus with numerous important corollaries about truth, expressed in the previous lecture as properties of the sequent calculus. Key concepts:

10cutelim.pdf  
Wed  Oct  2  Review  
Thu  Oct  3  Midterm I  Sample Solution  Homework 4  


Tue  Oct  8  Inversion:
We turn to the problem of efficiently building derivations, which is key to implementing theorem provers. To this end, we present two sequent calculi that restrict when rules are applicable. The first eliminates the principal formula of an inference from the premises as much as possible. The second, based on the first, eagerly applies invertible rules to avoid unnecessary nondeterminism in search. Key concepts:

11inversion.pdf  
Wed  Oct  9  Cut Elimination, Inversion Review  
Thu  Oct  10  Propositional Theorem Proving:
We refine the calculi obtained in the last lecture to eliminate the remaining need to retain principal formulas with implications in the premise of a rule. The result is Dyckhoff's contractionfree sequent calculus, which can be implemented to obtain a decision procedure for intuitionistic propositional logic. Key concepts:

12proving.pdf
For more information: ContractionFree Sequent Calculi for Intuitionistic Logic (Dyckhoff) 
Homework 5  


Tue  Oct  15  Logic Programming:
In this lecture we introduce an entirely different connection between logic and computation. We interpret logical rules as programs that are executed by proof search according to a fixed strategy. Unification supplies answer substitutions, so that computations may produce more information than just provability/unprovability. We see that the programmer must be aware of the search strategy in order to effectively create efficient terminating logic programs. Key concepts:

13lp.pdf, code  
Wed  Oct  16  Recitation  
Thu  Oct  17  Prolog:
We examine the basics of Prolog, the granddaddy of logic programming languages. We do some simple list programming and operations with numbers, observing some subtleties of equality in Prolog. Then we examine some basic nonlogical features for controlling search. Key concepts:

14prolog.pdf, code  


Tue  Oct  22  Prolog programming:
We do a variety of "finger exercises" to develop an intuition for simple recursive Prolog programs over lists and other structures. We introduce the nonlogical control constructs of conditional and cut. Key concepts:

code  
Wed  Oct  23  Prolog  
Thu  Oct  24 
Prolog idioms
We concentrate on progamming methods that are specific to logic programming or especially easy in logic programming: difference lists, program clauses as databases, and backtracking search. Key concepts:

11diff.pdf, sections 11.111.3, 11.511.7
code 
Homework 6  


Tue  Oct  29  Uniform Provability:
We isolate the prooftheoretic foundations of logic programming in the notion of uniform provability, which is closely related to inversion. Abstract logic programming languages (ALPL) are complete w.r.t. uniform provability. We see how to restrict clause and goal formulas to model Prolog so that it can be shown to be an ALPL, and discuss other restrictions (higher order Horn clauses, hereditary Harrop formulas, etc.) and briefly sketch some of the programming language features that could be provided in such ALPLs. Key concepts:

apal91.pdf,
sections 1, 2 from end of p. 4, 3 to top of p. 11, 4; A tutorial presentation of the basic technical ideas; Some helpful slides. 

Wed  Oct  30  Prolog lists, cut  
Thu  Oct  31  Metaprogramming in Prolog:
We examine how to specify the operational semantics of Prolog as an inference system, which we translate directly into a metacircular interpreter. We start by making explicit the order in which subgoals are solved. We examine the soundness and completeness of this simple interpreter and extend it to perform loop detection, depthlimited searching, and tracing. Key concepts: 
Metacircular
interpreter 1 (Operational Semantics); code 
Homework 7  


Tue  Nov  5  Metaprogramming in Prolog 2
We continue specifying the operational semantics of Prolog as an inference system, which we translate directly into a metacircular interpreter. Today we exert control over backtracking. This requires converting object programs into a normal form so that clause selection is deterministic and choice points are explicitly represented in clause bodies. The resulting system is sound but can't be complete due to its depthfirst character. We implement the system and extend the interpreter to count the number of proofs instead of simply reporting success or failure. Then we briefly look at an inference system for breadthfirst search. You're invited to try to prove it complete or find bugs in it; success will result in significant bonus points. Key concepts: 
Metacircular
interpreter 2 (Backtracking); code 

Wed  Nov  6  Review  
Thu  Nov  7  Unification:
We define a third abstract machine for abstract logic programming languages that handles the instantiation of variables lazily by relying on unification at the point of use and propagating it explicitely by means of substitution. Key concepts:

Unification; Lifting 
Homework 8  


Tue  Nov  12  Midterm II  Sample Solution  
Wed  Nov  13  Exam postmortem  
Thu  Nov  14  Linear logic  lp:12linear.pdf  


Tue  Nov  19  Linear Logic Programming  Logic Programming in a Fragment of Intuitionistic Linear Logic (Hodas and Miller); Read the parts outlined in red.  
Wed  Nov  20  Linear logic examples  
Thu  Nov  21  Bottomup Logic Programming  20bottomup.pdf  


Tue  Nov  26  Lollibot and bottomup linear logic programming  Examples from lecture, Other examples 

Wed  Nov  27  Thanksgiving Holiday  
Thu  Nov  28  Thanksgiving Holiday  


Tue  Dec  3  Elizabeth will give a talk  
Wed  Dec  4  Review  
Thu  Dec  5  Michael will give a talk  Homework 9  




Final (Date, Time, and Room TBA) 
[ Home  Schedule  Assignments  Handouts  Software ]
annpenny at Andrew