程序代写代做 algorithm go flex database game C AI graph html 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. Representing Time and Change
8. Prolog
9. Spatial Reasoning
10. Modes of Inference
11. MultiValued and Fuzzy Logics
12. NonMonotonic Reasoning
13. Description Logic
14. Propositional Resolution

15. FirstOrder Resolution
16. Compositional Reasoning
17. Uncertainty
18. Vagueness
19. Ontology and Ontologies

COMP5450M
Knowledge Representation
Lecture KRR1
Introduction to the Knowledge Represenation and Reasoning Masters Course
KRR Introductiontothe KnowledgeRepresenationandReasoningMastersCourse Contents KRR11

Course Elements
The course will cover the field of knowledge representation by giving a highlevel 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. X
KRR Introductiontothe KnowledgeRepresenationandReasoningMastersCourse Contents KRR12

Information and Learning
Essential information about the course will be available from the VLE website currently being updated.
There is no set text book for this course, but certain parts of the following provide very useful supporting material:
Russell S and Norvig P Artificial Intelligence. A Modern Approach Prentice Hall, third edition 2010 especially chapter 3.
Brachman RJ and Levesque HJ Knowledge Representation and Reasoning Morgan Kaufmann 2004
Poole D and Mackworth A Artificial intelligence : foundations of computational agents Cambridge University Press 2010
There is an html version of this title at http:artint.infohtmlArtInt.html KRR Introductiontothe KnowledgeRepresenationandReasoningMastersCourse Contents KRR13

Major Course Topics
Classical Logic and Inference.
The Problem of Tractability.
Representing and reasoning about time and change.
Space and physical objects.
Ontology and AI Knowledge Bases.
Handling Vagueness and Uncertainty in KRR Systems. Programming in Prolog.
KRR Introductiontothe KnowledgeRepresenationandReasoningMastersCourse Contents KRR14

Coursework
The module will have two pieces of coursework. Each coursework will consist of several parts covering the following topics:
Formalising some example problems and using an automated reasoning program,
Constructing a small Ontology,
implementing some fundamental inference capabilities using
Prolog,
investigating a major challenge for KRR, such as the
Winograd Schema Challenge
KRR Introductiontothe KnowledgeRepresenationandReasoningMastersCourse Contents KRR15

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.
KRR Introductiontothe KnowledgeRepresenationandReasoningMastersCourse Contents KRR16

The Winograd Schema Challenge
This challenge has been proposed as a more welldefined alternative to the famous Turing Test. It brings many problems of AI and KRR more sharply into focus than does the rather open ended Turing Test.
Corpus of Winograd Schema problems by Ernie Davis http:www.cs.nyu.edudavisepapersWS.html
Paper on Winograd Schema problems by Hector Levesque http:commonsensereasoning.org2011papersLevesque. pdf
KRR Introductiontothe KnowledgeRepresenationandReasoningMastersCourse Contents KRR17

Nature of the Challenge
A Winograd schema is a pair of sentences that differ in only one or two words and that contain an ambiguity that is resolved in opposite ways in the two sentences and requires the use of world knowledge and reasoning for its resolution.
The schema takes its name from a wellknown example by Terry Winograd 1972
The city councilmen refused the demonstrators a permit because they fearedadvocated violence.
If the word is feared, then they presumably refers to the city council; if it is advocated then they presumably refers to the demonstrators.
KRR Introductiontothe KnowledgeRepresenationandReasoningMastersCourse Contents KRR18

Requirements for a good schema
In his paper, The Winograd Schema Challenge Hector Levesque 2011 proposes to assemble a corpus of such Winograd schemas that are
easily disambiguated by the human reader ideally, the reader does not even notice there is an ambiguity;
not solvable by simple techniques such as selectional restrictions
Googleproof; ie no statistical test over text corpora that will reliably disambiguate.
The corpus would then be presented as a challenge for AI programs, along the lines of the Turing test. The strengths of the challenge are that it is more clearcut.
KRR Introductiontothe KnowledgeRepresenationandReasoningMastersCourse Contents KRR19

More Winograd Schemas
The trophy would not fit into the brown suitcase because it was too smalllarge. What was too smalllarge?
Joan made sure to thank Susan for all the help she had givenreceived. Who had givenreceived help?
The large ball crashed right through the table because it was made of steelstyrofoam What was made of steelstyrofoam?
KRR Introductiontothe KnowledgeRepresenationandReasoningMastersCourse Contents KRR110

COMP5450M
Knowledge Representation
Lecture KRR2
Introduction to Knowledge Represenation and Reasoning
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR21

AI and the KR Paradigm
The methodology of Knowledge Representation and Automated Reasoning is one of the major strands AI research.
It employs symbolic representation of information together with logical inference procedures as a means for solving problems.
Most of the earliest investigations into AI adopted this approach and it is still going strong. It is sometimes called GOFAI good oldfashioned AI.
However, it is not the only and perhaps not the most fashionable approach to AI.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR22

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? KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR23

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 highlevel intelligence.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR24

Intelligence via Language
The KR paradigm takes language as an essential vehicle for
intelligence.
Animals can be seen as semiintelligent because they only posses a rudimentary form of language.
The principle role of language is to represent information.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR25

Language and Representation
Written language seems to have its origins in pictorial representations.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR26

Language and Representation
Written language seems to have its origins in pictorial representations.
However, it evolved into a much more abstract representation.
KRR IntroductiontoKnowledgeRepresenationandReasoning
Contents
KRR26

Language and Logic
Pattersofnaturallanguageinferenceareusedasaguidetothe form of valid principles of logical deduction.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR27

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.
RS R
S
KRR IntroductiontoKnowledgeRepresenationandReasoning
Contents
KRR27

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.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR28

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 semiformal.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR29

What do we represent?
Ourproblem.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR210

What do we represent?
Ourproblem.
What would count as a solution.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR210

What do we represent?
Ourproblem.
What would count as a solution. Facts about the world.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR210

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.
KRR IntroductiontoKnowledgeRepresenationandReasoning
Contents
KRR210

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.
KRR IntroductiontoKnowledgeRepresenationandReasoning
Contents
KRR210

Finding a Good Representation
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR211

Finding a Good Representation
Wemustdeterminewhatknowledgeisrelevanttotheproblem.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR211

Finding a Good Representation
Wemustdeterminewhatknowledgeisrelevanttotheproblem. We need to find a suitable level of abstraction.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR211

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.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR211

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.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR211

Inference and Computation
A tough issue that any AI reasoning system must confront is that of Tractability.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR212

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.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR212

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. KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR212

Time and Change
112 Standard, classical logic was developed 112 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.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR213

Spatial Information
Knowledge of spatial properties and relationships is required for many commonsense reasoning problems.
While mathematical models exist they are not always wellsuited for AI problem domains.
We shall look at some ways of representing qualitative spatial information.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR214

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?
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR215

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:
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR216

Robotic Control
An important application for spatiotemporal 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 highlevel control of autonomous agents is a major goal of KR.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR217

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 .
We shall only briefly cover uncertainty in AR34.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR218

Ontology
Literally Ontology means the study of exists. It is studied in philosophy as a branch of Metaphysics.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR219

Ontology
Literally Ontology means the study of 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.
We shall examine ontologies in some detail.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR219

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.
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR220

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?
KRR IntroductiontoKnowledgeRepresenationandReasoning Contents KRR220

COMP5450M
Knowledge Representation
Lecture KRR3
Classical Logic I: Concepts and Uses of Logic
KRR ClassicalLogicI:ConceptsandUsesofLogic
Contents
KRR31

Lecture Plan
Formal Analysis of Inference Propositional Logic
Validity
Quantification
Uses of Logic
KRR ClassicalLogicI:ConceptsandUsesofLogic
Contents
KRR32

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.
KRR ClassicalLogicI:ConceptsandUsesofLogic Contents KRR33

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.
KRR ClassicalLogicI:ConceptsandUsesofLogic Contents KRR34

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. KRR ClassicalLogicI:ConceptsandUsesofLogic Contents KRR35

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 ….
KRR ClassicalLogicI:ConceptsandUsesofLogic
Contents
KRR36

Symbols for the Connectives
The propositional connectives are represented by the following symbols:
and or
P Q
P Q P Q
P QR, P QR
Brackets prevent ambiguity which would otherwise occur in a
formula such as P Q R.
More complex examples:
if…then
not P
KRR ClassicalLogicI:ConceptsandUsesofLogic Contents KRR37

Propositional Formulae
We can precisely specify the wellformed formulae of propositional logic by the following recursive characterisation:
Each of a set, P, of propositional constants Pi is a formula. Ifisaformulasois.
Ifandareformulaesois.
Ifandareformulaesois.
The propositional connectives , and are respectively called negation, conjunction and disjunction.
KRR ClassicalLogicI:ConceptsandUsesofLogic Contents KRR38

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.
KRR ClassicalLogicI:ConceptsandUsesofLogic Contents KRR39

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 rewrite rule: one that preserves the truth of formulae i.e. if the premisses are true so is the conclusion.
KRR ClassicalLogicI:ConceptsandUsesofLogic Contents KRR310

More Simple Examples
And Elimination And Introduction

Or Introduction

Not Elimination

KRR ClassicalLogicI:ConceptsandUsesofLogic
Contents
KRR311

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.
KRR ClassicalLogicI:ConceptsandUsesofLogic Contents KRR312

A 2Step 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 RB T R
B
Here we have used the or introduction rule followed by good old modus ponens.
KRR ClassicalLogicI:ConceptsandUsesofLogic Contents KRR313

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.
KRR ClassicalLogicI:ConceptsandUsesofLogic Contents KRR314

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
KRR ClassicalLogicI:ConceptsandUsesofLogic Contents KRR315

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.
KRR ClassicalLogicI:ConceptsandUsesofLogic Contents KRR316

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.
Ra, b, c Lovesjohn, mary
With many binary 2place relations the relation symbol is often
written between its operands e.g. 4 3.
Unary 1place relations are also called properties Talltom.
KRR ClassicalLogicI:ConceptsandUsesofLogic Contents KRR317

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 Dogspot Mammalspot, 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:
xDogx Mammalx
in which is the universal quantifier symbol and x is a variable
indicating which property is being quantified.
KRR ClassicalLogicI:ConceptsandUsesofLogic Contents KRR318

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:
xInysx Inukx Inysl
Inukl
Later we shall examine quantification in more detail. KRR ClassicalLogicI:ConceptsandUsesofLogic
Contents
KRR319

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.
KRR ClassicalLogicI:ConceptsandUsesofLogic Contents KRR320

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.
KRR ClassicalLogicI:ConceptsandUsesofLogic Contents KRR321

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 xEmployeex agex 0, then we must verify that:

We can do this using a proof system S if we can show that:
S
KRR ClassicalLogicI:ConceptsandUsesofLogic Contents KRR322

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: Locatedx, y Furniturex ?
Ans: x sofa1, y lounge , x table1, y kitchen , …
KRR ClassicalLogicI:ConceptsandUsesofLogic Contents KRR323

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.
KRR ClassicalLogicI:ConceptsandUsesofLogic Contents KRR324

COMP5450M
Knowledge Representation
Lecture KRR4
Classical Logic II:
Formal Systems, Proofs and Semantics
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR41

Sequents
A sequent is an expression of the form:
1, …, m 1, …, n where all 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. This notation as we shall soon see is very useful in
presenting inference rules in a concise and uniform way.
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR42

Special forms of sequent
A sequent with an empty lefthand 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 righthand side: 1, . . . , m
asserts that the set of premisses 1, …, m is inconsistent, which means that a formula of the form is provable from this set.
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR43

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:
,, ,
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR44

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.
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR45

A Propositional Sequent Calculus
Axiom: Rewrite:
, ,
Rules:
,, , and ,
,
, and ,
,
,
,
,
, ,
,
,
,
Exercise: Show that the rules and can be replaced by the rewrite rule .
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR46

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. KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR47

Proof Example 1
P Q, P Q
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR48

Proof Example 2
P Q P Q
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR49

Proof Example 3
P QR, P S, QSRS
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR410

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.
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR411

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 which are called truthvalues.
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 truthfunctions which completely determine the truthvalues of complex propositions in terms of the values of their atomic constituents.
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR412

TruthTables
The truthfunctions 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 truthvalue of the complex proposition formed by the connective for all possible truthvalues of the component propositions.
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR413

The TruthFunction for
The truthfunction 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 truthfunctionally equivalent to .
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR414

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 truthvalue 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 truthvalue of the atoms is given directly and the values of complex formulae are determined by the truthfunctions.
If a model, M, makes a formula, , true then we say that M satisfies .
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR415

Validity in terms of Models
Recall that an arguments 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 truthfunctional 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 truthfunctionally 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.
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR416

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 truthfunctional semantics for propositional formulae.
Thus,
How this can be show is beyond the scope of this course. KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR417
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:
xx
being the existential quantifier symbol.
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR418

Multiple Quantifiers
Consider the sentence: Everybody loves somebody We can consider this as being formed from an expression of the form lovesjohn, mary by the following stages.
First we remove mary to form the property lovesjohn, . . . which we existentially quantify to get: x lovesjohn, x
Then by removing john we get the property x loves…,x which we quantify universally to end up with:
y xlovesy, 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.
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR419

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 rewrite rule.
These two forms of formula are equivalent in meaning.
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR420

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.
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR421

An example
As an example we now prove that the formula xP x P x is a theorem of predicate logic. This formula asserts that every object either has or does not have the property P . . ..
Pa Pa Pa,Pa
PaPa xPxPx
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.
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR422

Another Example
Consider the follwing illegal application of : Pb Pb
Pb xPx
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.
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR423

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:
Fa Fa Fb xFx FaFb
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics
Contents KRR424

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.
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR425

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.
Fa,… Fa and …,Fb,… Fb Fa, Fb,xFx Fa Fb Fa, xFx Fa Fb
xFx FaFb
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR426

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.
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR427

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
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR428

Decidability
A class of problems is decidable if there is a decision procedure for that class; otherwise it is undecidable.
Problem classes 13 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.
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR429

SemiDecidability
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 semidecidable if every positive case can be verified in finite time but there is no procedure which will refute every negative case in finite time.
KRR ClassicalLogicII:FormalSystems,ProofsandSemantics Contents KRR430

COMP5450M
Knowledge Representation
Lecture KRR5
Classical Logic III: Representation in FirstOrder Logic
KRR RepresentationinFirstOrderLogic Contents KRR51

FirstOrder Logic
As we have seen FirstOrder Logic extends Propositional Logic in two ways:
The meanings of atomic propositions may be represented in terms of properties and relations holding among named objects.
Expressive power is further increased by the use of variables and quantifiers, which can be used to represent generalised or nonspecific information.
Note: a quantifier is called firstorder if its variable ranges over individual entities of a domain. Secondorder quantification is where the quantified variable ranges over sets of entities. In this course we shall restrict our attention to the firstorder case.
KRR RepresentationinFirstOrderLogic Contents KRR52

Terminology
The terms predicate, relation, and property are more or less equivalent.
Property tends to imply a predicate with exactly one argument e.g. P x, Redx, Catx.
Relation tends to imply a predicate with at least two arguments e.g. Rx, y, Tallerx, y, z, Gavex, y, z.
The term Predicate does not usually imply anything about the number of arguments athough occasionally it is used to imply just one argument.
FirstOrder Logic is sometimes referred to as Predicate Logic.
KRR RepresentationinFirstOrderLogic Contents KRR53

Symbols of FirstOrder Logic
Firstorder logic employs the following symbols:
Predicate symbols each with a fixed arity i.e. number of
arguments: P,Q,R,Red,Taller…
Constants names of particular individuals: a, b, john, leeds, …
Variable symbols: x, y, z, u, v, …
TruthFunctional Connectives unary: ,
binary: , , ,
Quantifiers: ,
The equality relation:
FirstOrder logic may be used with or without equality.
KRR RepresentationinFirstOrderLogic
Contents KRR54

Formulae of FirstOrder Logic
An atomic formula is an expression of the form: 1,…,n or 1 2
where is a relation symbol of arity n, and each i is either a constant or a variable.
A firstorder logic formula is either an atomic formula or a finite expression of one of the forms:
, , x, x
where and are firstorder formulae and is any of the binary
connectives, , or .
KRR RepresentationinFirstOrderLogic Contents KRR55

Restrictions on Quantification
Although the standard semantics for firstorder logic will assign a meaning to any formula fitting the stipulation on the previous slide, sensible formulae satisfy some further conditions:
For every quantification or there is at least one further occurrence of the variable in .
No quantification occurs within the scope of another quantification using the same variable.
Every variable occurs within the scope of a quantification using that variable.
The scope of a symbol in formula is the smallest sub expression of which contains and is a firstorder formula.
KRR RepresentationinFirstOrderLogic Contents KRR56

Simple Examples
using Relations and Quantifiers
Tom talks to Mary
Tom talks to himself
Tom talks to everyone Everyone talks to tom Tom talks to no one Everyone talks to themself Only Tom talks to himself
TalksTotom, mary TalksTotom, tom xTalksTotom, x xTalksTox, tom xTalksTotom, x xTalksTox, x xTalksTox, x x tom
KRR RepresentationinFirstOrderLogic
Contents
KRR57

Typical Forms of Quantification
All frogs are green:
xF x Gx Some frogs are poisonous:
No frogs are silver:
KRR RepresentationinFirstOrderLogic
Contents
KRR58
xF x P x
xF x Sx

Representing Numbers
In the standard predicate logic, we only have two types of quantifier:
xx and xx
How can we represent a statement such as I saw two birds ?
What about
xySawi, x Sawi, y ? This doesnt work. Why?
KRR RepresentationinFirstOrderLogic
Contents KRR59

At Least n
For any natural number n we can specify that there are at least n
things satisfying a given condition.
John owns at least two dogs:
xyDogx Dogy x y
Ownsjohn, x Ownsjohn, y
John owns at least three dogs:
xyzDogx Dogy Dogz
x y x z y z
Ownsjohn, x Ownsjohn, y Ownsjohn, z
KRR RepresentationinFirstOrderLogic Contents KRR510

At Most n
Every student owns at most one computer:
xStudentx yzCompy Compz y z
Ownsx, y Ownsx, z
or equivalently
xyz Studentx Compy Compz
Ownsx,y Ownsx,z y z
KRR RepresentationinFirstOrderLogic Contents KRR511

Exactly n
To state that a property holds for exactly n objects, we need to assert that it holds for at least n objects, but deny that it holds for at least n 1 objects:
A triangle has exactly 3 sides:
tTrianglet
xyzSideOfx, t SideOfy, t SideOfz, t
x y y z x z
xyzwSideOfx,t SideOfy,t SideOfz,t SideOfw,t x y y z x z

KRR RepresentationinFirstOrderLogic Contents KRR512

COMP5450M
Knowledge Representation
Lecture KRR6
Classical Logic IV: Semantics for Predicate Logic
KRR ClassicalLogicIV:SemanticsforPredicateLogic Contents KRR61

The Domain of Individuals
Whereas a model for propositional logic assigns truth values directly to propositional variables, in predicate logic the truth of a proposition depends on the meaning of its constituent predicate and arguments.
The arguments of a predicate may be either constant names a, b, … or variables u, v, …, z.
To formalise the meaning of these argument symbols each predicate logic model is associated with a set of entities that is usually called the domain of individuals or the domain of quantification. Note: Individuals may be anything either animate or inanimate, physical or abstract.
Each constant name denotes an element of the domain of individuals and variables are said to range over this domain.
KRR ClassicalLogicIV:SemanticsforPredicateLogic Contents KRR62

Semantics for Property Predication
Before proceeding to a more formal treatment of predicate, I briefly describe the semantics of property predication in a semi formal way.
A property is formalised as a 1place predicate i.e. a predicate applied to one argument.
For instance Happyjane ascribes the property denoted by Happy to the individual denoted by jane.
To give the conditions under which this assertion is true, we specify that Happy denotes the set of all those individuals in the domain that are happy.
Then Happyjane is true just in case the individual denoted by jane is a member of the set of individuals denoted by Happy.
KRR ClassicalLogicIV:SemanticsforPredicateLogic Contents KRR63

Predicate Logic Model Structures
A predicate logic model is a tuple
M D, ,
where:
D is a nonempty set the domain of individuals
i.e. D i1, i2, . . ., where each in represents some entity.
is an assignment function, which gives a value to each
constant name and to each predicate symbol.
KRR ClassicalLogicIV:SemanticsforPredicateLogic Contents KRR64

The Assignment Function
The kind of value given to a symbol by the assignment function
depends on the type of :
If is a constant name then is simply an element of D.
E.g. john denotes an individual called John.
If is a property, then denotes a subset of the elements of D.
This is the subset of all those elements that possess the property . E.g. Red would denote the set of all red things in the domain.
continued on next slide for case where is a relation symbol. KRR ClassicalLogicIV:SemanticsforPredicateLogic Contents KRR65

The Assignment Function for Relations
If is a binary relation, then denotes a set of pairs of elements of D.
For example we might have
R i1, i2, i3, i1, i7, i2, . . .
The value R denotes the set of all pairs of individuals that are related by the relation R.
Note that we may have im, in R but in, im R e.g. John loves Mary but Mary does not love John.
More generally, if is an nary relation, then denotes a set of ntuples of elements of D.
E.g. Between might denote the set of all triples of points, px, py, pz, such that py lies between px and pz.
KRR ClassicalLogicIV:SemanticsforPredicateLogic Contents KRR66

The Semantics of Predication
We have seen how the denotation function assigns a value to each individual constant and each relation symbol in a predicate logic language.
The purpose of this is to define the conditions under which a predicative proposition is true.
Specifically, a predication of the form 1, . . . n is true according to if and only if
1, . . . n
For instance, Lovesjohn, mary is true iff the pair john, mary the pair of individuals denoted by the two names is an element of Loves the set of all pairs, im, in, such that im loves in.
KRR ClassicalLogicIV:SemanticsforPredicateLogic Contents KRR67

Variable Assignments
and Augmented Models
In order to specify the truth conditions of quantified formulae we will have to interpret variables in terms of their possible values.
Given a model M D,, Let V be a function from variable symbols to entities in the domain D.
I will call a pair M,V an augmented model, where V is a variable assignment over the domain of M.
If an assignment V gives the same values as V to all variables except possibly to the variable x, I write this as:
V x V .
This notation will be used in specifying the semantics of
quantification.
KRR ClassicalLogicIV:SemanticsforPredicateLogic Contents KRR68

Truth and Denotation
in Augmented Models
We will use augmented models to specify the truth conditions of predicate logic formulae, by stipulating that is true in M if and only if is true in a corresponding augmented model M, V .
It will turn out that if a formula is true in any augmented model of M, then it is true in every augmented model of M. The purpose of the augmented models is to give a denotation for variables.
From an augmented model M, V , where M D, , we define the function V , which gives a denotation for both constant names and variable symbols. Specifically:
V , where is a constant;
V V , where is a variable.
KRR ClassicalLogicIV:SemanticsforPredicateLogic Contents KRR69

Semantics for
the Universal Quantifier
We are now in a position to specify the conditions under which a universally quantified formula is true in an augmented model:
xx is true in M, V iff xistrueineveryM,V,suchthatV x V.
In other words this means that xx is true in a model just in case the subformula x is true whatever entity is assigned as the value of variable x, while keeping constant any values already assigned to other variables in .
We can define existential quantification in terms of universal quantification and negation; but what definition might we give to define its semantics directly?
KRR ClassicalLogicIV:SemanticsforPredicateLogic Contents KRR610

Semantics of Equality
In predicate logic, it is very common to make use of the special relation of equality, .
The meaning of can be captured by specifying axioms such as xyx y Px Py
of by means of more general inference rules such as, from and derive .
We can also specify the truth conditions of equality formulae using our augmented model structures:
istrueinM,V,whereMD,,
iff V is the same entity as V .
KRR ClassicalLogicIV:SemanticsforPredicateLogic Contents KRR611

Full Semantics of Predicate Logic
1,…nistrueinM,V,whereMD,, iff V 1, . . . V n .
istrueinM,V,whereMD,,iffVV.

xx
istrueinM,Viffisnot trueinM,V istrueinM,ViffbothandaretrueinM,V istrueinM,ViffeitheroristrueinM,V
is true in M, V iff xistrueineveryM,V,suchthatV x V.
KRR ClassicalLogicIV:SemanticsforPredicateLogic Contents KRR612

COMP5450M
Knowledge Representation
Lecture KRR7
Representing Time and Change
KRR RepresentingTimeandChange Contents KRR71

Lecture Overview
This lecture has the following goals:
to demonstrate the importance of temporal information in knowledge representation.
to introduce two basic logical formalisms for describing time 1storder temporal logic and Tense Logic.
to present two AI formalisms for representing actions and change STRIPS and Situation Calculus.
to explain Frame Problem and some possible solutions.
KRR RepresentingTimeandChange Contents KRR72

Classical Propositions are Eternal
A classical proposition is either true or false.
So it cannot be true sometimes and false at other times.
Hence a contingent statement such as Tom is at the University does not really express a classical proposition.
Its truth depends on when the statement is made.
A corresponding classical proposition would be something like:
Tom wasiswill be at the University at 11:22am 822002.
This statement, if true, is eternally true.
KRR RepresentingTimeandChange Contents KRR73

Building Time into 1storder Logic
We can explicitly add time references to 1storder formulae. For example
HappyJohn, t could mean John is happy at time t.
In this representation each predicate is given an extra argument place specifying the time at which it is true.
KRR RepresentingTimeandChange Contents KRR74

Time as an Ordering of Time Points
To talk about the ordering of time points we introduce the special relation . Being a linear order it satisfies the following axioms.
1. t1t2t3t1 t2 t2 t3 t1 t3 , 2. t1t2t1 t2 t2 t1 ,
3. t1t2t1 t2 t2 t1 t1 t2,
transitivity linearity
antisymmetry
KRR RepresentingTimeandChange
Contents KRR75

Some Further Possible Axioms
Time will continue infinitely in the future:
ttt t
KRR RepresentingTimeandChange
Contents KRR76

Some Further Possible Axioms
Time will continue infinitely in the future:
ttt t What does the following axiom say?
t1t2t1 t2 t3t1 t3 t3 t2
KRR RepresentingTimeandChange Contents KRR76

Some Further Possible Axioms
Time will continue infinitely in the future:
ttt t What does the following axiom say?
t1t2t1 t2 t3t1 t3 t3 t2
This asserts the infinite divisibility of time usually called density.
KRR RepresentingTimeandChange Contents KRR76

Representing Temporal Ordering
Sue is happy but will be sad:
HappySue, 0 t0 t SadSue, t Here I use 0 to stand for the present time.
KRR RepresentingTimeandChange Contents KRR77

Representing Temporal Ordering
Sue is happy but will be sad:
HappySue, 0 t0 t SadSue, t Here I use 0 to stand for the present time.
We can describe more complex temporal constraints of a causal nature.
E.g. When the sun comes out I am happy until it rains:
tSt ut u rt r r u Rr Hu
KRR RepresentingTimeandChange Contents KRR77

Another Way of Adding Time
Rather than adding time to each predicate, several AI researchers have found it more convenient to use a special type of relation between propositions and time points:
HoldsAtHappyJohn, t
Can use this to define temporal relations in a more general way.
E.g.:
tHoldsAt, t tt t HoldsAt, t
KRR RepresentingTimeandChange Contents KRR78

Axioms for HoldsAt
1. HoldsAt, t HoldsAt , t HoldsAt, t 2. HoldsAt , t
3. HoldsAt, t HoldsAt, t
4. HoldsAt, t HoldsAtHoldsAt, t, t
5. t t HoldsAtt t, t
6. tHoldsAt, t HoldsAtt, t
KRR RepresentingTimeandChange
Contents
KRR79

Tense Logic
Rather than quantifying over time points, it may be simpler to treat time in terms of tense.
P means that was true at some time in the past. F means that will be true at some time in the future.
KRR RepresentingTimeandChange Contents KRR710

Axioms for Tense Operators
The tense operators obey certain axioms. For example:
1. F PF 2. P FP 3. PP P
4. FF F
Can you think of any more?
KRR RepresentingTimeandChange
Contents
KRR711

Priors Tense Logic
It is convenient to define:
has always been true H def P
will always be true G def F
KRR RepresentingTimeandChange
Contents KRR712

Priors Tense Logic
It is convenient to define:
has always been true will always be true H def P G def F
We now specify the following axioms:
1 HHH 2 GGG
3 HF
5 PGP
7 PHFP 9 P
4 GP
6 FHF
8 FGFP
10 F
Together with any sufficient axiom set for classical propositional
logic.
KRR RepresentingTimeandChange Contents KRR712

Models for Tense Logics
A tense logic model is given by a set M …,Mi,… of atemporal classical models, whose indices are ordered by a relation .
KRR RepresentingTimeandChange Contents KRR713

Models for Tense Logics
A tense logic model is given by a set M …,Mi,… of atemporal classical models, whose indices are ordered by a relation .
The models can be pictured as corresponding to different moments along the time line:
KRR RepresentingTimeandChange Contents KRR713

Validity in Tense Logic Models
Truth values of atemporal classical formulae are determined by each model as usual. A classical formula is true at index point i iff it is true according to Mi.
Tensed formulae are interpreted by:
Fistrueatiiffistrueatsomej suchthatij.
Pistrueatiiffistrueatsomej suchthatj i.
A tense logic formula is valid iff it is true at every index point in
every tense logic model.
KRR RepresentingTimeandChange Contents KRR714

Reasoning with Tense Logic
Reasoning directly with tense logic is extremely difficult. We need to combine classical propositional reasoning with substitution in the axioms.
Exercise: try to prove that PPp Pp from Priors axioms.
I couldnt !
But Model Building techniques can be quite efficient.
A model is an ordered set of time points, each associated with a set of formulae.
A proof algorithm can exhaustively search for a model satisfying any given formula.
KRR RepresentingTimeandChange Contents KRR715

STRIPS
The STanford Research Institute Planning System is a relatively simple algorithm for reasoning about actions and formulating plans.
STRIPS models a state of the world by a set of atomic facts. Actions are modelled as rules for adding and deleting facts.
Specifically each action definition consists of:
Action Description: Preconditions: Delete List:
Add List:
for example
movex, loc1, loc2
atx, loc1, movablex, freeloc2
atx, loc1, freeloc2
atx, loc2, freeloc1
KRR RepresentingTimeandChange
Contents KRR716

GoalDirected Planning
The STRIPS system enables a relatively straightforward implementation of goaldirected planning.
To find a plan to achieve a goal G we can use an algorithm of the following form:
1. If G is already in the set of world facts we have succeeded.
2. Otherwise look for an action definition
, 1,…,l, 1,…,m, 1,…, G, …,n with G in its add list.
3. Then successively set each precondition i as a new sub goal and repeat this procedure.
More complex search strategy is needed for good performance. KRR RepresentingTimeandChange Contents KRR717

Limitations of STRIPS
STRIPS works well in cases where the effects of actions can be captured by simple adding and deleting of facts. However, for general types of action that can be applied in a variety of circumstances, the effects are often highly dependent on context.
Even with the simple action movex,loc1,loc2 the changes in facts involving x will depend on what other objects are near to loc1 and loc2.
In general the interdependencies of even simple relationships. Are highly complex. Consider the ways in which a relation visiblefromx,y can change e.g. when crates are moved around in a warehouse.
KRR RepresentingTimeandChange Contents KRR718

Situation Calculus
Situation Calculus is a 1storder language for representing dynamically changing worlds.
Properties of a state of the world are represented by:
holds,s meaning that proposition holds in state s.
In the terminology of Sit Calc is called a fluent.
KRR RepresentingTimeandChange Contents KRR719

Actions in Sit Calc
In Sit Calc all changes are the result of actions:
result,s denotes the state resulting from doing action
when in state s.
KRR RepresentingTimeandChange Contents KRR720

Actions in Sit Calc
In Sit Calc all changes are the result of actions:
result,s denotes the state resulting from doing action
when in state s.
We can write formulae such as:
holds LightOff, s holds LightOn, result switch, s
KRR RepresentingTimeandChange Contents KRR720

Effect Axioms
Effect axioms specify fluents that must hold in the state resulting from an action of some given type.
Simple effect axioms can be written in the form:
holds,result,s poss,s
The reverse arrow is used so that the most important part is at the beginning. It also corresponds to form used in Prolog implemen tations.
Here poss is an auxiliary predicate that is often used to separate the preconditions of an action from the rest of the formula.
holdshasy, i, resultgivex, i, y, s possgivex, i, y, s KRR RepresentingTimeandChange Contents KRR721

Precondition Axioms
Preconditions tell us what fluents must hold in a situation for it to be possible to carry out a given type of action in that situation.
If we are using the poss predicate, a simple precondition takes the form:
Example:
poss,s holds,s
possgivex, i, y, s holdshasx, i, s
KRR RepresentingTimeandChange Contents KRR722

More Examples
poss mendx, i, s
KRR RepresentingTimeandChange Contents KRR723

More Examples
poss mendx, i, s
holds hasx, i brokeni hasx, glue, s
KRR RepresentingTimeandChange Contents KRR723

More Examples
poss mendx, i, s
holds hasx, i brokeni hasx, glue, s
possstealx, i, y, s
KRR RepresentingTimeandChange Contents KRR723

More Examples
poss mendx, i, s
holds hasx, i brokeni hasx, glue, s
possstealx, i, y, s
holdshasy, i asleepy stealthyx, s
KRR RepresentingTimeandChange Contents KRR723

Domain Axioms
As well as axioms describing the transition from one state to another actions and their effects, a Situation Calculus theory will often include domain axioms specifying conditions that must hold in every possible situation.
As well as fluents, a Sit Calc theory may utilise static predicates expressing properties that do not change.
ConnectedByDoorkitchen,dining room,door1 r1r2dConnectedByDoorr1, r2, d ConnectedByDoorr2, r1, d
KRR RepresentingTimeandChange Contents KRR724

Frame Axioms
Frame axioms tell us what fluents do not change when an action takes place.
KRR RepresentingTimeandChange Contents KRR725

Frame Axioms
Frame axioms tell us what fluents do not change when an action takes place.
When youre dead you stay dead:
holdsdeadx, result, s holdsdeadx, s
KRR RepresentingTimeandChange Contents KRR725

Frame Axioms
Frame axioms tell us what fluents do not change when an action takes place.
When youre dead you stay dead:
holdsdeadx, result, s holdsdeadx, s
Giving something wont mend it:
holdsbrokeni, resultgivex, i, y, s holdsbrokeni, s
KRR RepresentingTimeandChange Contents KRR725

holdsbrokeni, result, s
holds brokeni, s x mendx, i
KRR RepresentingTimeandChange Contents KRR726

The Frame Problem
Intuitively it would seem that, if we specify all the effects of an action, we should be able to infer what it doesnt affect.
We would like to have a general way of automatically deriving reasonable frame conditions.
The frame problem is that no completely general way of doing this has been found.
KRR RepresentingTimeandChange Contents KRR727

Solving the Frame Problem
The AI literature contains numerous suggestions for solving the frame problem.
None commands universal acceptance. There are two basic approaches:
KRR RepresentingTimeandChange Contents KRR728

Solving the Frame Problem
The AI literature contains numerous suggestions for solving the frame problem.
None commands universal acceptance. There are two basic approaches:
Syntactic derivation of frame axioms from effect axioms.
KRR RepresentingTimeandChange Contents KRR728

Ramifications
KRR RepresentingTimeandChange Contents KRR729

Events and Intervals
Tense logic and logics with explicit time variables represent change in terms of what is true along a series of time points. They have no way of saying that some event or process happens over some interval of time.
A conceptualisation of time in terms of intervals and events was proposed by James Allen and also Pat Hayes in the early 80s.
The formalism contains variables standing for temporal intervals and terms denoting types of event.
KRR RepresentingTimeandChange Contents KRR730

Allens Interval Relations
Allen also identified 13 qualitatively different relations that can hold between termporal intervals:
KRR RepresentingTimeandChange Contents KRR731

Ordering Events
By combining the occurs relation with the interval relations we can describe the ordering of events:
Occursget dressed,i Occurstravel to work, j Occursread newspaper,k Beforei, j
Duringk, j
KRR RepresentingTimeandChange
Contents
KRR732

COMP5450M
Knowledge Representation
KRR Prolog
Contents KRR81
Lecture KRR8
Prolog

Reasons to Learn a Bit of Prolog
The Logic Programming paradigm is radically different from the traditional imperative style; so knowledge of Prolog helps develop a broad appreciation of programming techniques.
Although not usually employed as a general purpose programming language, Prolog is wellsuited for certain tasks and is used in many research applications.
KRR Prolog Contents KRR82

Pitfalls in Learning Prolog
One reason that Prolog is not more widely used is that a beginner can often encounter some serious difficulties.
Trying to crowbar an imperative algorithm into Prolog syntax will generally result in complex, ugly and often incorrect code. A good Prolog solution must be formulated from the beginning in the logic programming idiom. Forget loops and assignments and think in terms of Prolog concepts.
Another difficulty is in getting to grips the execution sequence of Prolog programs. This is subtle because Prolog is written declaratively. Nevertheless, its search for solutions does proceed in a determinate fashion and unless code is carefully ordered it may search forever, even when a solution exists.
KRR Prolog Contents KRR83

Prolog Structures
You should be aware that coding for many kinds of application is facilitated by representing data in a structured way. Prolog like Lisp provides generic syntax for structuring data that can be applied to all manner of particular requirements.
A complex term takes the following form:
operatorarg1, …, argN Where arg1, …, argN may also be complex terms.
Although such a term looks like a function, it is not evaluated by applying the function to the arguments. Instead Prolog tries to find values for which it is true by matching it to the facts and rules given in the code.
KRR Prolog Contents KRR84

Pattern Matching and Equality
When evaluating a query containing one or more variables, Prolog tries to match the query to a stored or derivable fact, in which variables may be replaced by particular instances.
In fact the matching always goes both ways. If we have the code:
likes X, X .
Then the query ? likes john, john will give yes, even though there are no facts given about john, because the query matches the general fact which says that everyone likes themself.
KRR Prolog Contents KRR85

Matching Complex Terms
Prolog will also find matches of complex terms as long as there is a instantiation of variables that makes the terms equivalent:
loves brotherX, daughtertom .
? loves brother susan , Y .
X susan,
Y daughtertom
We can make Prolog perform a match using the equality operator:
? fgX,this,X fZ,Y,that. X that,
Y this,
Z gthat
Note that no evaluation of f and g takes place.
KRR Prolog Contents KRR86

Coding by Matching
A surprising amount of functionality can be achieved simply by pattern matching.
Consider the following code:
vertical linepointX,Y, pointX,Z .
horizontal linepointX,Y, pointZ,Y .
Here we are assuming a representation of line objects as pairs of point objects, which in turn are pairs of coordinates.
KRR Prolog Contents KRR87

The List Constructor Operator
The basic syntax that is used either to construct or to break up lists in Prolog is the headtail structure:
Head Tail
Here Head is any term. It could be an atom, a variable or some
complex structure.
Tail is either a variable or any kind of list structure.
The structure Head Tail denotes the list formed by adding Head at the front of the list Tail.
Thus a b,c,d denotes the list a,b,c,d.
KRR Prolog Contents KRR88

Matching Lists
Consider the following query:
? H T a, b, c, d, e.
KRR Prolog Contents KRR89

Matching Lists
Consider the following query:
? H T a, b, c, d, e.
This will return:
Head a,
Tail b,c,d,e
KRR Prolog
Contents
KRR89

Matching Lists
Consider the following query:
? H T a, b, c, d, e.
This will return:
Head a,
Tail b,c,d,e
Note that this is identical in meaning to:
? a, b, c, d, e H T .
KRR Prolog
Contents
KRR89

Recursion Over Lists
The following example is of utmost significance in illustrating the nature of Prolog. It combines, pattern matching, lists and recursive definition. Learn this:
inlist X, X .
inlist X, Rest : inlist X, Rest .
Given this definition, in listelt, list will be true, just in case elt is a member of list.
KRR Prolog Contents KRR810

Check if Arrays Share a Value in C
include stdio.h
int main
int arrayA 4 1,2,3,4;
int arrayB 3 3,6,9;
if arrayssharevalue arrayA, 4, arrayB, 3
printfYESn;
else printfNOn;

int arrayssharevalue int A1, int len1, int A2, int len2
int i, j;
for i 0; i len1; i
for j 0; j len2; j
if A1i A2j return 1;

return 0;
KRR Prolog
Contents
KRR811

Check if Lists Share an Element in Prolog
listsshareelement L1, L2 :
member X, L1 ,
member X, L2 .
? listsshareelement 1,2,3,4, 3,6,9 .
yes
KRR Prolog Contents KRR812

More Useful Prolog Operators and BuiltIns
We shall now briefly look at some other useful Prolog constructs using the following operators and builtin predicates:
math evaluation: is negation:
disjunction: ;
setof
cut: !
KRR Prolog
Contents
KRR813

Math Evaluation with is
Though possible, it would be rather tedious and very inefficient to code basic mathematical operations in term of Prolog facts and rules e.g. add1,1,2., add1,2,3. etc.
However, the is enables one to evaluate a math expression and bind the value obtained to a variable.
For example after executing the code line
X is sqrt 57 log10
Prolog will bind X to the appropriate decimal number:
X 7.700817170469251
KRR Prolog
Contents
KRR814

The Negation Operator,
It is often useful to check that a particular goal expression does
not succeed.
This is done with the operator. E.g.
lovesjohn, mary
lovesjohn, X
By using brackets one can check wether two or more predicates
cannot be simultaneously satisfied:
member Z, L1, memberZ, L2
KRR Prolog Contents KRR815

Forming Disjunctions with ;
Sometimes we may want to test whether either of two goals is
satisfied. We can do this with an expression such as:
handsomeX ; richX
This will be true if there is a value of X, such that either the
handsome or the rich predicate is true for this value. Thus, we could define:
attractive X : handsomeX ; richX .
KRR Prolog Contents KRR816

Combining Operators
In general, we can combine several operators to form a complex goal which is a truth functional combination of several simpler goals.
E.g.:
KRR Prolog
Contents
KRR817
eligible X : handsome X ,
singleX ; richX,
cheesygrin X .

The setof Predicate
It is often very useful to be able to find the set of all possible values
that satisfy a given predicate.
This can be done with the special builtin setof predicate, which is used in the following way:
setof X, some predicateX, L
This is true if L is a list whose members are all those values of X,
which satisfy the predicate some predicateX. E.g.:
eligibleshortlist L :
setof X, eligibleX, L .
KRR Prolog Contents KRR818

The Cut Operator, !
The socalled cut operator is used to control the flow of execution, by preventing Prolog backtrack past the cut to look for alternative solutions.
Consider the following miniprogram:
reda. blackb.
colorP,red : redP, !.
colorP,black : blackP, !.
colorP,unknown.
Consider what happens if we give the following queries:
? colora, Col.
? colorc, Col.
What would be the difference if the cuts were removed?
KRR Prolog Contents KRR819

Data Record Processing Example
Here is a typical example of how some data might be stored in the form of Prolog facts:
ID Surname
student 101, SMITH,
student 102, SMITH,
student 103, JONES,
student 104, DEMORGAN Augustus, log2010adm, Logic .
student 105, RAMCHUNDRA, Lal,
coursework 1, comp2010js, 45 .
coursework 1, comp2010ss, 66 .
coursework 1, comp2010jj, 35 .
coursework 1, log2010adm, 99 .
coursework 1, log2010lr, 87 .
log2010lr, Logic .
KRR Prolog
Contents
KRR820
First Name User Name Degree
John, comp2010js, Computing .
Sarah, comp2010ss, Computing .
Jack, comp2010jj, Computing .

Deriving Further Info from the Data
Given the data format used on the previous slide, the following code concisely defines how to derive the top mark for a given coursework:
topmark CW, First, Sur :
coursework CW, User, Mark1 ,
coursework CW, , Mark2 ,
Mark2 Mark1
,
student , Sur, First, User, .
Note: the extra layer of bracketing in … is required in order to compound two predicates to form a single argument for the operator.
KRR Prolog Contents KRR821

More Data Extraction Rules
Here are some further useful rules for extracting information from the student and coursework data:
studentuser U : student , , , U, .
userpasscw U, CW :
coursework CW, U, Mark ,
Mark 40.
username U, S,F : student , S, F, U, .
KRR Prolog Contents KRR822

Example Use of setof
The setof operator enables us to straightforwardly derive the
whole set of elements satisfying a given condition:
passlist CW, PassList :
setof Name, UuserpasscwU,CW,
usernameU,Name, PassList
.
Note: the construct U … is a special operator that is used within setof commands to tell prolog that the value of variable U can be different for each member of the set.
KRR Prolog Contents KRR823

Conclusion
The nature of Prolog programming is very different from other languages.
In order to program efficiently you need to understand typical Prolog code examples and build your programs using similar style.
Trying to put imperative ideas into a decarative form can lead to overly complex and error prone code.
Although Prolog code is very much declarative in nature, in order for programs to work correctly and efficiently one must also be aware of how code ordering affects the execution sequence.
KRR Prolog Contents KRR824

COMP5450M
Knowledge Representation
KRR SpatialReasoning
Contents KRR91
Lecture KRR9
Spatial Reasoning

Importance of Spatial Information
Spatial Information is crucial to many important types of software systems. For example:
Geographical Information Systems GIS
Robotic Control
Medical Imaging
Virtual Worlds and Video Games KRR SpatialReasoning
Contents
KRR92

Quantitative Approaches
Most existing computer programs that handle spatial information employ a quantitative representation, based on numerical coordinates.
A polygon is represented by a list of the coordinates of its vertices.
For example, a triangle in 2D space is represented by six numbers two for each of its three corners.
KRR SpatialReasoning Contents KRR93

Qualitative Representations
An approach to spatial reasoning, which is becoming increasingly popular in AI and has been studied for some time at Leeds is to use qualitative representations.
Qualitative representation use high level concepts to describe spatial properties and configurations.
E.g. Px, y can mean that region x is a part of region y. Qualitative spatial theories may be formulated in a standard
logical language, such as 1storder logic.
However the use of special purpose reasoning methods, such as compositional reasoning is often better than using general 1st order reasoning methods.
KRR SpatialReasoning Contents KRR94

Logical Primitives for Geometry
The Euclidean geometry of points can be axiomatised in terms of the single primitive of equidistance which holds between two pairs of points.
EQDx, y, z, w holds just in case distx, y distz, w. Equidistance satisfies the following axioms:
xyEQDx, y, y, x
xyzEQDx, y, z, z x y xyzuvwEQDx, y, z, u EQDx, y, v, w
reflexivity identity transitivity
EQDz, u, v, w
A complete axiomatisation requires quite a few more axioms.
KRR SpatialReasoning Contents KRR95

Points Lines and Regions
In Euclidean geometry and quantitative representations based upon it the point is taken as a primitive entity.
KRR SpatialReasoning Contents KRR96

Points Lines and Regions
In Euclidean geometry and quantitative representations based upon it the point is taken as a primitive entity.
A line can be defined by a pair of points.
KRR SpatialReasoning Contents KRR96

Points Lines and Regions
In Euclidean geometry and quantitative representations based upon it the point is taken as a primitive entity.
A line can be defined by a pair of points.
A two or three dimensional region is represented by a set of points.
Since sets are computationally unmanageable, one can normally only deal with regions corresponding to a restricted classes of point sets. E.g. polygons, polyhedra, spheres, cylinders, etc.
KRR SpatialReasoning Contents KRR96

RegionBased Representations
A number of qualitative representations have been proposed in which spatial regions are taken as primitive entities.
KRR SpatialReasoning Contents KRR97

RegionBased Representations
A number of qualitative representations have been proposed in which spatial regions are taken as primitive entities.
This has several advantages:
Simple qualitative relations between regions do not need to be analysed as complex relations between their points.
Natural language expressions often correspond to properties and relations involving regions rather than points or sets of points.
KRR SpatialReasoning Contents KRR97

The RCC8 Relations
The following set of binary topological relations, known as RCC8, has been found to be particularly significant.
KRR SpatialReasoning Contents KRR98

Example Topological Description
POc1, s DCc1, t DCc1, c2 TPPc2, s ECc2, t NTPPt, s
KRR SpatialReasoning Contents KRR99

Connection as a Topological Primitive
A very wide range of topological concepts can be defined in terms of the single primitive relation Cx, y, which means that region x is connected to region y.
This means that x and y either share some common part they overlap or they may be only externally connected the touch.
Connection is refexive and symmetric i.e. it satisfies the following axioms:
xCx, x xyCx, y Cy, x
KRR SpatialReasoning
Contents KRR910

Defining other Relations from Connection
Many other properties and relations can be defined from connection. For example:
DCx, y def Cx, y
Px, y def zCz, x Cz, y DRx, y def zPz, x Pz, y ECx, y def Cx, y DRx, y
KRR SpatialReasoning
Contents
KRR911

Defining the Sum of two Regions
One can define a function which gives the sum of two regions:
xyzx sumy, z wCw, x Cw, y Cw, z
c sumr, b
KRR SpatialReasoning
Contents KRR912

Intersections
If two regions overlap then there will be a region which is in the intersection of the two. This can be stated by the following axiom:
xyOx, y zINTx, y, z
KRR SpatialReasoning Contents KRR913

Intersections
If two regions overlap then there will be a region which is in the intersection of the two. This can be stated by the following axiom:
xyOx, y zINTx, y, z
So, the following figure satisfies INTr, b, m.
KRR SpatialReasoning Contents KRR913

SelfConnectedness
A region that consists of a single connected piece may be called onepiece, selfconnected or just connected not to be confused with the binary connection relation.
In terms of sum and binary connection we can define:
SCONx yzx sumy, z Cy, z
KRR SpatialReasoning Contents KRR914

Convexity
By adding a primitive notion of convexity e.g. using a convex hull function, we can define many properties relating to shape and also various containment relations.
Here we have: NTPPa, convccvia, POb, convccvia etc..
KRR SpatialReasoning Contents KRR915

Convexity and Convex Hulls
A region is convex just in case it is equal to its own convex hull. Thus, we could define:
CONVx convx x
Conversely, the convex hull function can be defined by:
y convx CONVy Px, y
zCONVz Px, z Py, z
So, the function conv and the predicate CONV are interdefinable. KRR SpatialReasoning Contents KRR916

Congruence
Another very expressive spatial relation which we may wish to employ is that of congruence.
Two regions are congruent, if one can be transformed into the other by a combination of a rotation and a linear displacement and possibly also a mirror image transposition.
KRR SpatialReasoning Contents KRR917

Exercise
Try drawing situations corresponding to the following formulae:
DCa, b DCa, c Pa, convsumb, c
ECa, convb DCa, b
INTa, b, c SCONa SCONb SCONc
POa, b POa, c xCx, a Cx, sumb, c
xyzPx, a Px, b Py, a Py, b Pz, b Pz, a ECa, b conva convb
KRR SpatialReasoning Contents KRR918

COMP5450M
Knowledge Representation
KRR ModesofInference
Contents KRR101
Lecture KRR10
Modes of Inference

Deduction
The form of inference we have studied sofar in this course is known as deduction.
An argument is deductively valid iff: given the truth of its premisses, its conclusion is necessarily true.
KRR ModesofInference Contents KRR102

Induction
A mode of inference which is very common in empirical sciences is induction.
In this form of inference we start with a usually large body of specific facts observations and generalise from this to a universal law.
E.g. from observing many cases we might induce:
All physical bodies not subject to an external force eventually come to a state of rest.
Although supported by many facts and not contradicted by a counterexample, an inductive inference is not deductively valid.
KRR ModesofInference Contents KRR103

Abduction
Abduction is the kind of reasoning where we infer from some observed fact an explanation of that fact.
Specifically, given an explanatory theory and an observed fact , we may abduce if:
,
For abduction to be reasonable we need some way of constraining
to be a good explanation of .
We generally want to abduce a simple fact, not a general principle
that would be induction.
In formal logic this may be difficult; but in ordinary commonsense reasoning abduction seems to be extremely common.
KRR ModesofInference Contents KRR104

Illustration of the Different Modes
1. All beans in the bag are red.
2. These beans came from the bag.
3. These beans are all red.
KRR ModesofInference Contents KRR105

Illustration of the Different Modes
1. All beans in the bag are red.
2. These beans came from the bag.
3. These beans are all red.
What are the following modes of reasoning?:
1, 2 3
KRR ModesofInference
Contents
KRR105

Illustration of the Different Modes
1. All beans in the bag are red.
2. These beans came from the bag.
3. These beans are all red.
What are the following modes of reasoning?:
1, 2 3 1, 3 2
deduction
KRR ModesofInference
Contents KRR105

Other Modes
Are there any other modes of reasoning?
KRR ModesofInference Contents KRR106

COMP5450M
Knowledge Representation
Lecture KRR11
MultiValued and Fuzzy Logics
KRR MultiValuedandFuzzyLogics Contents KRR111

Overview
This lecture gives a brief overview of multivalued and fuzzy logics.
These logics depart from classical logic in that they allow that propositions may have truth values that are intermediate between absolute truth and absolute falsity.
We shall see that giving a semantics for multivalued logics requires that the standard Boolean truth function interpretation of logical operators be replaced by more complex truth functions.
KRR MultiValuedandFuzzyLogics Contents KRR112

Classical Truth Values
In classical logic, it is assumed that every proposition is either true or false and not both.
Thus we take as the principles of excluded middle and non contradiction as fundamental theorems or axioms:

We say that classical logic gives a bivalent account of truth.
KRR MultiValuedandFuzzyLogics Contents KRR113

Degrees of Truth
One of the central ideas of multivalued and fuzzy logics which may be considered a type of multivalued logic is that certain propositions may be neither absolutely true nor absolutely false, but instead may have some intermediate truth value, which lies somewhere in between.
Such propositions typically involve vague adjectives. For instance:
Sue is tall.
Alfred is Bald.
That bag is heavy.
KRR MultiValuedandFuzzyLogics Contents KRR114

3Valued Logic
3valued logic, allows each proposition to have one of three possible truth values.
As well as the usual true T and false F there is a third truth value, which I will write as: U.
The truth value U may be described as: unknown, uncertain or indeterminate; or perhaps partly true.
KRR MultiValuedandFuzzyLogics Contents KRR115

3Valued Truth Tables
Several different 3Valued logics have been proposed, most notably those of ukasiewicz and Kleene.
Both of these logics agree on the basic truthtables for negation, conjunction and disjunction:
A B
B
T
U
F
A
T
T
U
F
U
U
U
F
F
F
F
F
A B
B
T
U
F
A
T
T
T
T
U
T
U
U
F
T
U
F

T
F
U
U
F
T
KRR MultiValuedandFuzzyLogics Contents KRR116

3Valued Implication Functions
Interpretation of the implication connective is more controversial. Keene and ukasiewicz logic give different truth tables for :
Kleene ukasiewicz
A B
B
T
U
F
A
T
T
U
F
U
T
U
U
F
T
T
T
A B
B
T
U
F
A
T
T
U
F
U
T
T
U
F
T
T
T
They differ on the value of A B, where both A and B have the truth value U.
KRR MultiValuedandFuzzyLogics Contents KRR117

Fuzzy Logic
and Fuzzy Truth Values
In the most common form of Fuzzy Logic the truth value of every proposition is a number in the range 0…1, where:
1 is definitely true
0 is definitely false.
0.5 is in the middle between true and false.
Values in 0.5…1 means that the proposition is more true than false though not completely true.
Values in 0…0.5 mean the proposition is more false than true. KRR MultiValuedandFuzzyLogics Contents KRR118

Characteristic Functions for Fuzzy Sets
Fuzzy truth values are often associated with the degree of membership of an entity in a fuzzy set. This is often modelled by a function of some relevant measurable property.
For instance, degree of membership of a person in the set of tall people can be modelled as a function of the height of a person:
Characteristic Function for Tall
1.0 Degree
of Truth
0.5
KRR MultiValuedandFuzzyLogics
Contents
KRR119
5ft 6ft 7ft Height

Fuzzy Truth Functions
The truth values of propositions formed by truth functional connectives in fuzzy logic are standardly modelled by the following numerical operations:
VA 1 VA
VA B MinVA,VB
VA B MaxVA,VB
KRR MultiValuedandFuzzyLogics Contents KRR1110

Examples
TallAlan 0.7 ThinAlan 0.4
So
TallAlan TallAllan ThinAlan TallAlan ThinAlan TallAlan ThinAlan
10.4 0.4 Min0.7, 0.4 0.4 1 M ax0.7, 0.4 0.3 M in0.7, 1 0.4 0.6
KRR MultiValuedandFuzzyLogics
Contents KRR1111

Very and Quite
We can also model other modifications of a proposition as fuzzy truth functions:
VVery V2
VQuite V12
So:
VeryTallAlan 0.72 0.49 QuiteThinAlan 0.412 0.632
KRR MultiValuedandFuzzyLogics
Contents
KRR1112

COMP5450M
Knowledge Representation
Lecture KRR12
NonMonotonic Reasoning
KRR NonMonotonicReasoning Contents KRR121

Monotonic vs NonMonotonic Logic
Classical logic is monotonic. This means that increasing the amount of information i.e. the number of premisses always adds to what can be deduced. Formally we have:

KRR NonMonotonicReasoning Contents KRR122

Monotonic vs NonMonotonic Logic
Classical logic is monotonic. This means that increasing the amount of information i.e. the number of premisses always adds to what can be deduced. Formally we have:

And indeed, in the semantics for classical logics we have:
Conversely a proof system is nonmonotonic iff:

KRR NonMonotonicReasoning Contents KRR122

So, adding information can make a deduction become invalid.
KRR NonMonotonicReasoning Contents KRR123

Motivation for NonMonotonicity
In commonsense reasoning we often draw conclusions that are not completely certain. We may then retract these if we get more information.
KRR NonMonotonicReasoning Contents KRR124

Motivation for NonMonotonicity
In commonsense reasoning we often draw conclusions that are not completely certain. We may then retract these if we get more information.
When we communicate we tend to leave out obvious assumptions.
KRR NonMonotonicReasoning Contents KRR124

The Tweety Example
This example has been discussed endlessly in the nonmonotonic reasoning literature.
Given the fact BirdTweety we would in most cases like to infer FliesTweety.
We could have an axiom xBirdx Fliesx But what if Tweety is a penguin?
We could tighten the axiom to
xBirdx Penguinx Fliesx
But then if all we know is BirdTweety we cannot make the
inference we wanted.
KRR NonMonotonicReasoning Contents KRR125

The Closed World Assumption
A simple form of nonmonotonic reasoning is to assume that everything that is not provable is false.
So we have an additional inference rule of the form:

KRR NonMonotonicReasoning
Contents KRR126

The Closed World Assumption
A simple form of nonmonotonic reasoning is to assume that everything that is not provable is false.
So we have an additional inference rule of the form:

But this can lead to inconsistency. We generally need the
restriction that must occur in . But we still have problems.
Let p q then neither p or q follow from so from the CWA we can derive p and q. But the formulapqpq is inconsistent.
KRR NonMonotonicReasoning Contents KRR126

Default Logic
Proposed by Ray Reiter in 1980.
This logic is built on propositional or 1storder logic by adding an extra inference mechanism.
KRR NonMonotonicReasoning Contents KRR127

Default Logic
Proposed by Ray Reiter in 1980.
This logic is built on propositional or 1storder logic by adding an extra inference mechanism.
Default Rules are used to specify typical default inferences e.g. Birds typically fly.
We can only make inferences from default rules provided it is consistent to do so.
For example, if Tweety is a bird the by default we can conclude that he flies. If, however, we know that Tweety is a penguin or ostrich etc. the this inference is blocked.
KRR NonMonotonicReasoning Contents KRR127

Default Rules
The general form of a default rule is
: 1,…,n The is often written underneath.
This means: If is true and it is consistent to believe each of the i not necessarily at the same time, then one may infer by default .
KRR NonMonotonicReasoning Contents KRR128

Normal Defaults
A normal default is one where the justification is the same as the conclusion:
E.g. Germanx : DrinksBeerxDrinksBeerx
Thus given Germanmax
we can use this default rule to infer DrinksBeermax unless we can prove DrinksBeermax.
KRR NonMonotonicReasoning Contents KRR129

NonNormal Defaults
The most obvious default rules are the normal ones, where we derive a conclusion as long as that conclusion is consistent.
However, sometimes it is useful to use a justification that is different from the conclusion.
E.g. Adultx : Marriedx Studentx Marriedx
The extra Studentx conjunct in the justification serves to block
the inference when we know that x is a student.
KRR NonMonotonicReasoning Contents KRR1210

Rules with no Prerequisite
By using rules with no prerequisite we can allow normal assumptions to be made where no information is given.
KRR NonMonotonicReasoning Contents KRR1211

Rules with no Prerequisite
By using rules with no prerequisite we can allow normal assumptions to be made where no information is given.
For instance if a scenario description does not mention it is raining we can assume it is not.
A default Sit Calc theory might contain the rule:
: HoldsRaining, s HoldsRaining, s
KRR NonMonotonicReasoning Contents KRR1211

Default Theories
A default theory is a classical theory plus a set of default rules. Thus it can be described by pair:
T , D ,
where T is a set of classical formulae and D a set of default rules.
KRR NonMonotonicReasoning Contents KRR1212

Provability in a Default Theory
Default logics are built on top of classical logics so the notion of classical deduction can be retained in the default logic setting:
Let T mean that is derivable from T by classical monotonic inference.
A na ve nonmonotonic deduction relation can be represented as follows:
Let T D mean that is derivable from T by a combination of classical inference and the application of default rules taken from D.
KRR NonMonotonicReasoning Contents KRR1213

SelfUndermining Inferences
Consider the simple default theory T , D, where: T R, P Q
D R : Q P
KRR NonMonotonicReasoning Contents KRR1214

SelfUndermining Inferences
Consider the simple default theory T , D, where: T R, P Q
D R : Q P
Since Q is consistent with T , we can apply the default rule and derive P . Then by modus ponens we immediately get Q.
But T P now entails Q and is thus inconsistent with the justification Q used in the default rule.
KRR NonMonotonicReasoning Contents KRR1214

WellFounded Default Provability
To get a betterbehaved entailment relation we want to block inferences that undercut the default rules used in their own derivation.
KRR NonMonotonicReasoning Contents KRR1215

WellFounded Default Provability
To get a betterbehaved entailment relation we want to block inferences that undercut the default rules used in their own derivation.
I first define a restricted entailment relation where derivations from T can only use defaults that are also compatible with an additional formula set S
Let T D : S mean that is derivable from T by a combination of classical inference and the application of default rules taken from D and whose justifications are consistent with T S.
KRR NonMonotonicReasoning Contents KRR1215

Extensions of Default Theories
We now characterise sets of selfconsistent inferences from a default theory.
KRR NonMonotonicReasoning Contents KRR1216

Extensions of Default Theories
We now characterise sets of selfconsistent inferences from a default theory.
An extension of T , D is a set of formulae E such that: 1. T E
KRR NonMonotonicReasoning Contents KRR1216

Extensions of Default Theories
We now characterise sets of selfconsistent inferences from a default theory.
An extension of T , D is a set of formulae E such that:
1. T E
2. If E then E deductive closure;
3.IfEand:1,…,n Dandfori1,…,n, i E then E default closure;
KRR NonMonotonicReasoning Contents KRR1216

Conflicting Extensions
Suppose a default theory contains the default rules: 1 : Raining Raining
and
2 WetWashing : Raining Raining;
and also the fact WetWashing.
KRR NonMonotonicReasoning
Contents
KRR1217

Conflicting Extensions
Suppose a default theory contains the default rules: 1 : Raining Raining
and
2 WetWashing : Raining Raining;
and also the fact WetWashing.
We can apply either of the rules. But, once we have applied one,
the justification of the other will be undermined. Thus there are two distinct extensions to the theory.
One containing Raining and the other containing Raining.
KRR NonMonotonicReasoning Contents KRR1217

Validity in Default Logic
Reiter suggested that each extension can be taken as a consistent set of beliefs compatible with a default theory.
In Default Logic the notion of valid inference can be characterised in various different ways. The most common are the following:
Credulous entailment is defined by:
T , D cred
just in case is a member of some extension of T , D.
KRR NonMonotonicReasoning Contents KRR1218

Computational Properties
of Default Reasoning
Adding default reasoning to a logic can greatly increase the complexity of computing inferences.
To apply a rule : we need to check whether is consistent with the rest of the theory.
If the logic is decidable default reasoning will still be decidable although usually more complex.
KRR NonMonotonicReasoning Contents KRR1219

Default Solution of
the Frame Problem in Sit Calc
One solution of the frame problem is to assume that nothing changes unless it is forced to change by some entailment of the theory. This can be expressed in a combination of Situation Calculus and Default Logic as follows:
holds,s: holds,result,sholds,result,s However, we still need to ensure that the background theory we
are using takes care of sementica and and causal relationships.
KRR NonMonotonicReasoning Contents KRR1220

Reading
To get a fuller understanding of default logic, I suggest you read the following paper:
Grigoris Antoniou 1999, A tutorial on default logics, ACM Computing Surveys, 314:337359.
DOI link: http:doi.acm.org10.1145344588.344602
You should be able to download this via the UoL library electronic
resources search for ACM Computing Surveys.
KRR NonMonotonicReasoning Contents KRR1221

KRR NonMonotonicReasoning Contents KRR1222

KRR NonMonotonicReasoning Contents KRR1223

KRR NonMonotonicReasoning Contents KRR1224

KRR NonMonotonicReasoning Contents KRR1225

COMP5450M
Knowledge Representation
KRR DescriptionLogic
Contents KRR131
Lecture KRR13
Description Logic

Motivation
AI knowledge bases often contain a large number of concept definitions, which determine the meaning of a concept in terms of other more primitive concepts.
KRR DescriptionLogic Contents KRR132

Motivation
AI knowledge bases often contain a large number of concept definitions, which determine the meaning of a concept in terms of other more primitive concepts.
Firstorder logic is well suited to representing these concept definitions, but is impractical for actually computing inferences.
We would like a representational formalism which retains enough of the expressive power of 1storder logic to facilitate concept definitions but has better computational properties.
KRR DescriptionLogic Contents KRR132

Relationships Between Concepts
Many types of logical reasoning depend on semantic relationships between concepts.
KRR DescriptionLogic Contents KRR133

Relationships Between Concepts
Many types of logical reasoning depend on semantic relationships between concepts.
For instance, the necessary fact that All dogs are mammals could be represented in 1storder logic as follows:
xDogx Mammalx
Another way of looking at the meaning of this formula is to regard
it as saying that Dog is a subconcept of Mammal.
KRR DescriptionLogic Contents KRR133

Negation, Conjunction and
Disjunction
It is often useful to describe relations between concepts in terms of negation, conjunction and disjunction.
KRR DescriptionLogic Contents KRR134

Negation, Conjunction and Disjunction
It is often useful to describe relations between concepts in terms of negation, conjunction and disjunction.
E.g. in 1storder logic we might write:
xBachelorx Malex Marriedx
In Description Logic we could simply write
Bachelor Male Married
Similarly we might employ a concept disjunction as follows:
Organism Plant Animal
KRR DescriptionLogic
Contents
KRR134

Universal and Null Concepts
For some purposes it is useful to refer to the universal concept , which is satisfied by everying, or the empty concept , which is satisfied by nothing.
KRR DescriptionLogic Contents KRR135

Universal and Null Concepts
For some purposes it is useful to refer to the universal concept , which is satisfied by everying, or the empty concept , which is satisfied by nothing.
For example
KRR DescriptionLogic
Contents KRR135
Plant Animal

Instances of Concepts
In 1storder logic we say that an individual is an instance of a concept by applying a predicate to the name of the individual. e.g. Bachelorfred.
KRR DescriptionLogic Contents KRR136

Instances of Concepts
In 1storder logic we say that an individual is an instance of a concept by applying a predicate to the name of the individual. e.g. Bachelorfred.
In description logic, concepts are just referred to by name and do not behave syntactically like predicates. Hence we introduce a special relation, which takes the place of predication. We write, e.g.:
Fred isa Bachelor
KRR DescriptionLogic
Contents KRR136

Roles
We can also use relational concepts, which in DL are usually called roles.
For example we can write:
Allen haschild Bob
KRR DescriptionLogic
Contents KRR137

Quantifiers
DL also allows limited form of quantification using the following variablefree constructs:
KRR DescriptionLogic Contents KRR138

Quantifiers
DL also allows limited form of quantification using the following variablefree constructs:
r.C
This refers to the concept whose members are all objects, such
that everything they are reletated to by r is a member of C. e.g.
Comedian def Person tellsjoke.Funny
KRR DescriptionLogic Contents KRR138

More Quantifiers
Similarly we have an existential quantifier, such that
r.C
is the concept whose members are all those individuals that are
related to something that is a C.
KRR DescriptionLogic Contents KRR139

More Quantifiers
Similarly we have an existential quantifier, such that
r.C
is the concept whose members are all those individuals that are
related to something that is a C. For example:
Parent haschild.
KRR DescriptionLogic
Contents KRR139

Another Example
We will define the conept of lucky man as a man who has a rich or beautiful wife and all his children are happy.
KRR DescriptionLogic Contents KRR1310

Another Example
Fanatics never respect each other.
KRR DescriptionLogic Contents KRR1311

KRR DescriptionLogic Contents KRR1312

COMP5450M
Knowledge Representation
Lecture KRR14
Propositional Resolution
KRR PropositionalResolution Contents KRR141

Overview
The discovery of the Resolution inference rule was a major breakthrough in automated reasoning.
It is wellsuited to computational implementation and is in most practical cases more efficient at finding proofs than previous systems.
In terms of computational complexity theory, propositional reasoning is NP Complete, however different algorithms certainly differ in their practical efficiency.
KRR PropositionalResolution Contents KRR142

Propositional Resolution
Consider modus ponens , with the implication re written as the equivalent disjunction:
,
KRR PropositionalResolution
Contents KRR143

Propositional Resolution
Consider modus ponens , with the implication re written as the equivalent disjunction:
,
This can be seen as a cancellation of with .
KRR PropositionalResolution Contents KRR143

Propositional Resolution
Consider modus ponens , with the implication re written as the equivalent disjunction:
,
This can be seen as a cancellation of with . More generally we have the rule
,
This is the rule of binary, propositional resolution.
The deduced formula is called the resolvent. KRR PropositionalResolution
Contents
KRR143

Special Cases
As special cases of resolution where one resolvent is not a disjunction we have the following:
, ,
,
KRR PropositionalResolution
Contents KRR144

Special Cases
As special cases of resolution where one resolvent is not a disjunction we have the following:
, ,
,
In the last case an inconsistency has been detected.
KRR PropositionalResolution
Contents
KRR144

Conjunctive Normal Form CNF
A literal is either an atomic proposition or the negation of an atomic proposition.
KRR PropositionalResolution Contents KRR145

Conjunctive Normal Form CNF
A literal is either an atomic proposition or the negation of an atomic proposition.
A clause is a disjunction of literals.
A CNF formula is a conjunction of clauses.
Thus a CNF formula takes the form:
p01 … p0m0 q01 … q0n0 p11 … p1m1 q11 … q1n1
::
pk1 … pkmk qk1 … qknk KRR PropositionalResolution
Contents
KRR145

Set Representation of CNF
A conjunction of formulae can be represented by the set of its conjuncts.
Similarly a disjunction of literals can be represented by the set of those literals.
Thus a CNF formula can be represented as a set of sets of literals. E.g.:
represents
p, q, r, s, t, u, v p q r s t u v
KRR PropositionalResolution Contents KRR146

Conversion to
Conjunctive Normal Form
Any propositional formula can be converted to CNF by repeatedly applying the following equivalence transforms, wherever the left hand pattern matches some subformula.
KRR PropositionalResolution Contents KRR147

KRR PropositionalResolution Contents KRR147

Move negations inwards:

Double Negation Elimination De Morgan
De Morgan
KRR PropositionalResolution
Contents
KRR147

Conversion to Conjunctive Normal Form
Any propositional formula can be converted to CNF by repeatedly applying the following equivalence transforms, wherever the left hand pattern matches some subformula.
Rewrite :

Move negations inwards:

Double Negation Elimination De Morgan
De Morgan
Distribute over :

KRR PropositionalResolution Contents KRR147

Complete Consistency Checking for CNF
The resolution inference rule is refutation complete for any set of clauses.
KRR PropositionalResolution Contents KRR148

Complete Consistency Checking for CNF
The resolution inference rule is refutation complete for any set of clauses.
This means that if the set is inconsistent there is a sequence of resolution inferences culminating in an inference of the form p, p , which demonstrates this inconsistency.
If the set is consistent, repeated application of these rules to derive new clauses will eventually lead to a state where no new clauses can be derived.
KRR PropositionalResolution Contents KRR148

Duplicate Factoring for Clausal Formulae
If we represent a clause as disjunctive formula rather than a set of literals, there is an additional rule that must be used as well as resolution to provide a complete consistency checking procedure.
Suppose we have: p p, p p. The only resolvent of these clauses is p p. And by further resolutions we cannot derive anything but these three formulae.
KRR PropositionalResolution Contents KRR149

With the set representation, this rule is not required since by definition a set cannot have duplicate elements so factoring is implicit.
KRR PropositionalResolution Contents KRR149

Giving a Resolution Proof
In the propositional case, it is quite easy to carry out resolution proofs by hand. For example:
A,B,C, A,D, B,E, C,ED,AE
KRR PropositionalResolution Contents KRR1410

Giving a Resolution Proof
In the propositional case, it is quite easy to carry out resolution proofs by hand. For example:
A,B,C, A,D, B,E, C,ED,AE Enumerate the clauses: Apply resolution rules:
1. A,B,C 7.
2. A, D 8.
3. B,E 9.
4. C,E 10.
5. D, A 11.
6. E
12.
Bfrom36
Cfrom46
A,C from 1 7
Afrom89
Afrom25 duplicate A deleted
from1011
KRR PropositionalResolution
Contents KRR1410

COMP5450M
Knowledge Representation
Lecture KRR15
FirstOrder Resolution
KRR FirstOrderResolution Contents KRR151

1storder Automated Reasoning
We have seen that 1storder reasoning is in general undecidable or more precisely semidecidable.
KRR FirstOrderResolution Contents KRR152

1storder Automated Reasoning
We have seen that 1storder reasoning is in general undecidable or more precisely semidecidable.
Nevertheless massive effort has been spent on developing inference procedures for 1storder logic.
Thisisbecause1storderlogicisaveryexpressiveandflexible language.
KRR FirstOrderResolution Contents KRR152

Resolution in 1storder Logic
Consider the following argument:
DogFido, xDogx Mammalx MammalFido
KRR FirstOrderResolution Contents KRR153

Resolution in 1storder Logic
Consider the following argument:
DogFido, xDogx Mammalx MammalFido Writing the implication as a quantified clause we have:
DogFido, xDogx Mammalx MammalFido If we instantiate x with Fido this is a resolution:
DogFido, DogFido MammalFido MammalFido
KRR FirstOrderResolution Contents KRR153

Resolution without Instantiation
Resolution does not always involve instantiation. In many cases one can derive a universal consequence.
Consider the argument:
xDogx Mammalx xMammalx Animalx xDogx Animalx
Which is equivalent to :
xDogx Mammalx xMammalx Animalx xDogx Animalx
KRR FirstOrderResolution Contents KRR154

1storder Clausal Form
To use resolution as a general 1storder inference rule we have to convert 1storder formulae into a clausal form similar to propositional CNF.
KRR FirstOrderResolution Contents KRR155

1storder Clausal Form
To use resolution as a general 1storder inference rule we have to convert 1storder formulae into a clausal form similar to propositional CNF.
To do this we carry out the following sequence of transforms:
1. Eliminate and using the usual equivalences.
2. Move inwards using the equivalences used for CNF plus: x x
x x
KRR FirstOrderResolution
Contents KRR155

4. Eliminate existential quantifiers using the Skolemisation transform described later.
KRR FirstOrderResolution Contents KRR156

4. Eliminate existential quantifiers using the Skolemisation transform described later.
5. Move universal quantifiers to the left.
KRR FirstOrderResolution Contents KRR156

4. Eliminate existential quantifiers using the Skolemisation transform described later.
5. Move universal quantifiers to the left.
This is justified by the equivalences
x x x x,
which hold on condition that does not contain the variable x.
6. Transform the matrix i.e. the part of the formula following the quantifiers into CNF using the transformations given above. Any duplicate literals in the resulting disjunctions can be deleted.
KRR FirstOrderResolution Contents KRR156

Skolemisation
Skolemisation is a transformation whereby existential quantifiers are replaced by constants andor function symbols.
KRR FirstOrderResolution Contents KRR157

Skolemisation
Skolemisation is a transformation whereby existential quantifiers are replaced by constants andor function symbols.
Skolemisation does not produce a logically equivalent formula but it does preserve consistency.
If we have a formula set xx then this will be consistent just in case is consistent, where is a new arbitrary constant that does not occur in or in .
Consistency is also preserved by such an instantiation in the case when xx is embedded within arbitrary conjunctions and disjunctions but not negations. This is because the quantifier could be moved outwards accross these connectives.
KRR FirstOrderResolution Contents KRR157

Existentials within Universals
How does Skolemisation interact with universal quantification. Consider 1 xyLovesx, y Lovesx, x
How does this compare with 2 xLovesx, Lovesx, x From2wecaninfer Loves,Loves,
But this inconsistency does not follow from 1.
From 1 we can get yLoves, y Loves,
KRR FirstOrderResolution
Contents KRR158

Skolem Functions
To avoid this problem Skolem constants for existentials lying within the scope of universal quantifiers must be made to somehow vary according to possible choices for instantiations of those universals.
How can we describe something whose denotation varies depending on the value of some other variable??
By a function.
Hence Skolemisation of existentials within universals is handled by the transform:
x1 …xn…yy x1 …xn…fx1,…,xn , where f is a new arbitrary function symbol.
KRR FirstOrderResolution Contents KRR159

1storder Clausal Formulae
A 1storder clausal formula is a disjunction of literals which may contain variables andor Skolem constantsfunctions as well as ordinary constants.
KRR FirstOrderResolution Contents KRR1510

1storder Clausal Formulae
A 1storder clausal formula is a disjunction of literals which may contain variables andor Skolem constantsfunctions as well as ordinary constants.
All variables in a clause are universally quantified. Thus, provided we know which symbols are variables, we can omit the quantifiers. I shall use capital letters for the variables like Prolog.
Example clauses are:
Ga, HX,YJb,Y, PgXQX, RX, Y SfX, Y
KRR FirstOrderResolution Contents KRR1510

Unification
Given two or more terms i.e. functional expressions, Unification is the problem of finding a substitution for the variables in those terms so that the terms become identical.
A substitution my replace a variable with a constant e.g. X c or functional term e.g. X fa or with a another variable e.g. XY
KRR FirstOrderResolution Contents KRR1511

Instances and Most General Unifiers
The result of applying a set of substitutions to a formula is denoted and is called an instance or instantiation of .
If is a unifier for and then we have . There may be other unifiers , such that .
If for all unifiers we have is an instance of , then is called a most general unifier or m.g.u for and .
An m.g.u. instantiates variables only where necessary to get a match.
If mgu but also then there must be some substitution such that
M.g.u.s are unique modulo renaming variables.
KRR FirstOrderResolution Contents KRR1512

An Algorithm for Computing Unifiers
There are many algorithms for computing unifiers. This is a simple rewriting algorithm.
To compute the m.g.u. of a set of expressions 1, . . . , n Let S be the set of equations 1 2,…,n1 n
We then repeatedly apply the rewrite and elimination rules given on the next slide to any suitable elements of S.
KRR FirstOrderResolution Contents KRR1513

1. Identity Elimination: remove equations of the form .
KRR FirstOrderResolution Contents KRR1514

1. Identity Elimination: remove equations of the form . 2. Decomposition:
1,…,n 1,…,n 1 1,…n n.
KRR FirstOrderResolution Contents KRR1514

1. Identity Elimination: remove equations of the form .
2. Decomposition:
1,…,n 1,…,n 1 1,…n n.
3. Match failure: or … …, where and are distinct constants or function symbols. There is no unifier.
.
4. Occurs Check failure: X . . . X . . .. X cannot be equal
to a term containing X. No unifier.
5. Substitution: Unless occurs check fails, replace an equation of the form X or X by X and apply the substitution X to all other equations in S.
KRR FirstOrderResolution Contents KRR1514

with a substitution that is a unifier for all the original set of terms.
KRR FirstOrderResolution Contents KRR1515

Unification Examples
Terms
Rg,Y FY PY,fa
RX,a FX PX,a
Unifier
Xg, Ya XY or Y X none a fa Zfa, Xffa Xa, Za
none Xga,Y.
none occurs check failure.
TX,fa TfZ,Z TX,a TZ,Z
RX, X Ra, b FX Fga,Y F X F ga, X
KRR FirstOrderResolution
Contents KRR1516

1storder Binary Resolution
1storder resolution is acheived by first instantiating two clauses so that they contain complementary literals. Then an inference that is essentially the same as propositional resolution can be applied.
So, to carry out resolution on 1storder clauses and we look for complementary literals and . Such that and are unifiable.
We apply the unifier to each of the clauses.
Then we can simply cancel the complementary literals and collect the remaining literals from both clauses to form the resolvent.
We also need to avoid problems due to shared variables. See next slide.
KRR FirstOrderResolution Contents KRR1517

1storder Binary Resolution Rule Formalised
To apply resolution to clauses and :
Let be a clause obtained by renaming variables in so that
and do not share any variables.
KRR FirstOrderResolution Contents KRR1518

1storder Binary Resolution Rule Formalised
To apply resolution to clauses and :
Let be a clause obtained by renaming variables in so that
and do not share any variables.
Suppose ,1,…n and ,1,…n If and are unifiable a resolution can be derived.
KRR FirstOrderResolution Contents KRR1518

Resolution Examples
ResolvePX, RX,aandQY,Z, RZ,Y
KRR FirstOrderResolution Contents KRR1519

Resolution Examples
ResolvePX, RX,aandQY,Z, RZ,Y mguRX, a, RZ, Y XZ, Y a
KRR FirstOrderResolution Contents KRR1519

Resolution Examples
ResolvePX, RX,aandQY,Z, RZ,Y mguRX, a, RZ, Y XZ, Y a Resolvent: PZ, Qa,Z
KRR FirstOrderResolution Contents KRR1519

Resolution Examples
ResolvePX, RX,aandQY,Z, RZ,Y mguRX, a, RZ, Y XZ, Y a Resolvent: PZ, Qa,Z
ResolveAa,X, HX,Y, GfX,Yand
Hc,Y, GfY,gY
KRR FirstOrderResolution Contents KRR1519

Resolution Examples
ResolvePX, RX,aandQY,Z, RZ,Y mguRX, a, RZ, Y XZ, Y a Resolvent: PZ, Qa,Z
ResolveAa,X, HX,Y, GfX,Yand
Hc,Y, GfY,gY
Rename variables in 2nd clause: Hc, Z, GfZ, gZ mguGfX,Y, GfZ,gZXZ, YgZ
KRR FirstOrderResolution Contents KRR1519

Factoring
for Refutation Compleness
Resolution by itself is not refutation complete. We need to combine it with one other rule.
This is the factoring rule, which is the 1storder equivalent of the deletion of identical literals in the propositional case.
The rule is: 1,2,1,…,n ,1,…,n
where 1 and 2 have the same sign both positive or both negated and are unifiable and have as their m.g.u..
The combination of binary resolution and factoring inferences is refutation complete for clausal form 1storder logic i.e. from any inconsistent set of clauses these rules will eventually derive the empty clause.
KRR FirstOrderResolution Contents KRR1520

COMP5450M
Knowledge Representation
Lecture KRR16
Compositional Reasoning
KRR CompositionalReasoning Contents KRR161

Compositional Reasoning
Given relations Ra,b and Sb,c, we may wish to know the relation between a and c.
Often this relation is constrained by the meanings of R and S.
KRR CompositionalReasoning Contents KRR162

Compositional Reasoning
Given relations Ra,b and Sb,c, we may wish to know the relation between a and c.
Often this relation is constrained by the meanings of R and S. For instance among the Allen relations we have:
Duringa, b Beforeb, c Beforea, c
The composition of relations R and S is often written as R; S. We can define: R; Sx, y def zRx, z Sz, y
KRR CompositionalReasoning
Contents KRR162

Disjunctive Compositions
Sometimes the composition of Ra,b and Sb,c allows for a number of qualitatively different possibilities for the relation T a, c
For instance consider the case where we know Duringb, r and Ended byr,g
There are 5 possible Allen relations between b and g.
KRR CompositionalReasoning Contents KRR163

Relational Partitions
In several important domains of knowledge, sets of fundamental relations R R1, . . . , Rn have been found which are:
Mutually Exhaustive all pairs of objects in the domain are related by some relation in R.
Pairwise Disjoint no two objects in the domain are related by more than one relation in R.
Hence every pair of objects in the domain is related by exactly one relation in R.
I shall call such a set a Relational Partition.
KRR CompositionalReasoning Contents KRR164

The RCC5 Relational Partition
In the domain of spatial relations there is a very general relational partition known as RCC5 consisting of the following relations:
This partition ignores the difference between regions touching at a boundary, which is made in RCC8.
KRR CompositionalReasoning Contents KRR165

Inverse and Disjunctive Relations
The inverse of a relation is defined by
Rx, y def Ry, x
KRR CompositionalReasoning
Contents KRR166

Inverse and Disjunctive Relations
The inverse of a relation is defined by
Rx, y def Ry, x
It will be useful to have a notation for a relation which is the
disjunction of several other relations.
I shall use the notation R1, . . . , Rn, where
R1,…,Rnx,y def R1x,y … Rnx,y For uniformity Rx, y can also be written as Rx, y.
Given a set of relations R, the set of all disjunctive relations formed from those in R will be denoted by R
KRR CompositionalReasoning Contents KRR166

Inverses and Disjunctive Relations in RCC5
In RCC5 each of the relations DR, PO, and EQ are symmetric and thus are their own inverses.
PPi is the inverse of PP and vice versa.
We can form arbitrary disjunctions of any of the relations.
However the following disjunctions are particularly significant: P PP, EQ part
Pi PPi, EQ part inverse
O PO, PP, PPi, EQ overlap
KRR CompositionalReasoning
Contents KRR167

Relation Algebras
A Relation Algebra is a set of relations RA that is closed under: negation, disjunction, inverse and composition.
i.e. R1,…,RnRAwehave
KRR CompositionalReasoning
Contents KRR168
R1, R1,…,Rn, R1
, R1;R2 RA

Relation Algebras
A Relation Algebra is a set of relations RA that is closed under: negation, disjunction, inverse and composition.
i.e. R1,…,RnRAwehave
R1, R1,…,Rn, R1 , R1;R2 RA
If R is a finite Relational Partition and R is closed under composition then R is a finite Relation Algebra; and R is a basis for that algebra.
Relation Algebras generated from a finite basis in this way have a nice computational property:
Every composition is equivalent to a disjunction of basis relations.
KRR CompositionalReasoning Contents KRR168

Composition Tables
If R is closed under composition then for every pair of relations R1, R2 R we can express their composition as a disjunction of relations in R.
KRR CompositionalReasoning Contents KRR169

Composition Tables
If R is closed under composition then for every pair of relations R1, R2 R we can express their composition as a disjunction of relations in R.
The compositions can then be recorded in a Composition Table, which allows immediate lookup of any composition.
KRR CompositionalReasoning Contents KRR169

The RCC5 Composition Table
For RCC5 we have the following table:
r r
r r
r r
r Ra,b r
r r
Rb, c r
DR
PO
EQ
PP
PPi
DR
all poss
DR, PO, PP
DR
DR, PO, PP
DR
PO
DR, PO, PPi
all poss
PO
PO, PP
DR, PO, PPi
EQ
DR
PO
EQ
PP
PPi
PP
DR
DR, PO, PP
PP
PP
all poss
PPi
DR, PO, PPi
PO, PPi
PPi
O
PPi
KRR CompositionalReasoning Contents KRR1610

Composing Disjunctive Relations
In general we may want to compose two disjunctive relations.
R1,… Rm;S1,…,Sn Ri ; Sj i1…m, j1…n
Thus to compose a disjunction we:
first find the compositions of each disjunct of the first relation with each disjunct of the second relations;
then, form the disjunction of all these compositions.
KRR CompositionalReasoning Contents KRR1611

Compositional Path Consistency
When working with a set of facts involving relations that form an RA we can use compositions as a powerful reasoning mechanism.
Wherever we have facts R1a, b and R2b, c in a logical database, we can use a composition table to look up and add some relation R3a, c.
Where we already have information about the relation between a and c, we need to combine it with the new R3 using the general equivalence:
…,Ri,…x,y …,Si,…x,y …,Ri,……,Si,…x,y
KRR CompositionalReasoning Contents KRR1612

Compositional Completion
The rule for combining a compositional inference with existing information can be formally stated as:
Rx,y,Sy,z,Tx,z R;STx,z
If using this rule we find that R;S T we have found an
inconsistency.
Where T R;S, we will have R;S T T so the inference
derives no new information.
KRR CompositionalReasoning Contents KRR1613

Relational Consistency Checking
Algorithm
To check consistency of a set of relational facts where the relations form an RA, we repeatedly apply the compositional inference rule until either:
wefindaninconsistency;
wecanderivenonewinformationfromany3relationalfacts.
If we are dealing with an RA over a finite relational partition then this procedure must terminate.
This gives us a decision procedure which runs in n3 time, where n is the number of objects involved.
KRR CompositionalReasoning Contents KRR1614

COMP5450M
Knowledge Representation
KRR Uncertainty
Contents KRR171
Lecture KRR17
Uncertainty

Overview
KRR Uncertainty Contents KRR172

COMP5450M
Knowledge Representation
KRR Vagueness
Contents KRR181
Lecture KRR18
Vagueness

Overview
KRR Vagueness Contents KRR182

COMP5450M
Knowledge Representation
Lecture KRR19
Ontology and Ontologies
KRR OntologyandOntologies Contents KRR191

Overview
KRR OntologyandOntologies Contents KRR192

Related Posts