Introduction to Computational Logic - Programming Systems

Jul 18, 2012 - Constructive type theory provides a programming language for ... We require that for every application of an operation exactly one of.
1MB Sizes 2 Downloads 243 Views
Introduction to Computational Logic Lecture Notes SS 2012 July 18, 2012

Gert Smolka and Chad E. Brown Department of Computer Science Saarland University

Copyright © 2012 by Gert Smolka and Chad E. Brown, All Rights Reserved

Contents 1 Introduction

1

2 Types and Functions 2.1 Booleans . . . . . . . . . . . . . . . . . . . . . . 2.2 Proof by Case Analysis and Simplification . 2.3 Natural Numbers and Structural Recursion . 2.4 Proof by Structural Induction and Rewriting 2.5 Pairs and Implicit Arguments . . . . . . . . . 2.6 Iteration . . . . . . . . . . . . . . . . . . . . . . 2.7 Factorials with Iteration . . . . . . . . . . . . 2.8 Lists . . . . . . . . . . . . . . . . . . . . . . . . . 2.9 Linear List Reversal . . . . . . . . . . . . . . . 2.10 Options and Finite Types . . . . . . . . . . . . 2.11 Fun and Fix . . . . . . . . . . . . . . . . . . . . 2.12 Standard Library . . . . . . . . . . . . . . . . . 2.13 Discussion and Remarks . . . . . . . . . . . . 2.14 Tactics Summary . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

3 3 5 6 9 11 13 15 16 17 19 20 21 22 23

3 Propositions and Proofs 3.1 Logical Operations . . . . . . . . . . . . . . . 3.2 Implication and Universal Quantification . 3.3 Predicates . . . . . . . . . . . . . . . . . . . . 3.4 The Apply Tactic . . . . . . . . . . . . . . . . 3.5 Leibniz Characterization of Equality . . . . 3.6 Propositions are Types . . . . . . . . . . . . 3.7 Falsity and Negation . . . . . . . . . . . . . . 3.8 Conjunction, Disjunction, and Equivalence 3.9 Automation Tactics . . . . . . . . . . . . . . 3.10 Existential Quantification . . . . . . . . . . . 3.11 Basic Proof Rules . . . . . . . . . . . . . . . . 3.12 Proof Rules as Lemmas . . . . . . . . . . . . 3.13 Inductive Propositions . . . . . . . . . . . . 3.14 An Observation . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

25 25 26 27 28 29 29 30 31 33 34 36 38 39 42

. . . . . . . . . . . . . .

iii

Contents

3.15 Excluded Middle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.16 Discussion and Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . 3.17 Tactics Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Untyped Lambda Calculus 4.1 Outline . . . . . . . . . . . . . . . . . . . . . 4.2 What Exactly Is A Term? . . . . . . . . . . 4.3 Formalization of Terms and Substitution 4.4 Formalization of Beta Reduction . . . . . 4.5 Church-Girard Programming . . . . . . . . 5 Basic 5.1 5.2 5.3 5.4 5.5 5.6

Dependent Type Theory Terms . . . . . . . . . . . . . . . Reduction . . . . . . . . . . . . Typing . . . . . . . . . . . . . . Basic Dependent Type Theory Adding Propositions . . . . . . Remarks . . . . . . . . . . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .