On this page:
Logic and Computation Intertwined
7.8

Logic and Computation Intertwined


(a flânerie by Prabhakar Ragde)

This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License. Please do not post exercise solutions to any public forum or publicly-accessible software repository.

    1 Introduction

      1.1 Required background

      1.2 Prospective audience

      1.3 Design philosophy

      1.4 The motivations for proof

      1.5 Informal proof in mathematics

      1.6 Informal proof in computer science

      1.7 What next?

    2 Propositional Logic

      2.1 Formulas

      2.2 The Boolean interpretation

      2.3 Proof for the implicational fragment

      2.4 Proofs as programs

      2.5 Proust for implication

      2.6 Assistance with proofs

      2.7 Adding the other connectives

      2.8 Classical vs intuitionistic logic

      2.9 Semantics for intuitionistic propositional logic

      2.10 Summary of rules for intuitionistic propositional logic

    3 Predicate Logic

      3.1 First-order logic

      3.2 Higher-order logic

        3.2.1 Universal quantification

        3.2.2 Wrong, wrong, wrong

        3.2.3 Simulating other features

        3.2.4 Neither proof nor assistant

        3.2.5 Equality, Booleans, and arithmetic

        3.2.6 Existential quantification

      3.3 Summary of rules for intuitionistic predicate logic

    4 Proof Assistants

      4.1 Common features

      4.2 Agda

        4.2.1 Up from nothing

        4.2.2 Propositional and predicate logic

        4.2.3 Ordering

        4.2.4 Equality

        4.2.5 Natural numbers

        4.2.6 Sorting

        4.2.7 Data Structures

      4.3 Coq

        4.3.1 Booleans

        4.3.2 Logic

        4.3.3 Numbers

        4.3.4 Inductively defined propositions

        4.3.5 Case study: sorting

    5 Handouts

    6 Resources

      6.1 Acknowledgements