Logic for Computer Science. Lecture Notes
Andrzej Szal-as
College of Economics and Computer Science, Olsztyn, Poland
and
Department of Computer Science, University of Linköping, Sweden
http://www.ida.liu.se/∼andsz
February 2002
, 2
Contents
I Introduction to Logics 7
1 Introduction 9
1.1 Introduction to the Course . . . . . . . . . . . . . . . . . . . . . 9
1.2 Introduction to Logics . . . . . . . . . . . . . . . . . . . . . . . . 10
1.3 Introduction to Proof Systems . . . . . . . . . . . . . . . . . . . . 11
1.4 BNF Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2 Propositional Calculus 17
2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.2 Syntax of Propositional Calculus . . . . . . . . . . . . . . . . . . 17
2.3 Semantics of Propositional Calculus . . . . . . . . . . . . . . . . 18
2.4 The Complexity of Propositional Calculus . . . . . . . . . . . . . 19
2.5 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
3 Predicate Calculus 21
3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
3.2 Syntax of Predicate Calculus . . . . . . . . . . . . . . . . . . . . 21
3.3 Semantics of Predicate Calculus . . . . . . . . . . . . . . . . . . . 23
3.4 The Complexity of Predicate Calculus . . . . . . . . . . . . . . . 25
3.5 Unification of terms . . . . . . . . . . . . . . . . . . . . . . . . . 26
3.6 Skolemization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3.7 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4 Applications of Predicate Calculus 29
4.1 Specifying Data Structures . . . . . . . . . . . . . . . . . . . . . 29
3
,
, 4 CONTENTS
4.2 Predicate Calculus as a Programming Language .................................31
4.3 Predicate Calculus as a Query Language .............................................32
4.4 Exercises ................................................................................................ 33
II Automated Deduction in Classical Logic 35
5 Automated Deduction in Propositional Calculus 37
5.1 Introduction ........................................................................................... 37
5.2 Resolution Method................................................................................. 37
5.3 Sequent Calculus .................................................................................... 39
5.4 Analytic Tableaux.................................................................................. 41
5.5 Exercises ................................................................................................ 44
6 Automated Deduction in Predicate Calculus 45
6.1 Introduction ........................................................................................... 45
6.2 Resolution Method................................................................................. 45
6.3 Sequent Calculus .................................................................................... 47
6.4 Analytic Tableaux.................................................................................. 48
6.5 Exercises ................................................................................................ 49
III Second-Order Logic and its Applications 51
7 Second-Order Logic 53
7.1 Introduction ........................................................................................... 53
7.2 Syntax of Second-Order Logic ............................................................... 53
7.3 Semantics of Second-Order Logic.......................................................... 54
7.4 The Complexity of Second-Order Logic................................................ 54
7.5 Second-Order Logic in Commonsense Reasoning................................. 55
7.6 Exercises ................................................................................................ 57
8 Second-Order Quantifier Elimination 59
8.1 Introduction ........................................................................................... 59
8.2 SCAN Algorithm.................................................................................... 59
Andrzej Szal-as
College of Economics and Computer Science, Olsztyn, Poland
and
Department of Computer Science, University of Linköping, Sweden
http://www.ida.liu.se/∼andsz
February 2002
, 2
Contents
I Introduction to Logics 7
1 Introduction 9
1.1 Introduction to the Course . . . . . . . . . . . . . . . . . . . . . 9
1.2 Introduction to Logics . . . . . . . . . . . . . . . . . . . . . . . . 10
1.3 Introduction to Proof Systems . . . . . . . . . . . . . . . . . . . . 11
1.4 BNF Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2 Propositional Calculus 17
2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.2 Syntax of Propositional Calculus . . . . . . . . . . . . . . . . . . 17
2.3 Semantics of Propositional Calculus . . . . . . . . . . . . . . . . 18
2.4 The Complexity of Propositional Calculus . . . . . . . . . . . . . 19
2.5 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
3 Predicate Calculus 21
3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
3.2 Syntax of Predicate Calculus . . . . . . . . . . . . . . . . . . . . 21
3.3 Semantics of Predicate Calculus . . . . . . . . . . . . . . . . . . . 23
3.4 The Complexity of Predicate Calculus . . . . . . . . . . . . . . . 25
3.5 Unification of terms . . . . . . . . . . . . . . . . . . . . . . . . . 26
3.6 Skolemization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3.7 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4 Applications of Predicate Calculus 29
4.1 Specifying Data Structures . . . . . . . . . . . . . . . . . . . . . 29
3
,
, 4 CONTENTS
4.2 Predicate Calculus as a Programming Language .................................31
4.3 Predicate Calculus as a Query Language .............................................32
4.4 Exercises ................................................................................................ 33
II Automated Deduction in Classical Logic 35
5 Automated Deduction in Propositional Calculus 37
5.1 Introduction ........................................................................................... 37
5.2 Resolution Method................................................................................. 37
5.3 Sequent Calculus .................................................................................... 39
5.4 Analytic Tableaux.................................................................................. 41
5.5 Exercises ................................................................................................ 44
6 Automated Deduction in Predicate Calculus 45
6.1 Introduction ........................................................................................... 45
6.2 Resolution Method................................................................................. 45
6.3 Sequent Calculus .................................................................................... 47
6.4 Analytic Tableaux.................................................................................. 48
6.5 Exercises ................................................................................................ 49
III Second-Order Logic and its Applications 51
7 Second-Order Logic 53
7.1 Introduction ........................................................................................... 53
7.2 Syntax of Second-Order Logic ............................................................... 53
7.3 Semantics of Second-Order Logic.......................................................... 54
7.4 The Complexity of Second-Order Logic................................................ 54
7.5 Second-Order Logic in Commonsense Reasoning................................. 55
7.6 Exercises ................................................................................................ 57
8 Second-Order Quantifier Elimination 59
8.1 Introduction ........................................................................................... 59
8.2 SCAN Algorithm.................................................................................... 59
