University of Alberta
Department of Computing Science
CMPUT 272

Introduction to
Logic in Computing Science

H. James Hoover and Piotr Rudnicki

© 1994 H. James Hoover and Piotr Rudnicki

Table of Contents

0.1: Course Overview

Section 2: The Island of Knights and Knaves

Section 3: The Syntax and Fixed Semantics of MIZAR MSE

3.1: Identifiers, Sorts, Constants, Variables, and Terms
3.2: Predicates and Atomic Formulas
3.3: Logical Connectives and Compound Formulas
3.4: Conditionals and Biconditionals
3.5: Quantifiers
3.6: Scope and Binding
3.7: The Semantics of Quantified Formulas
3.8: BNF Grammar for Quantified Formulas

Section 4: Interpretations

4.1: Satisfiability and Falsifiability
4.2: Translations
4.3: Problems in translation 4.3.1: A question 4.3.2: Its answer

Section 5: Arguments

5.1: The Structure of MIZAR Arguments
5.2: Basic Inference Rules 5.2.1: Rewriting or Repetition, RE 5.2.2: Negation Elimination, NE 5.2.3: Negation Introduction, NI 5.2.4: Conjunction Elimination, CE 5.2.5: Conjunction Introduction, CI 5.2.6: Disjunction Elimination, DE 5.2.7: Disjunction Introduction, DI 5.2.8: Implication Elimination, IE, or Modus Ponens, MP 5.2.9: Implication Introduction, II 5.2.10: Equivalence Elimination, EqE 5.2.11: Equivalence Introduction, EqI 5.2.12: Equality Elimination, =E 5.2.13: Equality Introduction, =I 5.2.14: Rules for Quantifiers
5.3: Annotated Proofs

Section 6: Hypothetical Reasoning

6.1: Implication Introduction, II
6.2: Proof by Contradiction 6.2.1: Contradiction Introduction, ContrI 6.2.2: Negation Introduction, NI
6.3: Derived Rules Of Inference 6.3.1: Modus Ponens Twice 6.3.2: Double Negation Introduction 6.3.3: Reverse Implication Elimination or Modus Tollens (MT) 6.3.4: Excluded Middle 6.3.5: Chained Implication 6.3.6: Reverse Implication 6.3.7: Case Analysis 6.3.8: Equivalence Elimination 6.3.9: Equivalence Introduction 6.3.10: Divergence 6.3.11: De Morgan's Laws 6.3.12: More Disjunction Elimination 6.3.13: Another Implication Elimination 6.3.14: More Implication Introduction 6.3.15: Referencing Distributed Statements
6.4: The Notion Of Visibility in a Reasoning
6.5: Examples

Section 7: Inference Rules for Quantified Formulas and Equality

7.1: Bound Variable Renaming
7.2: Proper Free Substitution
7.3: Equality Elimination, =E
7.4: Universal Elimination, UE
7.5: Existential Introduction, ExI
7.6: Examples of Universal Elimination, and Existential Introduction
7.7: Universal Introduction, UI
7.8: Existential Elimination, ExE
7.9: De Morgan's Laws for Quantifiers

Section 8: Proofs

8.1: II, NI, PbyC, UI Rules Revisited 8.1.1: Proof of an Implication 8.1.2: Proof of a Negation 8.1.3: Proof by Contradiction 8.1.4: Universal Introduction
8.2: Proof Structures 8.2.1: Conjunction 8.2.2: Implication 8.2.3: Disjunction 8.2.4: Equivalence
8.3: Omitting Proofs
8.4: Incorporating proofs
8.5: thesis
8.6: MIZAR Problems on Knights and Knaves 8.6.1: Puzzle 1 8.6.2: Puzzle 2 8.6.3: A theorem about Knights and Knaves 8.6.4: Three more theorems 8.6.5: And even more theorems

Section 9: Interpretations Revisited

9.1: Premises

Appendix 1: Sample Mizar Proofs

1.1: A murder mystery
1.2: K. Schubert's Steamroller

Appendix 2: Mizar MSE Grammar

2.1: Notation
2.2: Grammar
2.3: Problems with syntax 2.3.1: A question 2.3.2: Its answer

March 20, 1998 -- Farren Layton -- farren@ugrad.cs.ualberta.ca