CS代考 KRR Lectures — Contents

KRR Lectures — Contents
1. Introduction to the KRR MSc Course ⇒
2. Introduction to KRR ⇒
3. Fundamentals of Classical Logic I ⇒
4. Fundamentals of Classical Logic II ⇒
5. Fundamentals of Classical Logic III ⇒
6. Fundamentals of Classical Logic IV ⇒
7. The Winograd Schema Challenge ⇒
8. Representing Time and Change ⇒
9. Prolog ⇒
10. Spatial Reasoning ⇒
11. Modes of Inference ⇒
12. Multi-Valued and Fuzzy Logics ⇒
13. Non-Monotonic Reasoning ⇒
14. Description Logic ⇒

15. Propositional Resolution ⇒
16. First-Order Resolution ⇒
17. Compositional Reasoning ⇒
18. Uncertainty ⇒
19. Vagueness ⇒
20. Ontology and Ontologies ⇒

Knowledge Representation
Lecture KRR-1
Introduction to the Knowledge Represenation and Reasoning Masters Course
KR∧R— Introductiontothe KnowledgeRepresenationandReasoningMastersCourse ⟨Contents⟩ KRR-1-1

Course Elements
• The course will cover the field of knowledge representation by giving a high-level overview of key aims and issues.
KR∧R— Introductiontothe KnowledgeRepresenationandReasoningMastersCourse ⟨Contents⟩ KRR-1-2

Course Elements
• The course will cover the field of knowledge representation by giving a high-level overview of key aims and issues.
• Motivation and philosophical issues will be considered.
• Fundamental principles of logical analysis will be presented
(concisely).
• Several important representational formalisms will be examined. Their motivation and capabilities will be explored.
KR∧R— Introductiontothe KnowledgeRepresenationandReasoningMastersCourse ⟨Contents⟩ KRR-1-2

Course Elements
• The course will cover the field of knowledge representation by giving a high-level overview of key aims and issues.
• Motivation and philosophical issues will be considered.
• Fundamental principles of logical analysis will be presented
(concisely).
• Several important representational formalisms will be examined. Their motivation and capabilities will be explored.
• The potential practicality of KR methods will be illustrated by examining some examples of implemented systems.
KR∧R— Introductiontothe KnowledgeRepresenationandReasoningMastersCourse ⟨Contents⟩ KRR-1-2

Information and Learning
Course materials will be available from the module pages on Minerva and also at teaching.bb-ai.net/KRR.html.
KR∧R— Introductiontothe KnowledgeRepresenationandReasoningMastersCourse ⟨Contents⟩ KRR-1-3

Information and Learning
Course materials will be available from the module pages on Minerva and also at teaching.bb-ai.net/KRR.html.
There is no set text book for this course, but certain parts of the following provide very useful supporting material:
. and Norvig P. Artificial Intelligence, A Modern Approach, 3rd Edition (especially chapters 7–12).
Brachman RJ and J, Knowledge Representation and Reasoning, 2004
and Mackworth A, Artificial intelligence: foundations of computational agents,
There is an html version of this last title at
http://artint.info/html/ArtInt.html
KR∧R— Introductiontothe KnowledgeRepresenationandReasoningMastersCourse ⟨Contents⟩ KRR-1-3

Major Course Topics
• Classical Logic and Proof Systems.
• Automated Reasoning.
• Programming in Prolog.
• Representing and reasoning about time and change.
• Space and physical objects.
• Specialised AI representations: situation calculus, non- monotonic logic, description logic, fuzzy logic.
• Ontology and AI Knowledge Bases.
KR∧R— Introductiontothe KnowledgeRepresenationandReasoningMastersCourse ⟨Contents⟩ KRR-1-4

Coursework
The module will have four assessed pieces of work:
1. solution of problems by representing in logic and using an
automated theorem prover (Prover9)
2. implementation of knowledge-based inference capabilities
(using Prolog) (pairs work)
3. an online test consisting of short problems based on all the
different reasoning systems covered in the module.
KR∧R— Introductiontothe KnowledgeRepresenationandReasoningMastersCourse ⟨Contents⟩ KRR-1-5

Relation to
Basic Logical Background
A large amount of material is available in the form of slides and exercises.
We shall recap this but not revisit every detail.
We shall look at the application of KRR techniques in more general problem settings; and will often see that several represen- tational formalisms and reasoning mechanisms need to be combined.
KR∧R— Introductiontothe KnowledgeRepresenationandReasoningMastersCourse ⟨Contents⟩ KRR-1-6

Knowledge Representation
Lecture KRR-2
Introduction to Knowledge Represenation and Reasoning
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-1

AI and the KR Paradigm
The methodology of Knowledge Representation and Automated Reasoning is one of the major strands of AI research.
It employs symbolic representation of information together with logical inference procedures as a means for solving problems.
Although implementation and deployment of KRR techniques is very challenging, it has given rise to ideas and techniques that are used in a wide range of applications.
Most of the earliest investigations into AI adopted this approach and it is still going strong.
(It is sometimes called GOFAI — good old-fashioned AI.)
However, it is not the only (and perhaps not the most fashionable) approach to AI.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-2

Neural Nets
One methodology for research in AI is to study the structure and function of the brain and try to recreate or simulate it.
How is intelligence dependent on its physical incarnation? KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-3

Situated and Reactive AI
Another approach is to tackle AI problems by observing and seeking to simulate intelligent behaviour by modelling the way in which an intelligent agent reacts to its environment.
A popular methodology is to look first at simple organisms, such as insects, as a first step towards understanding more high-level intelligence.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-4

KRR vs ML
The view of AI taken in KRR is often considered to be opposed to
that of Machine Learning.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-5

KRR vs ML
The view of AI taken in KRR is often considered to be opposed to
that of Machine Learning. This is partly true.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-5

KRR vs ML
The view of AI taken in KRR is often considered to be opposed to
that of Machine Learning. This is partly true.
ML automatically creates models from data, that contain knowledge in an implicit form.
KRR typically uses hand-crafted models that store knowledge in an explicit way.
ML is primarily concerned with classification. KRR is primarily concerned with inference.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-5

KRR vs ML
The view of AI taken in KRR is often considered to be opposed to
that of Machine Learning. This is partly true.
ML automatically creates models from data, that contain knowledge in an implicit form.
KRR typically uses hand-crafted models that store knowledge in an explicit way.
ML is primarily concerned with classification. KRR is primarily concerned with inference.
Capabilities of ML systems are limited by the data upon which they are trained.
KRR can work in completely novel situations.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-5

Intelligence via Language
The KR paradigm takes language as an essential vehicle for
intelligence.
Animals can be seen as semi-intelligent because they only posses a rudimentary form of language.
The principle role of language is to represent information.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-6

Language and Representation
Written language seems to have its origins in pictorial representations.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-7

Language and Representation
Written language seems to have its origins in pictorial representations.
However, it evolved into a much more abstract representation.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning
⟨Contents⟩
KRR-2-7

Language and Logic
• Pattersofnaturallanguageinferenceareusedasaguidetothe form of valid principles of logical deduction.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-8

Language and Logic
• Pattersofnaturallanguageinferenceareusedasaguidetothe form of valid principles of logical deduction.
• Logical representations clean up natural language and aim to make it more definite.
For example:
If it is raining, I shall stay in. It is raining.
Therefore, I shall stay in.
R→S R
∴S
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning
⟨Contents⟩
KRR-2-8

Formalisation and Abstraction
In employing a formal logical representation we aim to abstract from irrelevant details of natural descriptions to arrive at the essential structure of reasoning.
Typically we even ignore much of the logical structure present in natural language because we are only interested in (or only know how to handle) certain modes of reasoning.
For example, for many purposes we can ignore the tense structure of natural language.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-9

Formal and Informal Reasoning
The relationship between formal and informal modes of reasoning might be pictured as follows:
Reasoning in natural language can be regarded as semi-formal.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-10

What do we represent?
• Ourproblem.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-11

What do we represent?
• Ourproblem.
• What would count as a solution.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-11

What do we represent?
• Ourproblem.
• What would count as a solution. • Facts about the world.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-11

What do we represent?
• Ourproblem.
• What would count as a solution.
• Facts about the world.
• Logical properties of abstract concepts (i.e. how they can take part in inferences).
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning
⟨Contents⟩
KRR-2-11

What do we represent?
• Ourproblem.
• What would count as a solution.
• Facts about the world.
• Logical properties of abstract concepts (i.e. how they can take part in inferences).
• Rules of inference.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning
⟨Contents⟩
KRR-2-11

Finding a “Good” Representation
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-12

Finding a “Good” Representation
• Wemustdeterminewhatknowledgeisrelevanttotheproblem.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-12

Finding a “Good” Representation
• Wemustdeterminewhatknowledgeisrelevanttotheproblem. • We need to find a suitable level of abstraction.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-12

Finding a “Good” Representation
• Wemustdeterminewhatknowledgeisrelevanttotheproblem.
• We need to find a suitable level of abstraction.
• Need a representation language in which problem and solution can be adequately expressed.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-12

Finding a “Good” Representation
• Wemustdeterminewhatknowledgeisrelevanttotheproblem.
• We need to find a suitable level of abstraction.
• Need a representation language in which problem and solution can be adequately expressed.
• Need a correct formalisation of problem and solution in that language.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-12

Finding a “Good” Representation
• Wemustdeterminewhatknowledgeisrelevanttotheproblem.
• We need to find a suitable level of abstraction.
• Need a representation language in which problem and solution can be adequately expressed.
• Need a correct formalisation of problem and solution in that language.
• We need a logical theory of the modes of reasoning required to solve the problem.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-12

Inference and Computation
A tough issue that any AI reasoning system must confront is that of Tractability.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-13

Inference and Computation
A tough issue that any AI reasoning system must confront is that of Tractability.
A problem domain is intractable if it is not possible for a (conventional) computer program to solve it in ‘reasonable’ time (and with ‘reasonable’ use of other resources such as memory).
Certain classes of logical problem are not only intractable but also undecidable.
This means that there is no program that, given any instance of the problem, will in finite time either: a) find a solution; or b) terminate having determined that no solution exists.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-13

Inference and Computation
A tough issue that any AI reasoning system must confront is that of Tractability.
A problem domain is intractable if it is not possible for a (conventional) computer program to solve it in ‘reasonable’ time (and with ‘reasonable’ use of other resources such as memory).
Certain classes of logical problem are not only intractable but also undecidable.
This means that there is no program that, given any instance of the problem, will in finite time either: a) find a solution; or b) terminate having determined that no solution exists.
Later in the course we shall make these concepts more precise. KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-13

Time and Change
1+1=2 Standard, classical logic was developed 1+1=2 primarily for applications to mathematics.
Since mathematical truths are eternal, it is not geared towards representing temporal information.
However, time and change play an essential role in many AI problem domains. Hence, formalisms for temporal reasoning abound in the AI literature.
We shall study several of these and the difficulties that obstruct any simple approach (in particular the famous Frame Problem).
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-14

Spatial Information
Knowledge of spatial properties and relationships is required for many commonsense reasoning problems.
While mathematical models exist they are not always well-suited for AI problem domains.
We shall look at some ways of representing qualitative spatial information.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-15

Describing and Classifying Objects
To solve simple commonsense problems we often need detailed knowledge about everyday objects.
Can we precisely specify the properties of type of object such as a cup?
Which properties are essential?
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-16

Combining Space and Time
For many purposes we would like to be able to reason with knowledge involving both spatial and temporal information.
For example we may want to reason about the working of some physical mechanism:
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-17

Robotic Control
An important application for spatio-temporal reasoning is robot control.
Many AI techniques (as well as a great deal of engineering technology) have been applied to this domain.
While success has been achieved for some constrained envioronments, flexible solutions are elusive.
Versatile high-level control of autonomous agents is a major goal of KR.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-18

Uncertainty
Much of the information available to an intelligent (human or computer) is affected by some degree of uncertainty.
This can arise from: unreliable information sources, inaccurate measurements, out of date information, unsound (but perhaps potentially useful) deductions.
This is a big problem for AI and has attracted much attention. Popular approaches include probabalistic and fuzzy logics.
But ordinary classical logics can mitigate the problem by use of generality. E.g. instead of prob(φ) = 0.7, we might assert a more general claim φ ∨ ψ.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-19

Ontology
Literally Ontology means the study of what exists.
It is studied in philosophy as a branch of Metaphysics.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-20

Ontology
Literally Ontology means the study of what exists.
It is studied in philosophy as a branch of Metaphysics.
In KR the term Ontology is used to refer to a rigorous logical specification of a domain of objects and the concepts and relationships that apply to that domain.
Ontologies are intended to guarantee the coherence of information and to allow relyable exchange of information between computer systems.
Use of ontologies is one of the main ways in which KRR techniques are exploited in modern software applications.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-20

Issues of Ambiguity and Vagueness
A huge problem that obstructs the construction of rigorous ontologies is the widespread presence of ambiguity and vagueness in natural concepts.
For example: tall, good, red, cup, mountain.
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-21

Issues of Ambiguity and Vagueness
A huge problem that obstructs the construction of rigorous ontologies is the widespread presence of ambiguity and vagueness in natural concepts.
For example: tall, good, red, cup, mountain.
How many grains make a heap?
KR∧R— IntroductiontoKnowledgeRepresenationandReasoning ⟨Contents⟩ KRR-2-21

Knowledge Representation
Lecture KRR-3
Classical Logic I: Concepts and Uses of Logic
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic ⟨Contents⟩ KRR-3-1

Lecture Plan
• Formal Analysis of Inference • Propositional Logic
• Validity
• Quantification
• Uses of Logic
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic
⟨Contents⟩
KRR-3-2

Logical Form
A form of an object is a structure or pattern which it exhibits.
A logical form of a linguistic expression is an aspect of its structure
which is relevant to its behaviour with respect to inference.
To illustrate this we consider a mode of inference which has been recognised since ancient times.
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic ⟨Contents⟩ KRR-3-3

Logical Form of an Argument
If Leeds is in Yorkshire then Leeds is in the UK Leeds is in Yorkshire
Therefore, Leeds is in the UK
If P then Q P → Q
PP ∴QQ
(The Romans called this type of inference modus ponendo ponens.)
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic ⟨Contents⟩ KRR-3-4

Propositions
The preceding argument can be explained in terms of propositional logic.
A proposition is an expression of a fact.
The symbols, P and Q, represent propositions and the logical symbol ‘ → ’ is called a propositional connective.
Many systems of propositional logic have been developed. In this lecture we are studying classical — i.e. the best established — propositional logic.
In classical propositional logic it is taken as a principle that:
Every proposition is either true or false and not both. KR∧R— ClassicalLogicI:ConceptsandUsesofLogic ⟨Contents⟩ KRR-3-5

Complex Propositions and Connectives
Propositional logic deals with inferences governed by the meanings of propositional connectives. These are expressions which operate on one or more propositions to produce another more complex proposition.
The connectives dealt with in standard propositional logic correspond to the natural language constructs:
• ‘… and …’,
• ‘. . . or . . .’
• ‘it is not the case that. . .’ • ‘if … then …’.
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic
⟨Contents⟩
KRR-3-6

Symbols for the Connectives
The propositional connectives are represented by the following symbols:
and ∧ or ∨
(P ∧ Q)
(P ∨ Q) (P →Q)
((P ∧Q)∨R), (¬P →¬(Q∨R))
Brackets prevent ambiguity which would otherwise occur in a
formula such as ‘P ∧ Q ∨ R’.
More complex examples:
if…then →
not ¬ ¬P
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic ⟨Contents⟩ KRR-3-7

Propositional Formulae
We can precisely specify the well-formed formulae of propositional logic by the following (recursive) characterisation:
• Each of a set, P, of propositional constants Pi is a formula. • Ifαisaformulasois¬α.
• Ifαandβareformulaesois(α∧β).
• Ifαandβareformulaesois(α∨β).
The propositional connectives ¬, ∧ and ∨ are respectively called negation, conjunction and disjunction.
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic ⟨Contents⟩ KRR-3-8

Proposition Symbols and Schematic Variables
The symbols P , Q etc. occurring in propositional formulae should be understood as abbreviations for actual propositions such as ‘It is Tuesday’ and ‘I am bored’.
In defining the class of propositional formulae I used Greek letters (α and β) to stand for arbitrary propositional formulae. These are called schematic variables.
Schematic variables are used to refer classes of expression sharing a common form. Thus they can be used for describing patterns of inference.
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic ⟨Contents⟩ KRR-3-9

Inference Rules
An inference rule characterises a pattern of valid deduction.
In other words, it tells us that if we accept as true a number of propositions — called premisses — which match certain patterns, we can deduce that some further proposition is true — this is called the conclusion.
Thus we saw that from two propositions with the forms α → β and α we can deduce β.
The inference from P → Q and P to Q is of this form.
An inference rule can be regarded as a special type of re-write rule: one that preserves the truth of formulae — i.e. if the premisses are true so is the conclusion.
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic ⟨Contents⟩ KRR-3-10

More Simple Examples
‘And’ Elimination ‘And’ Introduction
α∧βαβ αβα∧β
α∧β
‘Or’ Introduction
αα
α∨β β∨α α
‘Not’ Elimination
¬¬α
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic
⟨Contents⟩
KRR-3-11

Logical Arguments and Proofs
A logical argument consists of a set of propositions {P1, . . . , Pn} called premisses and a further proposition C, the conclusion.
Notice that in speaking of an argument we are not concerned with any sequence of inferences by which the conclusion is shown to follow from the premisses. Such a sequence is called a proof.
A set of inference rules constitutes a proof system.
Inference rules specify a class of primitive arguments which are justified by a single inference rule. All other arguments require proof by a series of inference steps.
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic ⟨Contents⟩ KRR-3-12

A 2-Step Proof
Suppose we know that ‘If it is Tuesday or it is raining John stays in bed all day’ then if we also know that ‘It is Tuesday’ we can conclude that ‘John is in Bed’.
Using T, R and B to stand for the propositions involved, this conclusion could be proved in propositional logic as follows:
T ((T ∨R)→B) (T ∨R)
B
Here we have used the ‘or introduction’ rule followed by good old modus ponens.
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic ⟨Contents⟩ KRR-3-13

Provability
To assert that C can be proved from premisses {P1, . . . , Pn} in a proof system S we write:
P1,…,Pn ⊢S C
This means that C can be derived from the formulae {P1, . . . , Pn}
by a series of inference rules in the proof system S.
When it is clear what system is being used we may omit the
subscript S on the ‘⊢’ symbol.
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic ⟨Contents⟩ KRR-3-14

Validity
An argument is called valid if its conclusion is a consequence of its premisses. Otherwise it is invalid. This needs to be made more precise:
One definition of validity is: An argument is valid if it is not possible for its premisses to be true and its conclusion is false.
Another is: in all possible circumstances in which the premisses are true, the conclusion is also true.
To assert that the argument from premisses {P1,…,Pn} to conclusion C is valid we write:
P1,…,Pn |= C
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic ⟨Contents⟩ KRR-3-15

Provability vs Validity
We have defined provability as a property of an argument which
depends on the inference rules of a logical proof system.
Validity on the other hand is defined by appealing directly to the meanings of formulae and to the circumstances in which they are true or false.
In the next lecture we shall look in more detail at the relationship between validity and provability. This relationship is of central importance in the study of logic.
To characterise validity we shall need some precise specification of the ‘meanings’ of logical formulae. Such a specification is called a formal semantics.
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic ⟨Contents⟩ KRR-3-16

Relations
In propositional logic the smallest meaningful expression that can be represented is the proposition. However, even atomic propositions (those not involving any propositional connectives) have internal logical structure.
In predicate logic atomic propositions are analysed as consisting of a number of individual constants (i.e. names of objects) and a predicate, which expresses a relation between the objects.
R(a, b, c) Loves(john, mary)
With many binary (2-place) relations the relation symbol is often
written between its operands — e.g. 4 > 3.
Unary (1-place) relations are also called properties — Tall(tom).
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic ⟨Contents⟩ KRR-3-17

Universal Quantification
Useful information often takes the form of statements of general property of entities. For instance, we may know that ‘every dog is a mammal’. Such facts are represented in predicate logic by means of universal quantification.
Given a complex formula such as (Dog(spot) → Mammal(spot)), if we remove one or more instances of some individual constant we obtain an incomplete expression (Dog(. . .) → Mammal(. . .)), which represents a (complex) property.
To assert that this property holds of all entities we write:
∀x[Dog(x) → Mammal(x)]
in which ‘∀’ is the universal quantifier symbol and x is a variable
indicating which property is being quantified.
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic ⟨Contents⟩ KRR-3-18

An Argument Involving Quantification
An argument such as:
Everything in Yorkshire is in the UK Leeds is in Yorkshire
Therefore Leeds is in the UK
can now be represented as follows:
∀x[Inys(x) → Inuk(x)] Inys(l)
Inuk(l)
Later we shall examine quantification in more detail. KR∧R— ClassicalLogicI:ConceptsandUsesofLogic
⟨Contents⟩
KRR-3-19

Uses of Logic
Logic has always been important in philosophy and in the foundations of mathematics and science. Here logic plays a foundational role: it can be used to check consistency and other basic properties of precisely formulated theories.
In computer science, logic can also play this role — it can be used to establish general principles of computation; but it can also play a rather different role as a ‘component’ of computer software: computers can be programmed to carry out logical deductions. Such programs are called Automated Reasoning systems.
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic ⟨Contents⟩ KRR-3-20

Formal Specification
of Hardware and Software
Since logical languages provide a flexible but very precise means of description, they can be used as specification language for computer hardware and software.
A number of tools have been developed which help developers go from a formal specification of a system to an implementation.
However, it must be realised that although a system may completely satisfy a formal specification it may still not behave as intended — there may be errors in the formal specification.
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic ⟨Contents⟩ KRR-3-21

Formal Verification
As well as being used for specifying hardware or software systems, descriptions can be used to verify properties of systems.
If Θ is a set of formulae describing a computer system and π is a formula expressing a property of the system that we wish to ensure (eg. π might be the formula ∀x[Employee(x) → age(x) > 0]), then we must verify that:
Θ |= π
We can do this using a proof system S if we can show that:
Θ⊢S π
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic ⟨Contents⟩ KRR-3-22

Logical Databases
A set of logical formulae can be regarded as a database.
A logical database can be queried in a very flexible way, since for any formula φ, the semantics of the logic precisely specify the conditions under which φ is a consequence of the formulae in the database.
Often we may not only want to know whether a proposition is true but to find all those entities for which a particular formula
containing variables holds. e.g.
query: Located(x, y) ∧ Furniture(x) ?
Ans: ⟨x = sofa1, y = lounge ⟩, ⟨x = table1, y = kitchen ⟩, …
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic ⟨Contents⟩ KRR-3-23

Logic and Intelligence
The ability to reason and draw consequences from diverse information may be regarded as fundamental to intelligence.
As the principal intention in constructing a logical language is to precisely specify correct modes of reasoning, a logical system (i.e. a logical language plus some proof system) might in itself be regarded as a form of Artificial Intelligence.
However, as we shall see as this course progresses, there are many obstacles that stand in the way of achieving an ‘intelligent’ reasoning system based on logic.
KR∧R— ClassicalLogicI:ConceptsandUsesofLogic ⟨Contents⟩ KRR-3-24

Knowledge Representation
Lecture KRR-4
Classical Logic II:
Formal Systems, Proofs and Semantics
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-1

Sequents
A sequent is an expression of the form:
α1, …, αm ⇒ β1, …, βn (where the αs and βs are logical formulae).
This asserts that:
If all of the αs are true then at least one of the βs is true. Hence, it means the same as:
(α1∧…∧αm) → (β1∨…∨βn)
This notation — as we shall soon see — is very useful in
presenting inference rules in a concise and uniform way.
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-2

Notation Issues
Many articles and textbooks write sequents using the notation:
α1, …, αm ⊢ β1, …, βn
instead of α1, …, αm ⇒ β1, …, βn.
(I used that notation in previous versions of my slides and notes.)
However, I believe this is confusing because the ⊢ symbol normally means provability. Indeed, some authors do talk about the ‘⊢‘ in a sequent as though it refers to a provability relation. But this is wrong: it functions as a special kind of connective.
The sequent calculus was orignated by , who used ‘ → ‘ in his sequents (and used ‘⊃ for the implication symbol).
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-3

Special forms of sequent
A sequent with an empty left-hand side:
⇒ β1, …, βn
asserts that at least one of the βs must be true without assuming
any premisses to be true.
If the simple sequent ⇒ β is valid, then β is called a
logical theorem.
A sequent with an empty right-hand side: α1, . . . , αm⇒ asserts that the set of premisses {α1, . . . , αm} is inconsistent.
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-4

Sequent Calculus Inference Rules
A sequent calculus inference rule specifies a pattern of reasoning in terms of sequents rather than formulae.
Eg. a sequent calculus ‘and introduction’ is specified by:
Γ⇒α, ∆ and Γ⇒β, ∆[⇒ ∧] Γ⇒(α∧β), ∆
where Γ and ∆ are any series of formulae.
In a sequent calculus we also have rules which introduce symbols
into the premisses:
α,β,Γ⇒∆ [∧⇒] (α ∧ β), Γ ⇒ ∆
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-5

Ordering Does Not Matter
The applicability of a rule to a formula depends on which side of the ⇒ it occurs on.
But the ordering of formulae on the same side does not matter.
Thus each rule can apply to either any formula on the left or any formula on the right.
Hence, sequent calculus rules normally come in pairs, with one being applicable to a certain kind of formula occurring on the left (e.g. [⇒ ∧ ]) and the other applicable when that kind of formula occurs on the right (e.g. [ ∧ ⇒ ]).
(We shall see this in the proof system that will be presented shortly. )
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-6

Sequent Calculus Proof Systems
To assert that a sequent is provable in a sequent calculus system, SC, I shall write:
α1, …, αm⇒ β1, …, βn
SC
Construing a proof system in terms of the provability of sequents allows for much more uniform presentation than can be given in terms of provability of conclusions from premisses.
We start by stipulating that all sequents of the form
α, Γ ⇒ α, ∆ are immediately provable.
We then specify how each logical symbol can be introduced into the left and right sides of a sequent (see next slide).
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-7

A Propositional Sequent Calculus
Rules:
Axiom
α,Γ⇒ α,∆
α, β, Γ ⇒ ∆ [∧⇒] Γ⇒α,∆ and Γ⇒β,∆[⇒∧]
(α∧β), Γ⇒ ∆
α,Γ⇒∆ and β,Γ⇒∆[∨⇒]
(α∨β), Γ⇒ ∆ Γ⇒ α, ∆ [¬⇒]
¬α, Γ ⇒ ∆
Γ⇒(α∧β), ∆ Γ⇒α,β,∆ [⇒∨]
Γ⇒ (α∨β), ∆
Γ, α⇒ ∆ [⇒¬]
Γ ⇒ ¬α, ∆
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics
⟨Contents⟩
KRR-4-8

Re-Write Rules
Re-write rules, are an easy way to specify transformations of a formula (on either side of a sequent) to an equivalent formula.
We shall write: α → β =⇒ ¬α ∨ β [ → r.w] as a short specification for the rules:
¬α∨β, Γ⇒ ∆[→r.w.] Γ⇒ ¬α∨β, ∆[→r.w.] α→β, Γ⇒ ∆ Γ⇒ α→β, ∆
Exercises:
1. Showthattherules[∨⇒]and[⇒ ∨]canbereplacedbythe rewriteruleα∨β =⇒ ¬(¬α∧¬β)
2. Specify rules for [ → ⇒ ] and [⇒ → ] that directly eliminate the → connective without replacing it by an equivalent form.
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-9

Sequent Calculus Proofs
The beauty of the sequent calculus system is its reversibility.
To test whether a sequent, Γ⇒ ∆, is provable we simply apply the symbol introduction rules backwards. Each time we apply a rule, one connective is eliminated. With some rules two sequents then have to be proved (the proof branches) but eventually every branch will terminate in a sequent containing only atomic propositions. If all these final sequents are axioms, then Γ⇒ ∆ is proved, otherwise it is not provable.
Note that the propositional sequent calculus rules can be applied in any order.
This calculus is easy to implement in a computer program. KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-10

Proof Example 1
(P → Q), P ⇒ Q
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-11

Proof Example 2
¬(P ∧¬Q)⇒ (P →Q)
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-12

Proof Example 3
((P ∨Q)∨R), (¬P ∨S), ¬(Q∧¬S)⇒(R∨S)
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-13

Formal Semantics
We have seen that a notion of validity can be defined independently of the notion of provability:
An argument is valid if it is not possible for its premisses to be true and its conclusion is false.
We could make this precise if we could somehow specify the conditions under which a logical formulae is true.
Such a specification is called a formal semantics or an interpretation for a logical language.
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-14

Interpretation of
Propositional Calculus
To specify a formal semantics for propositional calculus we take literally the idea that ‘a proposition is either true or false’.
We say that the semantic value of every propositional formula is one of the two values T or F — called truth-values.
For the atomic propositions this value will depend on the particular fact that the proposition asserts and whether this is true. Since propositional logic does not further analyse atomic propositions we must simply assume there is some way of determining the truth values of these propositions.
The connectives are then interpreted as truth-functions which completely determine the truth-values of complex propositions in terms of the values of their atomic constituents.
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-15

Truth-Tables
The truth-functions corresponding to the propositional connectives ¬, ∧ and ∨ can be defined by the following tables:
α
β
(α∧β)
F
F
F
F
T
F
T
F
F
T
T
T
α
β
(α∨β)
F
F
F
F
T
T
T
F
T
T
T
T
α
¬α
F
T
T
F
These give the truth-value of the complex proposition formed by the connective for all possible truth-values of the component propositions.
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-16

The Truth-Function for ‘→’
The truth-function for ‘ → ’ is defined so that a formulae (α → β)
is always true except when α is true and β is false:
α
β
(α → β)
F
F
T
F
T
T
T
F
F
T
T
T
So the statement ‘If logic is interesting then pigs can fly’ is true if either ‘Logic is interesting’ is false or ‘Pigs can fly is true’.
Thus a formula (α → β) is truth-functionally equivalent to (¬α ∨ β).
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-17

Propositional Models
A propositional model for a propositional calculus in which the propositions are denoted by the symbols P1, . . . , Pn, is a specification assigning a truth-value to each of these proposition symbols. It might by represented by, e.g.:
{⟨P1 = T⟩,⟨P2 = F⟩,⟨P3 = F⟩,⟨P4 = T⟩,…}
Such a model determines the truth of all propositions built up from the atomic propositions P1, . . . , Pn. (The truth-value of the atoms is given directly and the values of complex formulae are determined by the truth-functions.)
If a model, M, makes a formula, φ, true then we say that M satisfies φ.
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-18

Validity in terms of Models
Recall that an argument’s being valid means that: in all possible circumstances in which the premisses are true the conclusion is also true.
From the point of view of truth-functional semantics each model represents a possible circumstance — i.e. a possible set of truth values for the atomic propositions.
To assert that an argument is truth-functionally valid we write P1,…,Pn |=TF C
and we define this to mean that ALL models which satisfy ALL of the premisses, P1, . . . , Pn also satisfy the conclusion C.
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-19

Soundness and Completeness
A proof system is complete with respect to a formal semantics if every argument which is valid according to the semantics is also provable using the proof system.
A proof system is sound with respect to a formal semantics if every argument which is provable with the system is also valid according to the semantics.
It can be shown that the system of sequent calculus rules, SC, is both sound and complete with respect to the truth-functional semantics for propositional formulae.
Thus,
(How this can be show is beyond the scope of this course.) KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-20
Γ⇒ C ifandonlyif Γ |=TF C.
SC

More about Quantifiers
We shall now look again at the notation for expressing quantification and what it means.
First suppose, φ(. . .) expresses a property — i.e. it is a predicate logic formulae with (one or more occurrences of) a name removed.
If we want say that something exists which has this property we write:
∃x[φ(x)]
‘∃’ being the existential quantifier symbol.
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-21

Multiple Quantifiers
Consider the sentence: ‘Everybody loves somebody’ We can consider this as being formed from an expression of the form loves(john, mary) by the following stages.
First we remove mary to form the property loves(john, . . .) which we existentially quantify to get: ∃x[ loves(john, x)]
Then by removing john we get the property ∃x[ loves(…,x)] which we quantify universally to end up with:
∀y[ ∃x[loves(y, x)] ]
Notice that each time we introduce a new quantifier we must use a new variable letter so we can tell what property is being quantified.
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-22

Defining ∃ in Terms of ∀
We shall shortly look at sequent rules for handling the universal
quantifier.
Predicate logic formulae will in general contain both universal (∀) and existential (∃) quantifiers. However, in the same way that in propositional logic we saw that (α → β) can be replaced by (¬α ∨ β), the existential quantifier can be eliminated by the following re-write rule.
∃υ[φ(υ)] =⇒ ¬∀υ[¬φ(υ)] These two forms of formula are equivalent in meaning.
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-23

The Sequent Rule for ⇒ ∀ Γ⇒φ(κ),∆ [⇒∀]*
Γ ⇒ ∀υ[φ(υ)], ∆
The * indicates a special condition:
The constant κ must not occur anywhere else in the sequent.
This restriction is needed because if κ occurred in another formulae of the sequent then it could be that φ(κ) is a consequence which can only be proved in the special case of κ.
On the other hand if κ is not mentioned elsewhere it can be regarded as an arbitrary object with no special properties.
If the property φ(…) can be proven true of an arbitrary object it must be true of all objects.
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-24

An example
As an example we now prove that the formula ∀x[P (x) ∨ ¬P (x)] is a theorem of predicate logic. This formula asserts that every object either has or does not have the property P (. . .).
P(a)⇒ P(a) [⇒¬] ⇒P(a),¬P(a) [⇒∨]
⇒ (P(a) ∨ ¬P(a)) [⇒ ∀] ⇒ ∀x[P(x)∨¬P(x)]
Here the (reverse) application of the [⇒ ∀] rule could have been used to introduce not only a but any name, since no names occur on the LHS of the sequent.
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-25

Another Example
Consider the follwing illegal application of [⇒ ∀]: P(b)⇒ P(b)] [⇒∀]†
P(b)⇒ ∀x[P(x)]
† This is an incorrect application of the rule, since b already occurs
on the LHS of the sequent.
(Just because b has the property P (. . .) we cannot conclude that everything has this property.)
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-26

A Sequent Rule for ∀⇒
A formula of the form ∀υ[φ(υ)] clearly entails φ(κ) for any name κ.
Hence the following sequent rule clearly preserves validity:
φ(κ), Γ⇒ ∆ [∀⇒] ∀υ[φ(υ)], Γ ⇒ ∆
But, the formulae φ(κ) makes a much weaker claim than ∀υ[φ(υ)]. This means that this rule is not reversible since, the bottom sequent may be valid but not the top one.
Consider the case:
F(a) ⇒ (F(a) ∧ F(b)) [∀⇒ ] ∀x[F(x)]⇒ (F(a)∧F(b))
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics
⟨Contents⟩ KRR-4-27

A Reversible Version
A quantified formula ∀υ[φ(υ)] has as consequences all formulae of the form φ(κ); and, in proving a sequent involving a universal premiss, we may need to employ many of these instances.
A simple way of allowing this is by using the following rule:
φ(κ), ∀υ[φ(υ)], Γ ⇒ ∆ [∀⇒ ] ∀υ[φ(υ)], Γ ⇒ ∆
When applying this rule backwards to test a sequent we find a universal formulae on the LHS and add some instance of this formula to the LHS.
Note that the universal formula is not removed because we may later need to apply the rule again to add a different instance.
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-28

An Example Needing 2 Instantiations
We can now see how the sequent we considered earlier can be proved by applying the [∀⇒ ] rule twice, to instantiate the same universally quantified property with two different names.
F(a),…⇒F(a) and …,F(b),…⇒F(b) [⇒ ∧] F(a), F(b),∀x[F(x)] ⇒ (F(a) ∧ F(b)) [∀⇒ ] F(a), ∀x[F(x)] ⇒ (F(a) ∧ F(b)) [∀⇒ ]
∀x[F(x)]⇒ (F(a)∧F(b))
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-29

Termination Problem
We now have the problem that the (reverse) application of [∀⇒ ] results in a more complex rather than a simpler sequent.
Furthermore, in any application of [∀⇒ ] we must choose one of (infinitely) many names to instantiate.
Although there are various clever things that we can do to pick instances that are likely to lead to a proof, these problems are fundamentally insurmountable.
This means that unlike with propositional sequent calculus, there is no general purpose automaitc procedure for testing the validity of sequents containing quantified formulae.
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-30

Decision Procedures
A decision procedure for some class of problems is an algorithm which can solve any problem in that class in a finite time (i.e. by means of a finite number of computational steps).
Generally we will be interested in some infinite class of similar problems such as:
1. problems of adding any two integers together
2. problems of solving any polynomial equation
3. problems of testing validity of any propositional logic sequent 4. problems of testing validity of any predicate logic sequent
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-31

Decidability
A class of problems is decidable if there is a decision procedure for that class; otherwise it is undecidable.
Problem classes 1–3 of the previous slide are decidable, whereas class 4 is known to be undecidable.
Undecidability of testing validity of entailments in a logical language is clearly a major problem if the language is to be used in a computer system: a function call to a procedure used to test entailments will not necessarily terminate.
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-32

Semi-Decidability
Despite the fact that predicate logic is undecidable, the rules that we have given for the quantifiers to give us a complete proof system for predicate logic.
Furthermore, it is even possible to devise a strategy for picking instants in applying the [∀⇒ ] rule, such that every valid sequent is provable in finite time.
However, there is no procedure that will demonstrate the invalidity of every invalid sequent in finite time.
A problem class, where we want a result Yes or No for each problem, is called (positively) semi-decidable if every positive case can be verified in finite time but there is no procedure which will refute every negative case in finite time.
KR∧R— ClassicalLogicII:FormalSystems,ProofsandSemantics ⟨Contents⟩ KRR-4-33

Knowledge Representation
Lecture KRR-5
Classical Logic III: Representation in First-Order Logic
KR∧R— RepresentationinFirst-OrderLogic ⟨Contents⟩ KRR-5-1

First-Order Logic
As we have seen First-Order Logic extends Propositional Logic in two ways:
• The meanings of ‘ato

Related Posts