1. Introduction and JUnit
First Order Logic
1
8/31/21
1
Learning Objectives
Differentiate among various logics
Express first order logic (FOL) expressions
Differentiate syntax vs. semantics of FOL
Assess challenges of inference
2
Agenda: First Order Logic
3
Logics
Syntax of First Order Logic
Semantics of FOL
Inference
Various Logics
4
Russell & Norvig
Example:
p = A helicopter has flown on logic is the simplest. It states facts—statements with one of three values: True, False, and Unknown (or “Neither”).
Despite its simplicity, this introduces an AI concept that is sometimes used: the Closed World Assumption, which states that if a statement is unknown, then it is assumed to be false.
4
Various Logics
5
Russell & Norvig
The most common logic is First-order logic, in which we reason at the lowest meaningful level. Temporal logic accounts for time, as in I used to distrust every authority and I have recently changed my attitude towards authority—from which we can conclude I don’t distrust every authority. We will discuss fuzzy logic later in this module.
5
Agenda: First Order Logic
6
Logics
Syntax of First Order Logic
Semantics of FOL
Inference
First Order Logic is the simplest level of logic that allows reasoning. First we discuss its syntax.
Elements of FOL
7
Constants JaneRMuldoon7, Denver, 345643, …
Predicates IsProgrammer(), LivesInBoston(), …
Variables x, y, …
Connectives , , … is and; is or; is not
Equality = means is equivalent to
Quantifiers , , … is for every; is there exists
FOL is a symbolic system that mirrors aspects of the real world. It consists of the symbols shown. Predicates take on the values true or false. They may have parameters. Think of them as you would in conversation rather than as in a programming language; for example you might say I’m at the beach (which is either true or false) or AtBeach(), a predicate with parameter—so AtBeach(Eric) is again true or false.
7
Example
8
English:
“Not every Amazon customer has written a review”
FOL:
x [Customer(x, Amazon)
…
A predicate with 2 parameters
The figure shows the beginning of a FOL representation of a real-world predicate (a statement with true/false value). It says something exists which is a customer of Amazon and … .
There may be several ways to say the same thing, such as ACustomer(y, AmazonCo) … but the important thing is to be consistent.
8
Example
9
English:
“Not every Amazon customer has written a review”
FOL:
x [ [Customer(x, Amazon)
[p SoldBy(p, Amazon): ! HasReviewed(x, p)]
“such that”
This completes the FOL representation as an x exists which is an Amazon customer and which is such that, for every p sold by Amazon, x has not reviewed p.
9
Syntax of First Order Logic
10
Russell & Norvig
The figure begins to specify the form of FOL statements (“sentences”). It says that “every FOL sentence is either an AtomicSentence or a ComplexSentence; AtomicSentence’s are ether …”
10
Syntax of First Order Logic
11
Russell & Norvig
The figure shows the entire syntax (although there are variations). The success of FOL in accomplishing useful tasks is analogous to that of mathematics, and the types of logics are analogous to the types of mathematics.
11
Example
12
¬Brother(Tom,John)
Brother(Richard,John) ∧ Brother(John,Richard)
King(Richard) ∨ King(John)
¬King(Richard) ⇒ King(John)
Russell & Norvig
The first example in the figure says that Tomis not John’s brother. This assumes that we interpret the predicates in the self-evident manner. For example, in FOL, “Brother” is just a string: it is up to us to interpret it in the real world. We do in a consistent manner, throughout the problem we are dealing with.
12
More Realistic Example
13
Next step in my continuing education.
Constants BU, Northeastern, Harvard, JohnDoe …
Predicates LikesTo(…), Pays(…), Advancement(…)
Variables student, job, university, program, …
Rules (using quantifiers etc.) …
Procedure: Plug in a “world” (set of values)
Logic is applicable to a very wide range of problems, such as the one in the figure.
13
Some Relationships Between and
14
Russell & Norvig
There is an algebra (set of rules for FOL), which includes the above, and which reflect the real world. For example, at the bottom left, saying
some x satisfies property P
is the same as saying
it is not true that (every x satisfies P false).
14
Agenda: First Order Logic
15
Logics
Syntax of First Order Logic
Semantics of FOL
Inference
Models
16
Each “model” links the vocabulary of the logical sentences to elements of the possible world.
The domain of a model is the set of objects or domain elements it contains.
Adapted from Russell & Norvig p290
Models are the link between (the symbolic) FOL and the situation (the possible “world”) that you want to apply it to.
16
Semantics of FOL
17
Predicates are true or false in a world (“model”).
e.g., FOL:
x [Customer(x, y)
[y, p [HasReviewed(x, p) SoldBy(p, y)]]
–is true in the world where y is Amazon or WalMart
Toy Agent and FOL: WumpusWorld (R&N)
18
Can we express rules in FOL?
Russell & Norvig
To exercise first order logic, Russell and Norvig developed a simplified world in which an agent moves so as to land on gold. The agent uses FOL to make decisions about movement. AI is needed when movements are not deterministic (e.g., always continue the direction you were following).
There is a stationary, agent-destroying wumpus. Its stench can be sensed immediately to its north, south, east and west. There is an unknown number of “pits”, which emit a breeze similarly.
We’ll express the WumpusWorld rules in FOL.
18
WupusWorld Rules ( )
19
First, we’ll use propositional logic (not FOL).
Rule R1 means, for example,
If there is no stench in cell (1,1), then the Wumpus is not in cells (1,1), (1,2), or (2,1).
19
Application of FOL to Programming: Dafny
20
AUTOMATICALLY VERIFYING SOURCE CODE
method MultipleReturns(x: int, y: int) returns (more: int, less: int)
requires 0 < y
ensures less < x < more
{
…
}
https://rise4fun.com/dafny/tutorialcontent/guide
FOL is being applied in to many domains. One is to programming itself—to verify that function code is correct. This is the field of program correctness, whose importance is recognized every time a company like Boeing loses billions due to incorrect programs.
To carry this out, the preconditions (“requires”) and postconditions (“ensures”) must be precisely specified in FOL, using Dafny syntax.
20
Application of FOL to Programming: Dafny
21
AUTOMATICALLY VERIFYING SOURCE CODE
method MultipleReturns(x: int, y: int) returns (more: int, less: int)
requires 0 < y
ensures less < x < more
{
more := x + y;
less := x - y;
}
https://rise4fun.com/dafny/tutorialcontent/guide
The figure shows a code example that can be submitted to Dafny.
21
Quantifiers … What does this express?
22
https://rise4fun.com/dafny/tutorialcontent/guide
method Find(a: array
ensures 0 <= index ==> index < a.Length && a[index] == key ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key
{
….
}
The figure specifies a “find in an array” function. The second ensures specifies that a negative value of index is returned if key is not present in a.
22
What is this Saying … ?
23
https://rise4fun.com/dafny/tutorialcontent/guide
method Find(a: array
ensures 0 <= index ==> index < a.Length && a[index] == key
ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key
{
index := 0;
while index < a.Length
invariant 0 <= index <= a.Length
invariant forall k :: 0 <= k < index ==> a[k] != key
{
if a[index] == key { return; }
index := index + 1;
}
index := -1;
}
Dafny is not completely hands-off: it requires an invariant for every loop: predicates stating what each iteration of the loop does not change. The while loop shown in the figure has two invariants.
23
Expressing Predicates in Dafny
24
https://rise4fun.com/Dafny/SKw6
It is possible to name predicats in Dafny (such as sorted) and then refer to them (such as in method Demo).
24
Agenda: First Order Logic
25
Logics
Syntax of First Order Logic
Semantics of FOL
Inference
Everything Non-imply-able Must Be Supplied
26
Russell & Norvig
Everything in a FOL system that does not follow from a set of existing propositions must be supplied. This can be laborious, as we have seen in Dafny, but the idea is to supply it once and use many times.
26
Selected FOL Statements
27
A FOL system must be provided with a basis for operation. The figure shows selected FOL statements that we would have to provide to WumpusWorld (more later):
the definitions of the Adjacent predicate,
“objects can only be at one location at a time,” and
“a breeze is experiences at a cell if, and only if it is adjacent to a cell containing a pit.”
27
Everything Non-imply-able To Be Supplied
e.g., WumpusWorld
28
Russell & Norvig
The figure shown additional statements, including one about arrows(?) Two issues appear (1) when do we have enough? And (2) can contradictory facts be deduced? These are the kinds of theoretical questions that mathematical logic investigatges.
28
Applying Quantifiers: Unification
29
Russell & Norvig
The UNIFY quantifier in logic creates all solutions to a subset of propositions, within a set of propositions. The result of the first unification is (trivially) x = Jane. The solution to the third is y = John and x = the Mother of John. There is no solution to the fourth.
29
Prolog Logic Programming
30
https://www.matchilling.com/introduction-to-logic-programming-with-prolog/
The Prolog (“programming in Logic”) language was developed decades ago as a programming language based on first-order logic. It has been used, especially in Europe, as an AI language, and even as a general purpose language.
In the example shown, :- means “is implied by” or .
The last line is a query: asking for solutions to a statement based on a set of FOL statements.
30
Prolog Examples
31
likes(mary,food). likes(mary,wine). likes(john,wine). likes(john,mary).
The following queries yield the specified answers.
| ?- likes(mary,food). yes.
| ?- likes(john,wine). yes.
| ?- likes(john,food). no.
John likes anything that Mary likes
John likes anyone who likes wine
John likes anyone who likes themselves
http://www.cs.toronto.edu/~sheila/384/w11/simple-prolog-examples.html
The figure shows a set of propositions (using the propositional subset of Prolog).
The second paragfraph shown three queries.
The last paragraph shows what Prolog is capable of doing, even with this small set of statements.
31
More Prolog https://swish.swi-prolog.org/
32
There are many prolog systems, some cloud-based as shown in the figure.
Here is an interesting nontrivial example:
https://swish.swi-prolog.org/example/houses_puzzle.pl
32
Color Europe
33
Prolog is good at constraint-base search. For example, it can be used to color maps (i.e., such that adjacent countries are colored differently). Prolog does its best but is potentially inefficient.
33
Example of desired output: ?- colour_countries(Map).
Map = [austria/yellow, belgium/purple, bulgaria/yellow, croatia/yellow, cyprus/yellow, czech_republic/purple, denmark/yellow, estonia/red, finland/yellow, france/yellow, germany/red, greece/green, hungary/red, ireland/yellow, italy/red, latvia/green, luxemburg/green, malta/green, netherlands/yellow, poland/yellow, portugal/yellow, romania/green, slovakia/green, slovenia/green, spain/green, sweden/green, united_kingdom/green]
Prolog Example: Map Coloring
https://www.matchilling.com/introduction-to-logic-programming-with-prolog/
https://swish.swi-prolog.org/p/Map%20Coloring%20from%20Web.pl
The figure shows a start to the coloring implementation and a reference if you are interested.
34
FOL In Program Construction
35
R
E
You can use Dafny to check your FOL alone (i.e., with no programming involved). For example, if you want to verify the that the statements marked R in the figure imply the statements marked E, then you can ask, in effect, if I execute no code, do the postconditions follow from the preconditions?
35
Summary
First order logic often captures essentials
Syntax: universal
Semantics: link to real world
Inference mechanics has advanced
36
We have seen that first-order logic captures the kind of reasoning we normally think of. Logic engines have become increasingly efficient.
36
/docProps/thumbnail.jpeg