# University of AlbertaDepartment of Computing ScienceCMPUT 272 Introduction toLogic in Computing Science

## H. James Hoover and Piotr Rudnicki

© 1994 H. James Hoover and Piotr Rudnicki

## Section 4: Interpretations

### 4.3: Problems in translation

4.3.1: A question

## Section 5: 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

## Section 6: Hypothetical Reasoning

### 6.1: Implication Introduction, II

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

## 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.4: Universal Introduction

### 8.2: Proof Structures

8.2.1: Conjunction
8.2.2: Implication
8.2.3: Disjunction
8.2.4: Equivalence

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

## Appendix 2: Mizar MSE Grammar

### 2.3: Problems with syntax

2.3.1: A question