15-317 Constructive Logic
Schedule

  • The class notes provide additional reading material. They complement, but do not replace the lecture.
  • The schedule is subject to change throughout the semester.

  • 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.

    1. Proofs as Evidence for Truth
    2. Proofs as Programs
    3. Proofs as Computations
    4. Modal and substructural logics

    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?
    01-overview.pdf,

    Classical and Constructive Logic (pp. 1-4), by Jeremy Avigad
     
    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:
    • Proposition
    • Truth
    • Introduction and elimination rules
    • Hypothetical judgment
    • Substitution principle
    02-natded.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.

    03-harmony.pdf  
    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.

    04-pap.pdf  

    Tue Sep 10 Quantification:

    We introduce universal and existential quantification, making the transition from propositional to first-order 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:
    • Universal and existential quantification
    • Parametric judgments
    • Substitution principle for parametric judgments
    • Universal quantification and dependent function types
    • Existential quantification and dependently typed pairs
    05-quant.pdf, Computational Meaning of Quantifiers  
    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:
    • Induction
    • Primitive recursion
    06-nat.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 time-travelling mind-changing 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:
    • Proof by contradiction
    • Law of excluded middle, double negation elimination
    • Showing rule equivalence
    • A false and # judgments
    07-classical.pdf (lecture notes), Introduction to the philophical issues  
    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:
    • Proof terms
    • Continuations
    • Double-negation translations
    • Continuation-passing style (CPS)
    08-classical-programs.pdf Homework 2

    Tue Sep 24 Sequent Calculus:

    We develop the cut-free sequent calculus as a formal system for proof search in natural deduction that captures the notion of a verification exactly. All rules are applied bottom-up, from the conclusion to the premise, unlike the introduction and elimination rules that work bottom-up and top-down, respectively. This sequent calculus allows proving important properties about logic.

    Key concepts:
    • Sequents
    • Identity theorem
    • Subformula property
    • Consistency of propositional logic
    09-seqcalc.pdf      
    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:
    • Induction hypothesis
    • Coverage of all cases
    • Inversion
    03-induction.pdf, rule-induction.pdf Homework 3

    Tue Oct 1 Cut Elimination:

    We prove one of the central theorems in logic, namely that cut is admissible in the cut-free 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:
    • Cut
    • Cut elimination
    • Soundness and completeness
    • Sequent calculus for quantifiers
    10-cutelim.pdf
    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:
    • Goal-directed proof search
    • Nondeterminism
    • Nontermination
    • Invertible rules
    • Encoding control structure in inference systems
    11-inversion.pdf  
    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 contraction-free sequent calculus, which can be implemented to obtain a decision procedure for intuitionistic propositional logic.

    Key concepts:
    • The contraction-free sequent calculus
    • Right and left asynchronous formulas
    12-proving.pdf
    For more information: Contraction-Free 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:
    • Proof search as computation
    • Unification and answer substitutions
    • Backtracking and choice points
    • Subgoal ordering
    • Negation as failure
    • "Declarative" programs
    13-lp.pdf, code  
    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 non-logical features for controlling search.

    Key concepts:
    • Equality as unifiability
    • Numbers and constraint logic programming
    • Prolog lists
    • Representing recursive functions in Prolog
    • Modes
    • Prolog cut
    14-prolog.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 non-logical control constructs of conditional and cut.

    Key concepts:
    • Converting recursive function definitions to predicate definitions
    • Prolog lists
    • Prolog arithmetic
    • Conditional
    • Cut
    • Red versus green cuts
    code  
    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:
    • Unification
    • Difference lists
    • Clauses as databases
    • Backtracking state space search
    11-diff.pdf, sections 11.1-11.3, 11.5-11.7
    code
    Homework 6

    Tue Oct 29 Uniform Provability:

    We isolate the proof-theoretic 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:
    • Logical connectives as search directives
    • Clauses and goals as restricted sets of formulas
    • Uniform proofs
    • Abstract logic programming languages
    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.
     
    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, depth-limited searching, and tracing.

    Key concepts:
  • Metacircular interpreters
  • Subgoal ordering
  • Deductive systems for operational semantics
  • 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 depth-first 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 breadth-first search. You're invited to try to prove it complete or find bugs in it; success will result in significant bonus points.

    Key concepts:
  • Backtracking
  • Depth-first search versus breadth-first search.
  • Normal forms for programs
  • Metacircular interpreter 2 (Backtracking);
    code
     
    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:
    • Substitutions
    • Most general unifiers
    • Lifting
    Unification;
    Lifting
    Homework 8

    Tue Nov 12 Midterm II Sample Solution  
    Thu Nov 14 Linear logic lp:12-linear.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.  
    Thu Nov 21 Bottom-up Logic Programming 20-bottom-up.pdf  

    Tue Nov 26 Lollibot and bottom-up linear logic programming Examples from lecture,
    Other examples
     
    Thu Nov 28 Thanksgiving Holiday    

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


    Final (Date, Time, and Room TBA)    

    [ Home | Schedule | Assignments | Handouts | Software ]

    annpenny at Andrew