## 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.
Introduction to Computational Logic Lecture Notes SS 2012 July 18, 2012

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

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

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .