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

### 0.1: Course Overview

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

### 4.1: Satisfiability and Falsifiability

### 4.2: Translations

### 4.3: Problems in translation

- 4.3.1: A question
- 4.3.2: Its answer

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

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

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

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

### 9.1: Premises

### 1.1: A murder mystery

### 1.2: K. Schubert's Steamroller

### 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*