CSE 150 - Week 8 Discussion Notes

CSE 150 – Introduction to Artificial Intelligence
Week 8 –Discussion Notes: FO Logic
November 17, 2004

Outline:
1) Assignment 2 Feedback
2) First-Order Logic Introduction
3) Otter: Getting Started

1) Assignment 2 Feedback

Here are the statistics and grade histogram for assignment 2

Assignment 2 Grade Distribution

:

General Comments:

1) Improvement:
    The content in the reports, the design of the code, and the performance on test cases was signficantly improved from Assignment 1. I feel as though both assignment were equally as difficult. Nice work.

2) Always start with and Introduction.
    Many reports began with sections like "Implementation Details" or "Design of Code". You MUST start your report with an introduction that address the problem that you are addressing. For example, you were testing to see if 3-CNF boolean formula were in the language of 3 SAT. You took two approachs: DPLL and WalkSat...

3) Histograms and XY scatterplot are very different.
     Many of you submitted XY scatterplot rather than histograms. The XY-scatter plot would usually plot something like runtime vs. # number of flips, or runtime vs. search tree size. These scatterplots were not very descriptive for this particular problem. That is, it is not surprising that runtime increased linearly with the # of flip when running the WalkSat algorithm. You need to use HISTOGRAM where the x-axis are bins (ranges of numbers) and the y axis is the number of times your data points fall into each bin. An example is your grade distribution histogram shown above.

4) 3-CNF and 3-SAT
    In a couple of reports, '3-CNF' and '3-SAT' was the source of some confusion. 3-CNF is a language which is defined as the set of boolean forumla that are a conjunction of disjunctions where each disjunction has at most 3 literals. '3-SAT' is also a language and is defined as the set of boolean formulas that are in 3-CNF AND have a satisfying assignment. The problem we were addressing was determing whether a 3-CNF fromula was in 3-SAT.

5) Java was too slow for DPLL.
    There was only one group that could solve 100-Variable 3-CNF problems is a reasonable amount of time. Many of the C implementations ran in less than 5 seconds.

2) First-Order Logic Introduction

This week in discussion, we cover First Order Logic. This is the final topic of the course and is the focus of Assignment 4. AIMA does a reasonable job of introducing the concepts in section 8.2. Figure 8.3 on page 247 gives the syntax (BNF) for FO-logic. The BNF form is useful once you have a basic understanding of the logic. However, working through examples seems to be the best way to comprehend the concepts of FO logic. Kristin Branson's Section 5 Notes is a very good reference and include two-examples: midterm, and Animal Taxonomy. These notes were passed out and covered in this week's discussion section.

Comparing First-Order Logic to Zero-Order Logic.

In assignment 2, we work on Boolean Logic (aka Propositional Logic) which is also call Zero-Order logic. First Order Logic is an extention of Zero-Order logic. The difference are that FO logice has:
1) Constant-Symbols - There are specific objects like Professor Elkan, the color Orange, or the numbers 0 or 1. (Note that in ZO logic, 0 and 1 are the only constant symbols. There semantic meaning translates to True and False.)
2) Predicates - a procedure that maps term(s) to True/False. For example, the likesBlue(.) returns true if the argument likes blue. That is likesBlue(Professor Elkan) ->True
3) Functions - a procedure that maps teerm(s) to a term. For example, colorShirt(.) returns the color of the shirt. That is colorShirt(Professor Elkan) -> Green
4) Quantifiers - There are two quantifiers: 'For All' -denoted by an upside down A, and 'There Exist', denoted by a backwards E.
                      - Quanifier relate to a set of variables.
                      - The 'For All' quanifier usual appears with implication ( For All x P1(x) -> P2(x), where P1 and P2 are predicates)
                        - The 'There Exist' quanifier usually appears with conjunction ( There Exists x such that P1(x) and P2(x), where a and b are predicates.)
                         - Note that the quantifier are related through the following relationship:
                                        * For All x ¬P(x) = ¬There exists x P(x)
                                        * ¬For All x P(x) = There exists x ¬P(x)
                                        * See page 252 in AIMI for more details.

The best way to understand FO Logic and how quantifiers work is to go through an example. Suppose we have the predicated loves(x,y). The semantic meaning is 'if x loves y, then return true, otherwise return false. Note the x and y are variables that instance of individual people in the world. What do the following mean?:

	Syntax			Semantic Meaning
1	For All x,	For all y	loves(x,y)	Everybody loves everybody
2	There Exists x	There Exists y	loves(x,y)	At least one person loves at least one other person.
3	For All x,	There Exists y	loves(x,y)	Everybody loves at least one other person
4	For All y,	There Exists x	loves(x,y)	Everybody has at least one person who loves them
5	There Exists x	For all y	loves(x,y)	There exist somebody who loves everyone.
6	There Exists y	For all x	loves(x,y)	There exist somebody who is loved by everyone

Things to note:
A) In Cases 1 and 2, the order of the quantifer does not matter. This is true when we are using the same quantifier.
B) Case 3,4,5,6, the order of the quantifiers and the order of the variables in the predicate determines the semantic meaning.
C) In all cases, we assume that the object x is not the same object as y.

3) Otter: Getting Started

For Assignment 4, we will be using a programming languaged called OTTER. It is one of many "theorem-proving" programming languages that uses deduction based on user-specified axioms (logic rules) to answer queries (logic questions).

Otter has been installed in ieng9, but you may want to install a copy (Windows/Unix) on your own machine.

To run a simple test file on ieng9, follow these instructions:

----------------------------------------------------------------

To use OTTER, you will need to add link to you PATH environmental variable. This can be done by either:

 1) typing 'prep cs150f' at your command prompt.
 2) typing 'setenv PATH /home/solaris/ieng9/cs150f/otter/otter-3.3f/bin:$PATH' each time 
you login.

All these commands do is to tell your computer where to look to find the 'otter' executible. 

To test that this works on a simple test file, type:

% otter < /home/solaris/ieng9/cs150f/otter/Rabbit1.in

This will print the output of the program to standard output. If you wish pipe the output to a file, type

% otter < /home/solaris/ieng9/cs150f/otter/Rabbit1.in > Rabbit1.out

----------------------------------------------------------------

The file 'Rabbit1.out' is:

-------------------------------------------
%header syntax
set(auto).
formula_list(usable).

%The body of the code:

%Unique Names Assumption 
all x (x=x).

%content
Rabbit(MrsRabbit).
-Rabbit(MrMacGregor).
MrMacGregor = MrsRabbit.

%footer syntax
end_of_list.

---------------------------------------------------------

This was a very difficult assignment for the student last year. Starting early will help. At a bare minimum, you should make sure that you can run this very simple otter code.