0% found this document useful (0 votes)

253 views507 pages

2013 Book ModellingComputingSystems PDF

Uploaded by

Scripcari Olga

We take content rights seriously. If you suspect this is your content, claim it here.

Available Formats

Download as PDF, TXT or read online on Scribd

0% found this document useful (0 votes)

253 views507 pages

2013 Book ModellingComputingSystems PDF

Uploaded by

Scripcari Olga

We take content rights seriously. If you suspect this is your content, claim it here.

Available Formats

Download as PDF, TXT or read online on Scribd

You are on page 1/ 507

Undergraduate Topics in Computer Science

Faron Moller
Georg Struth

Modelling
Computing Systems
Mathematics for Computer Science
Undergraduate Topics in Computer Science
Undergraduate Topics in Computer Science (UTiCS) delivers high-quality instructional content for un-
dergraduates studying in all areas of computing and information science. From core foundational and
theoretical material to ﬁnal-year topics and applications, UTiCS books take a fresh, concise, and mod-
ern approach and are ideal for self-study or for a one- or two-semester course. The texts are all authored
by established experts in their ﬁelds, reviewed by an international advisory board, and contain numer-
ous examples and problems. Many include fully worked solutions.

For further volumes:

www.springer.com/series/7592
Faron Moller r Georg Struth

Modelling
Computing Systems

Mathematics for Computer Science

Faron Moller Georg Struth
Department of Computer Science Dept. Computer Science
Swansea University University of Sheffield
Swansea, UK Sheffield, UK
Series editor
Ian Mackie
Advisory board
Samson Abramsky, University of Oxford, Oxford, UK
Karin Breitman, Pontifical Catholic University of Rio de Janeiro, Rio de Janeiro, Brazil
Chris Hankin, Imperial College London, London, UK
Dexter Kozen, Cornell University, Ithaca, USA
Andrew Pitts, University of Cambridge, Cambridge, UK
Hanne Riis Nielson, Technical University of Denmark, Kongens Lyngby, Denmark
Steven Skiena, Stony Brook University, Stony Brook, USA
Iain Stewart, University of Durham, Durham, UK

ISSN 1863-7310 Undergraduate Topics in Computer Science

ISBN 978-1-84800-321-7 ISBN 978-1-84800-322-4 (eBook)
DOI 10.1007/978-1-84800-322-4
Springer London Heidelberg New York Dordrecht

Library of Congress Control Number: 2013943907

© Springer-Verlag London 2013

This work is subject to copyright. All rights are reserved by the Publisher, whether the whole or part of
the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation,
broadcasting, reproduction on microfilms or in any other physical way, and transmission or information
storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology
now known or hereafter developed. Exempted from this legal reservation are brief excerpts in connection
with reviews or scholarly analysis or material supplied specifically for the purpose of being entered and
executed on a computer system, for exclusive use by the purchaser of the work. Duplication of this pub-
lication or parts thereof is permitted only under the provisions of the Copyright Law of the Publisher’s
location, in its current version, and permission for use must always be obtained from Springer. Permis-
sions for use may be obtained through RightsLink at the Copyright Clearance Center. Violations are liable
to prosecution under the respective Copyright Law.
The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication
does not imply, even in the absence of a specific statement, that such names are exempt from the relevant
protective laws and regulations and therefore free for general use.
While the advice and information in this book are believed to be true and accurate at the date of publica-
tion, neither the authors nor the editors nor the publisher can accept any legal responsibility for any errors
or omissions that may be made. The publisher makes no warranty, express or implied, with respect to the
material contained herein.

Printed on acid-free paper

Springer is part of Springer Science+Business Media (www.springer.com)

CONTENTS v

Contents

Preface xiii

0 Introduction 1

!
"

# $

%

&
'
(
(
)
) *

+

' )

, "
, $ * -

., &

/
.

Part I: Mathematics for Computer Science 15

1 Propositional Logic 17
' 0
1

#22
' #2
' /$

*
2
03
3
&
( 4%

)
)
' #2 )
1 '

'

1
-

"
2 5 ' #2
$2
* #22

$

( 4%

/ 2

) 2
$ #5 #2 4%

)
1

2 Sets 57

* )
"
$
, 4 & -

'

(
!
6 ' (
vi CONTENTS

!
!

!!
!
!"
#!
$
%
&$'
( ) !

($
*+"
, , " !

&!!

*-

3 Boolean Algebras and Circuits 87

. &$'

,
$ !

. &$' /
0% "
1

($
!
$

"

#2
$ " &!! //
.
1 3"' //
&!!
$ .
1 3"' /
."
!
$ 4) &!! /
."
!
$ 5" &!! /
"
$ & 0$ % /
&!!

*-
/

4 Predicate Logic 109

!
! 5 6
' /
7"
8 ! ."! 6
'

, 7"
8

*-

7"
8

."!! 7"
8

9" ) 7"
8
/
#!
$
!
($

&!!

*-

5 Proof Strategies 131

& 5
*-
) $
)

) $
) 3$

) $
) :"
! *+"
,
) $
)
:"

) $
) 7"
8

, 7"
8

CONTENTS vii

6 Functions 155

!
" #
$%&' "
$%&' (
)*
+ )

!(
,
!- !(

%

7 Relations 179

. /
0
" . /
0
&
. /
0

&
0
12
' /
0
$%&' /
00
!(
% /'
+ /
0
3&

+ . /
#
/
4
2
1
4
2
/
#
).%%
.%%
/

! 2
/

' /

2

/

2

$
3

8 Inductive and Recursive Deﬁnitions 201

0 1 2
.

)
#
0 1 2
.

). )
#
0 - 5 "% #
0 1 2
.

!.&
#
0 1 2
.

"
0 /
2
"
0 /
2
3

0
00

#

9 Proofs by Induction 223

$2' 6 1 2
2

3%. )( 1 '%

!(
1 '%
0
viii CONTENTS

!
" # $ !
# %&& '
( )
! *
+ * "
, -'(&
%(
#& -'

10 Games and Strategies 251

")" +.. .%
") )
")
") %(
") /'
") 0 .

")! #& -' !"

Part II: Modelling Computing Systems 277

11 Modelling Processes 279

""" 1&& $ 2 ,"
"" %( ,!
"" # 1
""" $ & 0
"" # '
""
"" %
"" 0 0
"" -3&2 0 )
"" #& -' )

12 Distinguishing Between Processes 309

"" $ 0& + )
" ( + -3& "
" 0& 4& "
" 0& %& "
" $ 0& + 45 $
2 026
"" 7&
" 7& 0& +
" #& -' ,
CONTENTS ix

13 Logical Properties of Processes 333

!
"
#$

%
&
'
(
)' * %+
, -! .'
%
/ 01

%

14 Concurrent Processes 357

.
%,
(
+
#2 $ (

01
%

%

3
' /
%

$ .
' ,
& ,
, 01

,,

15 Temporal Properties 381

% . ' 4
/
% 2
5 /
%

! 5 /
% 65 6 /
% #
$
/%
% .$ #
$ 07
/,
% )1 .
//
% 8(
9+
%
$

-
)1
9
% 1' )1
9
%% 01

. ' 4

9,
%% 2
5 9/
%%

! 5 9/
%% 65 6 9/
% ) )1
99
%, 01

+

Solutions to Exercises 405

Index 493
List of Figures

! " # $

%& '

(
#

)) $

$
* +$
$

,- ¿ +.
$ /
0 1
$ /

1

1 2 '# 3

& 4 & 50 # 6

,♂- # ,♀-

. 7
$
. 8 #
0 #& .
. 9#
: 6

6 +1

6
$$
6 # $1
6 0 # #& $
6+
# $.
6$
0 # 8& 16
61 &
1

6
! #
%( ;:<:=:7 >## $

=78 $ # 1
+ .
$ (! #

.1
1 7 .
xii LIST OF FIGURES

! HML

" HML #

$ %

$ & '

$ (
$

# " )())

# * # $
# * $
#$ +! , - . $
## +! ( / $
# +! $
# (
$
Preface

! "

# $

%& %& '

(

$ $ $

) *

+ (

* $ $ -

%

$

$ #

'

/

$ # '

)

/ 0 %
xiv Preface

! "
#$$%

&

'

( "

)

* "
+
"

&

,

-

-

,

!

&

(

,

!

. /

,

( !

&

,

)

!

0

, )
1 /

' .

&

,

!

Æ

2

)

1 // ) - -
Preface xv

!

" #
" ##

$

% &

'
" #

" ##

(

)
%
#
$

&

$ *

(
$ "

(

$

(

$ ++

$ )

!

$

% ,

#

$&

-

(

#

#
.

xvi Preface

Speciﬁcation

Implementation Synthesis

Veriﬁcation

" #

" # !
$
%

&&

&&

!
'

(

! ) ( " (
*

+
, -
. /

0 ( % "
" " Æ
Chapter 0

Introduction

"
#

$

% %

&

' (

)

+

' (

-

. /

(

Æ

0

+
1

%

(

F. Moller, G. Struth, Modelling Computing Systems,

Undergraduate Topics in Computer Science,
DOI 10.1007/978-1-84800-322-4_1, © Springer-Verlag London 2013
2 Introduction

!

"

Æ
#

$

&

%

0.1 Examples of System Failures

' (

0.1.1 Clayton Tunnel Accident

)

*
Examples of System Failures 3

Æ

!

" #
"
$
% &
"

' $ (
)*
+ ,-.,

)/ 0 ,1.

'

#

2 3 $

' #

-!4* -!,* -!/4 5

"

6 ' 7 6
"

8 -!)- -!/, -!/* # "

6 ( 9
6 6
$
6 (

3

: 0

5

:

4 Introduction

! "
!

#

"

"

$

%

!

&
'

"

" "

"
"

"

"

(

'

"

)

*
+,
- ' .

/ 0 12234
0.1.2 USS Scorpion
5 6378
"
99 9

33 "

"

"

" "

"

:

"

&
+,
0 ; <

= $
633>4

"

*

&

'

"

*

:

:

0.1.3 Therac 25 Radiotherapy Machine

1?

+638?*8@4 *
Examples of System Failures 5

! "
#$
%

& $
'
26()

*+,* - *../)

0

&

1

2& )

3

4 5

&

2& )

)

2&

&

6
7)

0

0

)

0

8

8)

9
&

:

%

:

)

&

&

%

&

;

:

1 #< &

$

&

'

&

1 #0

:

&

'

1

"
5

0.1.4 London Ambulance Service

% ;
*..
$
"

!$=)
0 $"!$=

%

>

6 Introduction

!

"

#$

# %%

& "

#

'

( #

)

#

%

'

(

*!
! # + ,
- .

/
0
'

( . ( 1

2/// .( 3
45 %6678

$
! # ,

-

#
"

9 1
0.1.5 Intel Pentium
: 2 3 3. %665

;

:

"
#

;

"

# $

"
%77

<

#

!

* 8

=

>

<
Examples of System Failures 7

Ü Ý

! " # $
%

! &" " '

'!( )*! +! , - *
0.1.6 Ariane 5
. / ! 0 % 1

- -2!

)! 3 -2 4 - 5
)
- %
%+ 4 .
%+- 6 -2
- " - 76 %-
-2

" 0 % -2 -

76 % - !
0 ! -

- -

88
- -29 7 " 7

% 7 % 0 ! -
+ %
1
7

6 " -
%
*
" % 5- - - +7
+7 7 7 7 +7
1 4 0 % 1 -

% -
- 7% 6 --
!
-

1 0: 7

1 * 1 -

5- ! - !
76 6 76 - 6 0 . +
-

6! % % %

6 76 1
7%
%+ 4!
6 - % 0
7
6 %

%+ 4 " - % %
- 6 % 1
" 1 ) .;6 ' %
& -+
- % %
%- 6(
7- 1 <
& -
;

6 %
%- 6 % -
0
-
6( . - = > - 1-6

% - &-- ! - % - +

6 ;
6(
&1 ) .;6 ' !(
http://esamultimedia.esa.int/docs/esa-x-1819eng.pdf*

0.1.7 Needham-Schroeder Protocol

? - - .! 6 - -
6 ! -
6 -6 6
% 6 6 ! - 6 - -
!

6 - % 6 - -6 "
8 Introduction

!"#

$
%
&

'

"

(

"

&

)
&

&
*
& +

&

'/01 '2
3

4

& '//2

.
' -

&

(
& "
&

)
&

&

5
& &
&

System, Model, Abstraction and Notation 9

!" # $
% & '

(

)!*+ ,*, ,*) & ,-- +

.

/

/

Æ
0

/

Æ
1
2
.

/

3

.

' 1
4

5

6

0.2 System, Model, Abstraction and Notation

% ( %( % ( %(

.
6
/

10 Introduction

System

!

"

!
#
$

%

%

%

$

"

!

&
'

(

!

)

*

!

Model
+,-

. +/- $

0

$

!

System, Model, Abstraction and Notation 11

Æ

!

"

¯

#$%

¯

& '

#(%

)

*

'

Abstraction

+

,
-

12 Introduction

!

"

#

$

%&' (((

)
*
+ !,

- . $

%

!&
!&&

/

0

/ 1

2

3 4

5

/ 6
3 !78, #
#

1

/ 2

9

!78! : 4

;
%4 /

4

<

= 4

/

.

Notation

4

0 >4
*
6

>

-

9

"
?@
.
4

!7'(4!7'7

6

Speciﬁcation, Implementation and Veriﬁcation 13

!

! "
#

$
%

&

0.3 Speciﬁcation, Implementation and Veriﬁcation

"

# '

!
"
(

) Speciﬁcation

"

* Implementation

'

"

#

'

+ Veriﬁcation

'
"

"

,

-

'

"

&

14 Introduction

!

Part I

Mathematics for
Computer Science
Chapter 1

Propositional Logic

! " #

# " $ " $

% " ! & ' "

" (

" )! $

% &

% "

%! & ! "#

" # ) %

" * ! + ! , -

% ( ( ! " & -

. ! *

% " "

" ! % &

% % ) ( "

" % & % /)
" ( % " " ! %
% 0

"

" " 1%

%% %% "

" $ " % " %

" "

( " $

! " . % "

" " "

% " "

F. Moller, G. Struth, Modelling Computing Systems,

Undergraduate Topics in Computer Science,
DOI 10.1007/978-1-84800-322-4_2, © Springer-Verlag London 2013
18 Propositional Logic

#

1.1 Propositions and Deductions

% Either this man is dead or my watch has stopped.

& My watch is still ticking.
Therefore
' This man is dead.
( )

" statements propositions

( )

*

# +

% This man is dead.

or
% My watch has stopped.

$ " deduction inference

#

conclusion #
Propositions and Deductions 19

premises

atomic propositions
This man
is dead

propositional connectives or

Example 1.1

! "
# $%

$&'

(

(

( ) * (

+

+

( +
(

+
( ,

-

( *

(
.

( +

/ #

(
*

( .

(
( + .
+
( +

+

(

0

)

1

(

)

+ (

+ (

(
20 Propositional Logic

Exercise 1.1 (Solution on page 405)

! " #
$ " %%& %

' (
)
* ) +
,
- ! ! . %

/ ! ! .0 ! 1.!
%
.0 / . 1
' %
% .
% 2
%! % !

% +
Exercise 1.2 (Solution on page 405)

1 % %%
' 3 %! 1 1 . %
-1 1 . %
4 3 %%
' 3 %! 1 1 . %
4 3 %%
4 1 1 . %
' ! %
4 %
4

$ 4
.
% 1%
5 1 % 1%
4
.
4
.
% 1%! 6 % 1%
7
% 1%
4
.
The Language of Propositional Logic 21

Exercise 1.3 (Solution on page 406)

! "

#

"

$ "

"

%#

&
"

' "

"

%#

&

( "

"

%#

&

) "

#

%#

&
"

1.2 The Language of Propositional Logic

syntax

*
object language

meta-
language +

+

,

*

-

*

.
*
sym-
bols

* ,
formulæ -

-

22 Propositional Logic

1.2.1 Propositional Variables

¾

! "

#
#

$ %

Propositional
variables

&

$ '

(
'!#)

# *

& '
(
Dead +
) ,-

.

,

.
,.
, .

, . ,.

propositional connectives &/

() , . () , . ( ) , . ( ) ,. (

) ,. 0

1.2.2 Negation
negation ( )

' 1

Example 1.3

Dead ( ) Dead (

)

(
The Language of Propositional Logic 23

Exercise 1.4 (Solution on page 406)

! "

# $! % ! &'

1.2.3 Disjunction
disjunction

$

'

(

(
)

*

disjuncts

Example 1.4

Dead
Watch

+
Dead Watch

,

Dead Watch

Example 1.5

-

-

- ,

24 Propositional Logic

KingMoved RookMoved KingMoved
RookMoved

Exercise 1.5 (Solution on page 406)

!
"

# $% &' $% ('
& $( )' $* ('
% $( +' $+ ,'

-
$
'

.
/
0 1

2
$ '
3 2

3
-

4
3
1
$ 51 ##6
&7'

Exercise 1.6 (Solution on page 406)

8

!
1
!

# 9 : 3

8 1 ;
& 2
% < 2
The Language of Propositional Logic 25

1.2.4 Conjunction
conjunction

conjuncts
Example 1.6

Dead

Watch

! Dead Watch

" #

$
%

Exercise 1.7 (Solution on page 407)

& '

( )* +, )* -,
+ )- ., )/ -,
* )- 0, )0 1,

1.2.5 Implication
2
implication

3

26 Propositional Logic

¯
¯
Æ

premise

conclusion

Example 1.7

SignalDanger

TrainStop

SignalDanger TrainStop

Exercise 1.8 (Solution on page 407)

JoelHappy
AmandaHappy

JoelHappy AmandaHappy AmandaHappy JoelHappy !

Exercise 1.9 (Solution on page 407)

%

'

(
The Language of Propositional Logic 27

1.2.6 Equivalence
equivalence Ô ¸ Õ
Ô Õ Ô
Õ
Ô Õ
Ô Õ Ô Õ

¯Ô Õ

¯Ô Õ

¯Ô Æ Õ

¸

µ !

Ô ¸ Õ Ô µ Õ Ô ´ Õ
" Õ µ Ô#
Example 1.9

$ TrainEnter

TunnelClear

TrainEnter ¸ TunnelClear

1.2.7 The Syntax of Propositional Logic

& '

propositional formula
¯ atomic formula È É
Ê
¯ compound formula

( ))

* true "
# false "
#
&
syntax

*

!
( )) well-
formed formula "wﬀ #
+ ( )) " #
Ô Õ metavariables

28 Propositional Logic

Ô Õ

true

false

Ô Ô

ÔÕ Ô Õ

ÔÕ Ô
Õ

1.2.8 Parentheses and Precedences

!
"

#
$

% $
! &

" %
'

"
(
$

" #

(
) (

$
% ! & * + %

! &
% %
&

"
$ $ & ! &

( % ,

È É Ê "
È É Ê

È É Ê

" ( %
,

-

. $

"
) (

"$
% " %
" % " % /

(
" $ $

Ô Õ Ö ×

The Language of Propositional Logic 29

Example 1.10

!
" #
$

$ %

&
'
(

)
%

)
*

+ '

)
,

Exercise 1.10 (Solution on page 407)

-

. / 0102

3 / 04

5 /

&
(

30 Propositional Logic

1.2.9 Syntax Trees

syntax tree

È É È É

È É
È É
!
È É È É

È É

"
# È É

" $
È É $ È É
# È É

È É
# È É È É

"

È É È É
!

!

%

&
È É È É

&

Example 1.11

'

È É Ê É (

È
É
Ê
É
The Language of Propositional Logic 31

È
É Ê É

É Ê

É Ê É

È É Ê É

!!
"

È É Ê É

Example 1.12

#
È É

#

" $$

È É

È É

È É

È É
%

È

É

É
%

É

&

# È É

Exercise 1.12 (Solution on page 407)

!
%' (

!

!

$ È É É È
) È É È
* È É È

+ È É Ê Ë

, È É Ê È É È Ê
32 Propositional Logic

1.3 Modelling with Propositional Logic

Example 1.13

...
if CabinPressure < MinPressure then PrepareForLanding;
if FlightHeight < MinHeight then PrepareForLanding;
...

...
if (CabinPressure < MinPressure and FlightHeight < MinHeight)
then PrepareForLanding;
...

Pressure Height

"
Land
PrepareForLanding #

$Pressure Land% $Height Land%

$Pressure Height% Land

#

Pressure Land
Height Land
"

Pressure Height
Land

#

Pressure Height
Land
"

#

& '

&

$Pressure Height% Land
Modelling with Propositional Logic 33

Example 1.14

! !

"

!

!
¯ !
!
¯ !
!
!
!

! !
!
!
!
!
# $% &
'

(

!
) " * $+,%'$+-+ '
"

.. !

)

Exercise 1.14 (Solution on page 408)

" /& 0 1 '

$ &

34 Propositional Logic

!"" #
$ % & # "
'
( #
) * #
+, - . "

Exercise 1.15 (Solution on page 410)

/ " +, 0
#

RightToCastleLeft 1 RightToCastleRight

2 # 1

MayCastleLeft 1 MayCastleRight

2 # 1

KingMoved
/ #"
LeftRookMoved 1 RightRookMoved

/ 1 #"

PieceBetweenLeft 1 PieceBetweenRight

/ " 1

KingAttack
/ "
Ambiguities of Natural Languages 35

¯ LeftSquareAttack RightSquareAttack

¯ KingMoveLeftAttack KingMoveRightAttack

Exercise 1.16 (Solution on page 410)

!
" #

# $ $

& '"

(
"

JonF )Joel* $

JonO )Joel* !
$

FonJ )Felix* $

FonO )Felix* !
$

OonJ )Oskar* $

OonF )Oskar* $

+ % # $
)Oskar*

(
"

1.4 Ambiguities of Natural Languages

,

#
-
&&.

/
"

- 0

Æ

36 Propositional Logic

Example 1.16

“Everyone who sits quietly for the next hour
will get an ice cream when we stop for petrol.”

!

"

“Anyone who misbehaves will not get ice cream.”

#

$

%
&
#

#

$

'

(

$

Example 1.17

)

“You may have coﬀee or tea with your meal.”

*

+

“You may have coﬀee with your meal
or you may have tea with your meal.”

#

, , -

Ambiguities of Natural Languages 37

!

"

" !

“You may have coﬀee with your meal

and you may have tea with your meal.”
#

!

!

“You may have coﬀee with your meal
and you may have tea with your meal,
but not both.”
$ %

!

!

& You may have coﬀee with your meal

& You may have tea with your meal

' ( ' (
#
!
!
!
! )* +
'
(

,

! modality
may

do

!

!

!

& You have coﬀee with your meal

& You have tea with your meal

!

'- (

38 Propositional Logic

“You have coﬀee with your meal
or you have tea with your meal,
but not both.”

“You have coﬀee but not tea with your meal
or you have tea but not coﬀee with your meal.”

“You do not have both coﬀee and tea with your meal.”

“You do not have coﬀee with your meal
or you do not have tea with your meal.”
!

"

#

$

Example 1.18

%

&

$

! ' $

(

) * $

+

“If Carlos is a man, then Carlos is the King of Spain.”

, $

+

“If Carlos is a woman, then Carlos is the King of Spain.”

-

#

%

$

+
Ambiguities of Natural Languages 39

“If Carlos is a woman, then Carlos is the Queen of Spain.”

“If I told you once, I told you a hundred times!”

!

“If he ever pays me back, then I’ll be a monkey’s uncle!”

"

! #

Example 1.19

$

“If you understand implication, then you will pass the exam.”

% $
&

' $

!

(

)

* $

+

, $ -

#

40 Propositional Logic

Exercise 1.19 (Solution on page 411)

!

"

Exercise 1.20 (Solution on page 411)

# "

1.5 Truth Tables

$

%

&

'

%

#
(

)

truth table
* negation #

'

*

T
F +

F T
T F

Truth Tables 41

' $ ' $

F F F F F F
F T T F T F
T F T T F F
T T T T T T
& % & %

' $ ' $

F F T F F T
F T T F T F
T F F T F F
T T T T T T
& % & %

Example 1.20

!
“Everyone who sits quietly for the next hour
will get an ice cream when we stop for petrol.”

"

Quiet # You sit quietly
Ice # You get an ice cream

$

Quiet Ice %
& %

!
' $
Quiet Ice Quiet Ice
F F T
F T T
T F F
T T T
& %
ÓÒÐÝ

Quiet Ice
%

42 Propositional Logic

!

"

#$

Exercise 1.21 (Solution on page 411)

% &' (() *

“If you understand implication, then you will pass the exam.”

!

Example 1.21

+

, , , ,
#
-
Cat . Catherine goes to the party
Jim . Jim goes to the party
Jules . Jules goes to the party
+ #
Cat Jim Jules
! + ,
, # /

Cat Jim Jules
0 !

Truth Tables 43

' $
Jim Jules
Cat Jim Jules Jim Jules Cat Jim Jules
F F F F T T
F F T F T T
F T F F T T
F T T T F T
T F F F T T
T F T F T T
T T F F T T
T T T T F F
& %

Cat Jim Jules

Jim
Jules

Cat Jim Jules

!

" # $
%
' $
Cat Jim Jules Cat Jim Jules
F F F F T T F F F
F F T F T T F F T
F T F F T T T F F
F T T F T F T T T
T F F T T T F F F
T F T T T T F F T
T T F T T T T F F
T T T T F F T T T
´¼µ ´¼µ ´¼µ ´½µ (4) ´¿µ ´½µ ´¾µ ´½µ
& %

%

&

'

Cat Jim Jules
(

44 Propositional Logic

Jim Jules

Cat Jim Jules

Exercise 1.22 (Solution on page 412)

!

È " É" Ê Ë # $

#
$
Ò

#

Exercise 1.23 (Solution on page 412)

%

& È É
È É È É
È É Ê Ë

Exercise 1.24 (Solution on page 413)

'(
)
Ô Õ
*
' $
Ô Õ ÔÕ
F F F
F T T
T F T
T T F
& %

" Ô Õ

"
" Ô Õ

%
( &&+ , (-

Ô Õ

Equivalences and Valid Arguments 45

1.6 Equivalences and Valid Arguments

Cat Jim Jules Cat Jim
Jules

!

Cat Jim Jules Cat Jim
Jules

Cat Jim Jules Cat Jim Jules

"
#

$

logically equivalent

tautology

valid
contradiction

unsatisﬁable

%

&

&

satisﬁable
Example 1.24

"
'
!

(
#

F T T F T F
T F T T F F

(

(

)
* +

+
46 Propositional Logic

Exercise 1.25 (Solution on page 413)

"

# $

% % & ' ()

Either this man is dead or my watch has stopped.

My watch is still ticking.
Therefore
This man is dead.

"
#
*

%
%
# )

Dead Watch Watch Dead

+ %

%
$

# , &

)

' $
Dead Watch Dead Watch Watch Dead
F F F F F F T F T F
F T F T T F F T T F
T F T T F T T F T T
T T T T T F F T T T
& %

- %
. /)

If my dog barks, then my dog doesn’t bite.

My dog doesn’t bark.
Therefore
My dog bites.
Algebraic Laws for Logical Equivalences 47

' $
Barks Bites Barks Bites Barks Bites
F F F T T F T T F F F
F T F T F T T T F T T
T F T T T F F F T T F
T T T F F T F F T T T
& %

counterexample

Exercise 1.26 (Solution on page 414)

!" ##$

%

& Pressure Land Height Land

& Pressure Height Land(

& Pressure Height Land

)

%

*

!"

1.7 Algebraic Laws for Logical Equivalences

+

*
*

,

*

- "
$ ./0 & 12

$ . / 0 & $ . / $ 0
& #1 / #0 & 12

/ & / (

48 Propositional Logic

Commutativity Laws

Associativity Laws

! " !
"
! " !
"

Idempotence Laws

Distributivity Laws

! " !
" ! "
! " !
" ! "

De Morgan’s Laws

! "
! "
Double Negation Law

Tautology Laws
true true true

Contradiction Laws
false false false

Excluded Middle Laws

true false

Absorption Laws

! "
! "

Implication Law

Algebraic Laws for Logical Equivalences 49

Contrapositive Law

Equivalence Law

"

#
$ %

&
'

'

(

Example 1.26

) '

'

!

true

) '

'

true

Example 1.27

)

!
50 Propositional Logic

true

Exercise 1.27 (Solution on page 415)

!
"
#
$
%
&

1.8 Additional Exercises

! '

(

)!*

+
),

-+
).

+
)

(+
Additional Exercises 51

!

"

!

#

" $

%

%

"

"
&

%

" &

&

' #

%( ) **

+

Æ

, -

* **

+ .
**&

/*
+ .

*
**
+ .
**

"

**

½ + .
**

/*

*
**&
*
¾ + .
**

/*

*
**&
*

)

0 *

**

1 2

3

4 5

4
52 Propositional Logic

! "
#

"

#
$

#
$

% & CatAway

' ! MicePlay

'
!
' !
' !

( )

“Every card with a circle on one side

always has stripes on the other side.”

+

'
" Wason Selection Test
,
-
.

/(00 1

*

2345
Additional Exercises 53

!

!

"

#
$
% & '

()(*! (+,

-

& !
'

!

. &

&
/ 0
1

& !
2

&

'

3 !

()(*

&
3 !

(+,

4 )

#

&
&

!

2
!

& /2
!

2

!
&

5
$
6 5

! &

! " &

! ! )
7
) ! 87

5
9 5 ) $ " 7
$
: ) 3

; ! #

5 3

&
& !

3

&
&
5 3

&
& !
2

&
& ! &

5 3
!

&

) <

&
54 Propositional Logic

!
"

#$ %

'

(

'

)

(

#*

' ,

! -

!
.

0

0

1 "

1 0

'

2

.

30

1

1

! !

) 4 1

Additional Exercises 55

! "

!

#

$

%

&
' (
) (
*
% )

+, -

.&
!
"
! +/0

! %
%
0 %

!

+1 -

!
&
!

%
!

Chapter 2

Sets

! "

# $

% & ' % & % (&
% & % & % & % &
% & #

2.1 Set Notation

) set * # *

elements

members # * cardinality

false true +
, - ./ +

+

0 1
2 )

) 3 4 5 6 ! +

F. Moller, G. Struth, Modelling Computing Systems,

Undergraduate Topics in Computer Science,
DOI 10.1007/978-1-84800-322-4_3, © Springer-Verlag London 2013
58 Sets

! "

#
¯ $ %
&&
'

'
% ( $$ $ $(

) *

+ +

, - +

.
)
$( $ / '

) 0 1 2

3

4

set-builder notation #

5 3

6

Example 2.1

#
$

0 /

#
# 0 /

1 7
#
#
1 7

#

#

#
#

Membership, Equality and Inclusion 59

! "

! " # $

$ # " ! " # $

%
!

& '

(

Exercise 2.1 (Solution on page 416)

)

" % !
*
# %

$ % + ,---

. % / 0 Æ

2.2 Membership, Equality and Inclusion

(
1
2 Membership

3 $ 3 ". 4 3 $ 3 ". 5

60 Sets

" !

Exercise 2.2 (Solution on page 416)

# $ % & % &$

! ' % ( ) ) * !

)! ' % ) ( ) * !

Exercise 2.3 (Solution on page 416)

#& % $+

! ) ) !
)! ) ) !
! ) ) !
! !
*! !

,& - equal

. ! , $
& $ $ $ &
/ ! "$

(

(

!

0 $ 1 $Æ& -

&2 & !

Exercise 2.4 (Solution on page 416)

#& % 3$ +

Membership, Equality and Inclusion 61

subset

superset

!

"

#

$ % &

Example 2.4

"

!

"

'
'
Venn diagrams (

& )

* + ,
* +
* + , -
.

& /
'

universe of discourse

)

0
1!
62 Sets

!" ## $

# % #" &'
# ! ( '
#&! & !&
(

& # )& "

(
)& "
)

Exercise 2.5 (Solution on page 416)

*# &) )&&' && & +

, &! $& ' # & )&&' # & &)
! & &) '# &!$&

- reﬂexive & )& $"

- antisymmetric )
- transitive )

.&&$ " ' # & # &(
#& " &
& )& #
Sets and Properties 63

2.3 Sets and Properties

Primes

!
Primes "

Primes

#$

$

%

$ & '

#$
$

(

!
$

)

$ $
"

(
!

#$

$

Example 2.5

*

$

&

$

$

$ ' +$$!

,

- Animals

Humans

$
Humans Animals "

(
Humans Animals

Example 2.6

.
Ê
/ $$
$
"

64 Sets

Ê
Ê
Ê
Ê

! "

Example 2.7

#
"

$ % & #' (

!! " )

"

$ % & #' (

2.3.1 Russell’s Paradox

)
" !

*
" "! +

!

-

* '
. )

. #

. - "

/

0!!

)
" !! " 1

"

Operations on Sets 65

! Russell’s Paradox

"
#
$ !

%

&
'
#
#
( &

Exercise 2.7 (Solution on page 416)

#

) '

* + , + ( "- .

2.4 Operations on Sets

$

&
$

2.4.1 Union
union
/ 0'
) '

66 Sets

Example 2.8

Example 2.9

"

# $

% &

# $

% & '

(

2.4.2 Intersection
intersection

)

"% "
*
! *
"

Example 2.10

!
Operations on Sets 67

Example 2.11

disjoint

!
"

"

Theorem 2.11 Inclusion-Exclusion Principle

2.4.3 Diﬀerence
diﬀerence

#

$

Í

Example 2.12

% & ' ( ) & ( * + %, % ' )

68 Sets

Example 2.13

" #$

2.4.4 Complement
complement %# &
' ' & (
(

' & $ )# *

&$ #

Example 2.14

+'& ' ' , - $

, - $

, -

Example 2.15

+'& ' ' $

& & !
! . & &

Operations on Sets 69

Exercise 2.15 (Solution on page 416)

! "

# #

# $ %

# $ % #

Exercise 2.16 (Solution on page 417)

& !
' #
# ( !

)" ) '" *

# ( !

)" ) '" *

# +
!

*

# (
!
*

2.4.5 Powerset
,
powerset $ %
"'

$ % #
,
"!
$ %
#
( "! $ % $ %#

+
) ' "' # (

') ¬Ò $ %
"'

¬Ò $% - #

70 Sets

Example 2.16

" # $% &' ( )

# $% &' (

# $% &' (
# $% # &' # (
$% &' $% ( &' (
# $% &' # $% (
# &' ( $% &' (

# $% &' (

%

Operations on Sets 71

Example 2.17

! "! #

$ %
&
' (
"

Friends #
$ %
&
'

)

"!

! Friends * " "" $ &

! !

) "!

#
%
' Friends

Exercise 2.17 (Solution on page 417)

+
Friends Friends
,
$ -

" ./ ( !

0 1

Exercise 2.18 (Solution on page 418)

*
"!

2
( !
1

Exercise 2.19 (Solution on page 418)

3

! 1
72 Sets

2.4.6 Generalised Union and Intersection

! " ! " #
$

! " % ! " ! " % ! "

% %

&
!"
$

Ë % $

Ì % $

% % Ì
Ë

$

' %
Ë % Ì
( %
Ë ! " % Ì ! "
)
Ë Ì
% %

#

* Ë

+ Ì

Example 2.19

+ ,+'-'

ClassLists

,+'-' ClassLists # Students

Ordered Pairs and Cartesian Products 73

Students
Ë ClassLists
Ì ClassLists

Exercise 2.20 (Solution on page 418)

Ì ¬Ò Ë ¬Ò

2.5 Ordered Pairs and Cartesian Products

ordered pair ﬁrst coordinate
second coordinate !
" # $
! # ! $ %
"

&

Cartesian product
'

(

Ê Ê Ê ¾
!
Example 2.20

)
*+

, *+

,
' -
.)/ 0

+ + + 1 +
1 + 1 1 +

+ 1
74 Sets

Example 2.21

Keys Values Keys
Values

! "

#
$

#

%
IDNumbers & '( )*+,-
'.
" /0+)-
'1 *23)-
'! 4*5+-

! "

%
CapitalCities & '. 6
-
'6 7
-
'( -
'
-

8

Æ
. "
& ' - %

' -

#

$

# Ê & Ê Ê Ê
¿

9

$

& &
Ordered Pairs and Cartesian Products 75

Example 2.22

Example 2.23

pixel

!
! "# $$%
#
&

" #
' RGB model

(
% !¿ % ! ) Ê * %
%
#
+ # ,
% % %

#

-

% % % % % % .
(
*
Pixel ) !
!
Colour ) % !¿

(
Point ) Pixel Colour

# "
(

Exercise 2.23 (Solution on page 418)

"

/0 # / 0 1(

76 Sets

2.6 Modelling with Sets

Example 2.24

! "

#

$

%

&

! '
(

)

Exercise 2.24 (Solution on page 418)

*

+ , -
!!.

/
"

!

, 0 /)

1 "

2 " /
3 4

Modelling with Sets 77

Exercise 2.25 (Solution on page 419)

All babies are illogical.
Nobody is despised who can manage a crocodile.
Illogical persons are despised.

!

! !!

Exercise 2.26 (Solution on page 420)

All oceans are full of water.
No ponds are oceans.
Therefore no ponds are full of water.

Example 2.26

!
" #$ !

"
" !
%&

!

'(

"

!

)
*" %%

"

!
"

!
+
*
,
- !
"

, , ,
, , ,
,

78 Sets

¯

!

¯ "

!

#

$

¯ %# && ! '

(

¯ )

!
'

*

¯ &+
&, '

-

¯ ,
&*
'

+

¯ )

-,

!

,

.

, ( +
* $
-

%
.

/

- , $ * + ( 0 ,
#

!

.

/
Algebraic Laws for Set Identities 79

¯ ¯
¯¯¯ ¯ ¯
¯ ¯ ¯ ¯ ¯
¯ ¯ ¯ ¯¯ ¯¯
¯ ¯
¯ ¯ ¯¯ ¯ ¯ ¯¯
¯¯ ¯ ¯ ¯ ¯¯ ¯
¯ ¯
¯

2.7 Algebraic Laws for Set Identities

! "

"

#

$

Commutativity Laws
% %
Associativity Laws
& ' % & ' & ' % & '

Idempotence Laws
% %
Distributivity Laws
& ' % & ' & ' & ' % & ' & '

De Morgan’s Laws
& ' % & ' %
Double Complement Law
80 Sets

Universe Laws

Empty Set Laws

Complement Laws

Absorption Laws

Exercise 2.27 (Solution on page 420)

!

Example 2.27

"
#

Exercise 2.28 (Solution on page 420)

$

%
&
! ' (

! #
! ! !
Logical Equivalences versus Set Identities 81

Example 2.28

! " #
$ " " " #

% #

Exercise 2.29 (Solution on page 421)

&
#

2.8 Logical Equivalences versus Set Identities

'
$ ( $ ) *#+
)
) ,#+# -

. .#
Commutativity Laws Commutativity Laws
"
"
Associativity Laws Associativity Laws
! ! ! " !
! ! ! " !
Idempotence Laws Idempotence Laws
"
82 Sets

Distributivity Laws Distributivity Laws

De Morgan’s Laws De Morgan’s Laws

Double Negation Law Double Complement Law

Tautology Laws Universe Laws

true true
true

Contradiction Laws Empty Set Laws

false
false false

Excluded Middle Laws Complement Laws

true
false

Absorption Laws Absorption Laws

false true

Additional Exercises 83

Example 2.29

Implication Law

true

!"

Exercise 2.30 (Solution on page 421)

#

$

Contrapositive Law
% Equivalence Law " "

$

' $

(
Exercise 2.31 (Solution on page 421)

)

"
*

+

2.9 Additional Exercises

,
% - . /
. / 0 1 2
% . 0 1

)

3
"
"
84 Sets

!

"

## #

$

%
##

& '
##

(

(

) !
* " $ &

+

##
#

*

,

, " $ &

- . symmetric diﬀerence

/

#

0

## #

Additional Exercises 85

!
! "

# $

% %

& &

' ( !(

)

'

*' ' +

% ,- .' ( " '

!

'

$ '
/( ' -
%
$ '

( '

% " 0 (

'

'

% % *

( ! '
( ''

! "
#
% 1
' ! ,- 2

%
1 ! .' 2

.'

!

% % *
3 !
'

' 4 3 ' !

' ( *
#

!
2
%

!
,- 2

.
"

%
( !
!

!
" '

/ * $

$
% !

% ( %

* ( !
$

1

! * *% ! ' % ! ( '

! !
'

/ 5
#
* * ( !

6 . 7
autological
*
'% 8
9

"

: 8
( * 9
"

( * :

%
$ ( * .( 7

"
* heterological '% 8 "9

8' ( * 9
"
86 Sets

Chapter 3

Boolean Algebras and Circuits

!
Boolean
algebras

#

$ % &

& "

logic gates

% '
(

& '

(

F '( T '
(

)

*

3.1 Boolean Algebras

Boolean algebra

'

(

% &
zero unit

+ sum product

¼

complementation "

' (

'

,
(

+ ¼
"

Laws of Boolean Algebra - . &

F. Moller, G. Struth, Modelling Computing Systems,

Undergraduate Topics in Computer Science,
DOI 10.1007/978-1-84800-322-4_4, © Springer-Verlag London 2013
88 Boolean Algebras and Circuits

Commutativity:

Associativity:

Distributivity:

Identity:

Complement: ¼

¼

! "

# $ # " !! %"
"

Example 3.1 The Boolean Algebra of Sets

&

& & & ' # & & & & ! #
¼

$ !& & !

!(" )! *+
Commutativity:

Associativity:

Distributivity:

Identity:

Complement:

Boolean Algebras 89

Example 3.2 The Boolean Algebra of Propositions

false true

¼

"

# $
%
&'
Commutativity:

Associativity: ! !

! !

Distributivity: ! !
!
! !
!
Identity: false
true
Complement: true
false

Example 3.3 The two-valued Boolean Algebra

($

$

# '

¼

)

$
$

Exercise 3.3 (Solution on page 421)

*
(

+ $
$

$

¼

, -$
!!
$ ¼ ¼
90 Boolean Algebras and Circuits

3.2 Deriving Identities in Boolean Algebras

!

"

# $
! %&

Theorem 3.3 Further Distributive Laws

Ü ' Ý Þ ( ÜÞ ' ÝÞ

ÜÝ ' Þ ( Ü ' Þ Ý ' Þ

Proof: " ) !

Ü ' Ý Þ ( Þ Ü ' Ý

( ÞÜ ' ÞÝ

( ÜÞ ' ÝÞ

Theorem 3.4 Idempotence Laws

Ü'Ü ( Ü

ÜÜ ( Ü

Proof: " ) !

Ü ' Ü ( Ü ' Ü*

( Ü ' ÜÜ ' Ü ¼

( Ü ' ÜÜ ¼

( Ü'+

( Ü

Theorem 3.5 Domination Laws

Ü'* ( *

Ü+ ( +

Deriving Identities in Boolean Algebras 91

Proof:

Ü Ü Ü Ü
¼

Ü Ü Ü

ÜÜ ¼

Theorem 3.6 Absorption Laws

ÜÝ Ü
Ü

Ü Ü Ý Ü

Proof:

Ü ÜÝ Ü ÜÝ
Ü Ý

ÜÝ
Ü
Ü

Theorem 3.7

Ü Ý ÜÞ ÜÝ ÜÞ Ý Þ

Proof:
Ý Ý Ü Ý

Ý Ü Þ

ÝÜ ÝÞ

ÞÜ ÞÝ

Þ Ü Ý

Þ Ü Þ

Þ

92 Boolean Algebras and Circuits

Ü Ü ¼

ÜÜ ! "

Ý #
¼

Ü

¼

Theorem 3.8 Uniqueness of Complement

ÜÝ
ÜÝ Ý Ü
Ü
¼ ¼

Ü Ü ÜÜ
¼ ¼

Proof: $
Ü Ý ÜÝ
ÜÝ

ÜÜ
¼

ÜÝ
ÜÜ ¼

! %& Ý Ü ¼

Theorem 3.9 Involution Law

'Ü (
¼ ¼
Ü

Proof:
Ü ¼
'Ü (
¼ ¼

Ü Ü ¼

Ü 'Ü (
¼ ¼ ¼

ÜÜ ¼

! %& 'Ü ( Ü ¼ ¼

Exercise 3.9 (Solution on page 422)

)
¼ ¼

Theorem 3.10 De Morgan Laws

'Ü Ý ( ¼
ÜÝ ¼ ¼

'ÜÝ( ¼
Ü ¼
Ý ¼

The Duality Principle 93

Proof:

Ü ÝÜ Ý Ü Ý Ü Ý
¼ ¼ ¼ ¼

!""
#" $% &

Ü Ý Ü Ý
¼ ¼ ¼

Ü ÝÜ Ý ÜÜ Ý ÝÜ Ý

¼ ¼ ¼ ¼ ¼ ¼

Ý Ü

¼ ¼

Ü Ý Ü Ý Ü Ý Ü Ü Ý Ý
¼ ¼ ¼ ¼

Ý Ü

Exercise 3.10 (Solution on page 422)

'
&
"
ÜÝ Ü Ý ÜÝ Ü Ý
¼ ¼ ¼ ¼ ¼

( ) ÜÝ ÜÞ Ü Ý Ü Þ

Ý Þ ¼ ¼

$ ) ÜÝ
Ü Ý
* Ü Ý ÜÝ Ü Ý Ý ¼ ¼

3.3 The Duality Principle

+ " , &
dual "
&&

&
- &

"

& , &

"

"

# "
Ü Ý Þ ÜÝ Þ ¼ ¼

# & "
, &
Theorem 3.11 The Principle of Duality

Proof: #

"

" "

" "
94 Boolean Algebras and Circuits

Example 3.11

ÜÜÝ Ü!

Ü Ü Ý Ü "Ü Ý

Ü "Ý

Ü Ý"

Ü"

#

$
Ü ÜÝ Ü
%&'

!
'

($
'
)

)

'

$

'

'
(

$

*

'

( # '

*
+ , '

+ ,

Exercise 3.11 (Solution on page 423)

-

.( %/"

/ ÜÝ Ü¼ Ý ¼ ¼ ÜÝ ¼
Ü¼ Ý

0 # ÜÝ Ü Þ Ü Ý
¼
Ü Þ ¼

Ý Þ
% # Ü Ý "
Ü Ý "

1 Ü " ' ' Ý ÜÝ ¼

Ü¼ Ý Ý
Logic Gates and Digital Circuits 95

3.4 Logic Gates and Digital Circuits

bits

!

" #

$

%

Example 3.12

"!

&

"!
'

(
&

# (

"

)

*
(
"!

) (

(
+

(
"

96 Boolean Algebras and Circuits

OR gates AND gates NOT gates
OR gate

Ü
Ý

ÜÝ
Ü Ý
ÜÝ !

"

Ü Ü Ý
Ý

AND gate

Ü
Ý

ÜÝ

Ü Ý
Ü Ý !

"

Ü Ü Ý
Ý

NOT gate

Ü

Ü ¼

Ü!
Ü
¼

! Ü

"

Ü Ü ¼

#

Ü Ý Ü Ý Ü Ý ÜÝ Ü Ü ¼

! ! ! ! ! ! !
! ! ! !
! ! !

$

%
&

% '

(& )) *

ÜÝ

ÜÝ #

Logic Gates and Digital Circuits 97

Example 3.13

!

"
Ü
Ý Ù
Þ Ú Û

# Ü$ Ý Þ
# Ü Ý

%&
Ù ' ÜÝ ($
Þ
%)#

Ú ' Þ #
Ù Ú
*

¼

)+
* Û ' Ù , Ú
# -

$
$

Û ' ÜÝ , Þ ¼

#

"

Ü Ý Þ Ù Ú Û
. . . . / /
. . / . . .
. / . . / /
. / / . . .
/ . . . / /
/ . / . . .
/ / . / / /
/ / / / . /

0
$ Ü'/$ Ý '. Þ '/$

%& .$

%)# 1

)+ .$

Û

."
Ü'/
Ý'. .
Þ'/ . Û'.

#
*
Û ' ÜÝ , Þ ¼

È É Ê $
$

98 Boolean Algebras and Circuits

Example 3.14

¯

! "#
$
¯

"#
$
¯

"#
$
¯

! %&

$ '
¯ !

%&

! $ '

( ( ( ( ( ( ( (
( ( ) ( ( ( ( (
( ) ( ( ( ( ( (
( ) ) ( ( ) ( )
) ( ( ( ( ( ( (
) ( ) ( ) ( ) )
) ) ( ) ( ( ) )
) ) ) ) ) ) ) )
"

$ ' $ ' ' $ ' '
Logic Gates and Digital Circuits 99

Exercise 3.14 (Solution on page 423)

exclusive-OR gate XOR gate

¨
¨
!
!
!

!

"

!
!

¨
"

!
#

Exercise 3.15 (Solution on page 423)

$
# %

Exercise 3.16 (Solution on page 424)

&

'

# '

¯
!
(
¯

!
(
¯

!

!
#

100 Boolean Algebras and Circuits

3.5 Making Computers Add

3.5.1 Binary Numbers

!

"

#

$ %
$
&

% ' ( %

)*+,

-

¯ , , $

¯ + + $

¯ * *

! "$

¯ ) )

! "

)*+, . ) ¿
. ) . )

* *
¾
/ . . *

+ +
½
/ . . +

, ,
¼
/ . . ,
)*+,

0

'

'
!" ( %

-
Making Computers Add 101

! !

" "

$% & & &% & ' %

& &

&%
&
&
(

&%
%) %
(
* &
& +

Example 3.16

( ,
&%)

¯ & -
,
(
#

¯ &
#
(
-

¯ &
-
(

¯ &

(

. & , - &% )

¢ ¢ - -
¢ ¢

¢ ¢ !

¢ ¢ "
¢ ¢

¢ ¢
,
102 Boolean Algebras and Circuits

3.5.2 Adding Binary Numbers

Example 3.17

!!!"! !"!!"

#

$
½ ½ ½

!!!"!
!"!!"
!!""!!

!

"

!

!
%

Exercise 3.17 (Solution on page 424)

% &

#
'

(
)# #
¿ ¾ * *#
$

Making Computers Add 103

3.5.3 Building Half Adders

! "#$% &

%

'

half
adder
(
) &

* %

+
%
,

-

.+ , /
¼ ¼

%
)

% ¼ ¼

+

¼
¼

¼
/ ¼
+

¼
/ ¼

0

12

+

, / ¼ ¼

+ 12 % 1(
(3 4
+

'
4

)

0

)

5 6 % &
+
104 Boolean Algebras and Circuits

¼

¼ ¼ ¼

¼ ¼ ¼

¼ ¼

¼ ¼¼ ¼¼

¼ ¼

!

"

# $

¼

%

#&

¼ ¼

'

$
(

)
)

#

*
+

3.5.4 Building Full Adders
'

! !
,

(

-

"

, full adder

./

0
1 2

$

Making Computers Add 105

¼ ¼ ¼ ¼ ¼ ¼

¼ ¼ ¼

¼ ¼

!"#
¼ ¼ ¼

¼ ¼ ¼ ¼ ¼ ¼

" # " #
¼ ¼

¼ ¼ ¼

¼ ¼

¼ ¼ ¼

" # " #
¼ ¼
¼

$
%&

'( ÜØ
¼ ¼

Ø

'( ÝÞ

3.5.5 Putting It All Together

' ) *

+
,*

,* ¿¾

-*

'(

.(

.(

.(

/ 0

) %

106 Boolean Algebras and Circuits

3.6 Additional Exercises

!
! "
#
$ # % &

&

' & (

lcm ")

gcd ") $ &
¼

* + $ # * , #

#
-.
#
/
0
¬Ò "

& ( + !
¼

!"1 2
! !

% " $ & ! ( $
¼ ¼

" 3 "

, " $ ! ( $ &
¼ ¼

" 3 "

4 NAND gate
0
!"5

& & $
&
&
&

$
&

)

"

6 78 67

" 3
( !
¼

9 NOR gate
0
!"5

& & $

& &
& &
&
Additional Exercises 107

! ""

# $ #

"
% &
¼

'

"" (

% %
# % %
¼ ¼

%

¼ ¼

# #

#&
(
# )

* +( ,

" " -
# . #
# + )" + , )"
/ " 01 + 01
+ , & )" "2 &

"
3 multiplexer

¼ ½

) 4
108 Boolean Algebras and Circuits

× Ü ¼ Ü½ Ö

Ü¼

Ö

Ü½

×

×
selector Ö
Ü¼ Ü½ ×

Ö ! × Ü¼ " ×Ü½ #
¼
Chapter 4

Predicate Logic

! "

%

predicates &

" "

& quantiﬁers &

4.1 Predicates and Free Variables

'
( " #

Ü # Ü

)

" (

" *

" #

Ü # Ü È
" *
Ü
" È

" predicate È +Ü, - *
Ü

È .

" "

Ü " $ "

F. Moller, G. Struth, Modelling Computing Systems,

Undergraduate Topics in Computer Science,
DOI 10.1007/978-1-84800-322-4_5, © Springer-Verlag London 2013
110 Predicate Logic

!

"

#

free variable $

% &
&
' (
' ))
#
!

truth set

#

*
"

Example 4.1

+

, "

- . /

, , . + ,

"

0 1

. ,

- / .
+ ,

. ,

2

$

0 1 0 1

0 1 0 1 #
3 3

#

4

#

Quantiﬁers and Bound Variables 111

Example 4.2

!

"
"

!

#$

Exercise 4.2 (Solution on page 424)

& '

(
) & '
(
& '

(
& '

* & (

4.2 Quantiﬁers and Bound Variables

+ , -$ . /

0

1

!

/

,
-$
. /

0

112 Predicate Logic

Children

#Ü$
%
Ü

"
% % " &

%
% "

'

& "

#$ # $ #$ #

$
% "

(

#Ü$ "

) "

"

# #$ # $ #$ #

$$

# #$ # $ #$ #
$$

# #$ # $ #$ #
$$

# #$ # $ #$ #
$$

)

)

% %
" " %

*

"
+
#Ü$
Ü

" % ,

-

'

#.$ #/$ #0$ #11$ #1.$

2
,

#Ü$

Ü , % ,

-
'

Quantiﬁers and Bound Variables 113

quantiﬁcation !! "

!

!

!

#!

4.2.1 Universal Quantiﬁcation

$!

!

È Ü

Ü
!

%

Ü È Ü
!!

Ü È Ü &

" !

È Ü
'

Ü
#!
universal quantiﬁcation
(

)
(
*+ ,

! Ü
!

"

Ü Ü
!! " !

! !
! '!
!

!
!

!

!
!

-
! Ü Ü % !

!

#!
'
Ü

'
!
& bound variable &
' '" !
.
/Ü0

Example 4.3

Ü À Ü
!

À Ü 1 Ü

114 Predicate Logic

Example 4.4

!"
Ü Ã Ü É Ü
Ã Ü #
Ü
ÉÜ #
Ü

!"

" " "
"

"
"

Ã Ü É Ü

"
Ü

$ Ã Ü
$
Ü

$ ÉÜ
%

Ü

&

ÉÜ

"
"

& "
'
!"
!"

Ü Ã Ü É Ü

Ü Ã Ü É Ü

"
Quantiﬁers and Bound Variables 115

Example 4.5

Exercise 4.5 (Solution on page 424)

" # $

% & $

' ( $

4.2.2 Existential Quantiﬁcation

)

116 Predicate Logic

Ü
È Ü

È Ü

Ü

Ü Ü

! Ü Ü Ü ! ! ! !
" # $ Ü% " # " #
!

Example 4.6

Ü À Ü
À Ü ( Ü
&
!

& À Ü
'
! )
*+ ,
! & ,
! !

#

Example 4.7

'
Quantiﬁers and Bound Variables 117

Exercise 4.7 (Solution on page 424)

# $

% &

Exercise 4.8 (Solution on page 425)

!
"#
!

118 Predicate Logic

4.2.3 Bounded Quantiﬁcations

bounded quantiﬁcation

!
!
"

#
$
# !

"
Quantiﬁers and Bound Variables 119

Example 4.8

! " # $%& ' ()* + &

' ' & $ , $¾ &

, ¾ , ¾
-
' &
'
, ¾ &

&

, ¾ &

Example 4.9

.

' //
# ((% ' )$ 0
& 1
2 3

& '

-

4 4

&

&
'
'

' 5

3

5

3 0
4
& 6Oskar7

8 , 0
1 2 3

9
,

6Joel7
9 6Felix7

9 6Oskar 7
1
&

-

( #

)

'

120 Predicate Logic

Oskar

Exercise 4.9 (Solution on page 425)

!

"

4.3 Rules for Quantiﬁcation

# $ % $ &
$ $ % $ ' &

($ )& $ % $
& $ $ % $ ' &

* + ,

$% ($ - ) - .$&

($ - ) - .$ /$
$% $ 0 *

Rules for Quantiﬁcation 121

Example 4.10

Ü !Ü"

# $ $ # !Ü"

Ü

#

%

&
'
Children (

)
) %

%

*

! "

! "

'

! ) " #

'
! "

*
#

! " ! "

+ %

# %

,

'

! "

# $ $ # ! "

'
! "

*
#

! "
! "

Exercise 4.10 (Solution on page 425)

#

) #

%

)

*

- )
122 Predicate Logic

! " # $ % &

' ' #$
(

ÜÈ Ü ÉÜ ÜÈ Ü ÜÉÜ

ÜÈ Ü ÉÜ ÜÈ Ü ÜÉÜ
ÜÈ Ü ÉÜ ÜÈ Ü ÜÉÜ
) ÜÈ Ü ÉÜ ÜÈ Ü ÜÉÜ
*

+
, È Ü ÉÜ ' Ü$ È Ü
' Ü ÉÜ ' Ü
"$ È Ü ' Ü ÉÜ
' Ü$ È Ü ÉÜ ' Ü
+
, È Ü ÉÜ ' Ü$ È Ü
' Ü ÉÜ ' Ü
!$ È Ü '$ ÉÜ
'$ È Ü ÉÜ
' Ü
- %$ " % (

Ü
Ü Ü Ü
Rules for Quantiﬁcation 123

Ü Ü Ü

!

"
Ü
¼

# $
"

%
&

"

&
' ("
&

&

"

&

)

&

&

*

)

"
)

"
)

!

"
#
¼

+ $
"
%

&

&

&

("

&

&

&

, -

)

"

'

$

)

-

*
-

%

.

"

)
*

)

/

-

124 Predicate Logic

Example 4.11

Ê

Ê

! " !!

!
"

!

!
! # !
!

4.4 Modelling in Predicate Logic

! $ !

%

Example 4.12

&
' !(( )#
$

All babies are illogical.
Nobody is despised who can manage a crocodile.
Illogical persons are despised.

!
* !
!

+
+
+
+
Modelling in Predicate Logic 125

Ü

!

"

"

Exercise 4.12 (Solution on page 426)

#

$ % &

'

(

Example 4.13

#
)
* +, -- . .

/
!

,
. * 0

& --

$
--
#
) $

!
1

" 1 2

,

1
!

3 4.5

.
6

.

."
126 Predicate Logic

¯

¯

¯
! " #

$ % & ' $ % (

) # )
* #

$ + ,% $ -%
$. % $. / %
$0 0% $0 .% $0 - % $0 + +%
$ / .% $ , 0% $ - ,%
$/ . .% $/ / ,% $/ + /%
$, 0 % $, -% $, / %
$- . 0% $- 0 % $- , -% $- %
$+ / % $+ ,%
$ % $ . +%
1* # " #

Additional Exercises 127

! !
" ! #$!
! %&!

# #$! !

' #$! #$!

$ #$! %&!

% %&! !

( %&! #$!

& %&! %&!

)*

+
,

--

.,

/
,
0
" .,

,
,

.,
1
,
,

# .,

,
,

2

,

3 ,

*
1
,

,

Exercise 4.13 (Solution on page 426)

4,

4 --
)
#

4.5 Additional Exercises

5

,

,

*

1

./

+ .

128 Predicate Logic

! "#

$
% &%

"

' (

"#)

* "#

%
% %

%

)

%

$

$
$

%
"$
%
&%

$
)

"$ $

%

+ "#
"

% % Ê
%

,
,
¾
¾

Additional Exercises 129

! !

"

#

$ % &
' ( ) *

(* *

)
*

+ *

(* !, -
& .
*

+

/0 1 2

!"
#
$
%"
# &

!"
& &

$
%"
.
!

&
// 1 2

# '&

!"
( ! '' "
# '&

"
.

!

&
/3 #

"

(

!"
#!
''

"
&

''

"
Chapter 5

Proof Strategies

! proof "
#

Æ

theorems

$
%

" #

(

(

(

)

'

(

*

' -
.

/ )0

1 )

/2 3 1

F. Moller, G. Struth, Modelling Computing Systems,

Undergraduate Topics in Computer Science,
DOI 10.1007/978-1-84800-322-4_6, © Springer-Verlag London 2013
132 Proof Strategies

proof strategies

"
#

$

5.1 A First Example

! %
&

&

!

&
Í

Theorem 5.1

Proof: ' (

) *
&

+
,

A First Example 133

!

"
! #! !

$

#
$

%

&

$

' (

!

)

$

# $

introduction strategies

#
$

#

!

*

(

134 Proof Strategies

"

"

#$

%

Exercise 5.2 (Solution on page 427)

&

'
(

5.2 Proof Strategies for Implication

)

"

* +

,

,

-

Proof Strategies for Implication 135

' $

&

%

Example 5.2

! "

!
#

$
%
%
&

'
' % %
#

$
( %
Proof:
% %
% %
) % ' %

%

*

136 Proof Strategies

Example 5.3

Proof:

Exercise 5.3 (Solution on page 427)

!

' $

&
%

Example 5.4

"# $

%

Proof: & %

%

Proof Strategies for Implication 137

modus ponens

' $

&
%

modus tollens

' $

&
%

!

" ## $! % & ''(
138 Proof Strategies

Example 5.5

Proof:

Exercise 5.5 (Solution on page 427)

!

" #

5.3 Proof Strategies for Negation

"

$
"

%

$ $

$

$
' $

&

%

" " "
" $ "
&
$ "

Proof Strategies for Negation 139

' $

&

%

proof by
contradiction

reductio ad absurdum

Example 5.6

Proof. !

"

¾
#
" ¾
¾ ¾ " ¾
$ % &
'(
¾

) "

* ¾ " ¾ " %)¾ " +¾ ¾ " ¾

,

&

-
&

&
.. (' -

140 Proof Strategies

Example 5.7

Proof.

½ ¾ ¿
½ ¾ ¿

½

! !

" ! !

!
!
!
! !

!#

Example 5.8

!

$
!
! !

!
%
!
!

&

! '

" ! !

!

' (
!

!)

!
!! (

!
Proof. $

! *
!

!

#

Proof Strategies for Negation 141

A Diﬀerent Proof.

Example 5.9

"

Proof.

¾
#

Exercise 5.9 (Solution on page 427)

"

142 Proof Strategies

Exercise 5.10 (Solution on page 428)

5.4 Proof Strategies for Conjunction and Equivalence

' $

& %

!
"

' $' $

%& %

&

#
$ %

%

&
Example 5.10

Proof Strategies for Conjunction and Equivalence 143

Proof: Ü

Example 5.11

Proof:

' $

%
&

' $' $

&
%&
%
144 Proof Strategies

5.5 Proof Strategies for Disjunction

É Æ

' $' $

È É

&
È É %&
È É %

È É

È
Ê

É
Ê

È É

' $
Ê

È

Ê

&
È É %

Example 5.12

Ò

Ò¾

!
" #
Proof: $ Ò

Proof Strategies for Disjunction 145

¯

¾
¾
¾

¯

¾
¾ ¾ ¾

! "
#
" "

$

"

"

' $
!

&

%

Example 5.13

%

¾

Proof: !

¾ &

'

¾

(

Exercise 5.13 (Solution on page 428)

%

"

146 Proof Strategies

Exercise 5.14 (Solution on page 429)

' $

!

"

&

# %

Example 5.14

" # " #

Proof. $ " # % " # " #
" #
Proof Strategies for Quantiﬁers 147

Example 5.15

¾
Proof.

¾

¾

Exercise 5.15 (Solution on page 429)

! " "

Exercise 5.16 (Solution on page 429)

# ! ¾

$ % & ' ¾
! ( ) *

Exercise 5.17 (Solution on page 430)

+ , -
Fact: "
. $( . ) !
. *
Proof: /

. ) !
. *

0 . ) !
. *
1
"
. $( . ) !
. *

5.6 Proof Strategies for Quantiﬁers

5.6.1 Universal Quantiﬁcation
/ #
, , 2#
3
2
!

, !
/
4 , 2

3

0 , , , !

3
! , 0
, !
148 Proof Strategies

' $

&

%

!
"# $ %
& ' (
)
*
+ #
,-
'

' $

&

%

Example 5.17

. /

Proof. / +

Proof Strategies for Quantiﬁers 149

Example 5.18

Proof.

Exercise 5.18 (Solution on page 430)

5.6.2 Existential Quantiﬁcation

! "
#
$# $

%

& %
%

#

150 Proof Strategies

' $

&
%

!

" #

!
$
%

' $

&
%

Example 5.19

& ' ( )

*( '
Proof. ' *)
( ' ( ( ' +

+
) ' *) )( ' ,
( (
*( ' *)(
* ( ' ,
(
Proof Strategies for Quantiﬁers 151

Æ

!

"#

$

%

% $ $ &

# $ "
'

"

( ) ( ) *

" ( ) "

(
) ( )
+
( ) %

,#
"
%

$

Exercise 5.19 (Solution on page 430)

-
.

( )

/

# 0 ( " "
)

()*
"

"

Example 5.20 A Strange Proof of Existence

Fact:
"

Proof. 1 $ " 2" 34

¾
5
"#

¾
& 6

¾

#
¾ ¾
& 6

#
¾
¾ (¾¾) ¾

152 Proof Strategies

Exercise 5.20 (Solution on page 431)

!"
5.6.3 Uniqueness
#

$

%

&

$

! '

(
)
(

$

Example 5.21

&
(
¾

Proof. *
(
+! ¾

#
( + ! ( ++!! (
¾
¾
¿ ¾
¾

'

$ ( $
+ ! ( $
¾ ¾

( + ! (
¾

Example 5.22

,

&

!

)

Proof. *
(

Additional Exercises 153

Ë

Ë

Exercise 5.22 (Solution on page 431)

5.7 Additional Exercises

!" Ê #
$

%!

&
$

&
"
"
&&

' %!

' $ &&

! " &&
(

! !"

)
'
* &

! !"
"
! !"

+ %!

¾
,

- & ! "

. ) *
/

$ (
.
0 " #

"
154 Proof Strategies

É È
È É È Ê É Ê
È É È Ê É Ê

Ü È Ü É Ü Ü È Ü Ü ÉÜ

Ü È Ü É Ü Ü È Ü Ü ÉÜ
Ü È Ü É Ü Ü È Ü Ü ÉÜ
Ü È Ü É Ü Ü È Ü Ü ÉÜ
Ü È Ü

Chapter 6

Functions

! "

6.1 Basic Deﬁnitions

' function

!

(

"

)

+ "

( ,-

Example 6.1

.

"

/
-//"

F. Moller, G. Struth, Modelling Computing Systems,

¯
¯ ¯
¯ ¯

¯ ¯

! "

# $% # " &# $
' " ( )* ++
, - " .

/0 # #

Class 1 # ' , #

( - ! &# )* .
#

Marks 1 + % 2 " ++

score Class Marks

##0 30 score ( 1 4 # score #
( # 0 # 0 score (

5 #

6
5 # 30

score ' 1 score ! 1 "

/0 * * *

5 #
0 * # ## *
7 * # 7

Basic Deﬁnitions 157

domain
codomain argument
value
½ ¾
arity

binary function

inﬁx
!

" # " $ #" " $

% range range

range

&
image

% !
range
&
½

preimage

½
'

(

Example 6.2

) " * +

) " *

%
) " *

) %

" %

*
) " ) *

½

) *
½
) *
158 Functions

Exercise 6.2 (Solution on page 431)

score

!

" #

Example 6.3

$

"

%

&

id ' "

' id () *

' ¬Ò ( )

' *

(&
% %

)
+ % " ,
!

"

- .#
!
'
"

/ '

( )

*

Exercise 6.3 (Solution on page 432)

" "

Humans
,
! "%

( )

()

- ()

0
()

Example 6.4

,
! "
%
%% # %

,
! ' Ê Ê %
Basic Deﬁnitions 159

Ê Ê

! ! "# ! ¿ $
!

¿

%

&
#
# '

'
(

)
"# " *!(

!
+
graph
( graph (

( #
*# graph (
!# , *!( score
! -*! (

graphscore , % , . +

/
0
- % /
1 2
/ 3 /
&!
. # 44 $

! % 5

¿ (

graph ¿ Ê
160 Functions

Theorem 6.4

graph graph

Proof:

graph graph !

graph
graph

graph graph
!
graph
graph graph graph

Exercise 6.4 (Solution on page 432)

"# $%&

6.2 One-To-One and Onto Functions

'

(
)

¼ ¼

* #

¿

+ , + ,
-

)

Deﬁnition 6.4

one-to-one 1-1 injective
¼ ¼ ¼

¼
¼
¼

!

!
One-To-One and Onto Functions 161

¼
¼
¼

2013 Book ModellingComputingSystems PDF

Uploaded by

2013 Book ModellingComputingSystems PDF

Uploaded by

Undergraduate Topics in Computer Science

For further volumes:

Mathematics for Computer Science

ISSN 1863-7310 Undergraduate Topics in Computer Science

Library of Congress Control Number: 2013943907

© Springer-Verlag London 2013

Printed on acid-free paper

Springer is part of Springer Science+Business Media (www.springer.com)

Part I: Mathematics for Computer Science 15

3 Boolean Algebras and Circuits 87

4 Predicate Logic 109

5 Proof Strategies 131

8 Inductive and Recursive Deﬁnitions 201

9 Proofs by Induction 223

10 Games and Strategies 251

Part II: Modelling Computing Systems 277

11 Modelling Processes 279

12 Distinguishing Between Processes 309

13 Logical Properties of Processes 333

14 Concurrent Processes 357

15 Temporal Properties 381

  .  ' 4

Solutions to Exercises 405

  !  " # $

  %&  '   

 &  4 & 50 # 6

6            +1

 !           HML 

$   %    

# "        )( ) ) 

          

            

               

                 

            !   "

     !    "

       %&   %&    ' 

         (      

       

)              * 

     +        ( 

    *      $   $   - 

                

%  

 $             

               $  

      

'               

              / 

   $  #   '        

         

    

#              

 Speciﬁcation              

 Implementation Synthesis        

 Veriﬁcation              

             "  #  

     

      

  &  

     ) 

 -    

      

  

             

   

      

     %        

           

F. Moller, G. Struth, Modelling Computing Systems,

 

           

   

  !

"   

          $ 

. ' 4

! " # $

%& '

& 4 & 50 # 6

6 +1

! HML

$ %

# " )())

! "

! "

%& %& '

(

) *

+ (

* $ $ -

%

$

$

'

/

$ # '

#

Speciﬁcation

Implementation Synthesis

Veriﬁcation

" #

&

)

-

%

!

"

$

:

! &" " '

&

&

.

% ( %( % ( %(

!

)

/

! " #

# " $ " $

% &

%! & ! "#

. ! *

% " "

"

" " 1%

%% %% "

( " $

! " . % "

% " "

#

% Either this man is dead or my watch has stopped.

" statements propositions

*

# +

% This man is dead.

$ " deduction inference

#

() , . () , . ( ) , . ( ) ,. (

Dead ( ) Dead (

# 9 : 3

Dead

& '