Prolog

http://ubuntuforums.org/showthread.php?t=159367

$ apt-cache search prolog

http://www.cs.bris.ac.uk/Teaching/Resources/COMS30106/labs/tracer.html

----- start my-prog.pl -----
link(a,b).
link(c,d).
link(b,c).
path(X,Z) :- link(X,Z).
path(X,Z) :- link(Y,Z), path(X,Y).
----- end my-prog.pl -----

? trace.
? [my-prog].
? path(a,d).
true
? path(a,e).
false

http://www.cse.ucsc.edu/classes/cmps112/Spring03/languages/prolog/PrologIntro.pdf

---------------------------
append([],List,List).
append([H|Tail],X,[H|NewTail]) :- append(Tail,X,NewTail).
---------------------------
?- trace. append([a,b,c],[d,e],X).

Unknown message: query(yes)
Call: (7) append([a, b, c], [d, e], _G329) ? creep
Call: (8) append([b, c], [d, e], _G410) ? creep
Call: (9) append([c], [d, e], _G413) ? creep
Call: (10) append([], [d, e], _G416) ? creep
Exit: (10) append([], [d, e], [d, e]) ? creep
Exit: (9) append([c], [d, e], [c, d, e]) ? creep
Exit: (8) append([b, c], [d, e], [b, c, d, e]) ? creep
Exit: (7) append([a, b, c], [d, e], [a, b, c, d, e]) ? creep
X = [a, b, c, d, e].

1 Call append([a,b,c],[d,e],Result). %% Initial call
%% Result = [a|NewTail]
2 Call append([b,c],[d,e],NewTail). %% First recursive call
%% NewTail = [b|NewTail1]
3 Call append([c],[d,e],NewTail1). %% Second recursive call
%% NewTail1 = [c|NewTail2]
4 Call append([],[d,e],NewTail2). %% Third recursive call
5 exit NewTail2 = [d,e] %% Unifying with base case
%% of append.
6 exit NewTail1 = [c,d,e] %% Back substitution of
%% NewTail2
7 exit NewTail = [b,c,d,e] %% Back substitution of
%% NewTail1
8 exit Result = [a,b,c,d,e] %% Back substitution of
%% NewTail

Programs
http://www.anselm.edu/homepage/mmalita/culpro/index.html

Palindrome
palindrome(L):- reverse(L,L).

my_reverse([],[]).
my_reverse([H|T],R):- my_reverse(T,T1),append(T1,[H],R).
?- palindrome([a,b,b,a]).
true

Circumscription, closed world assumption, default logic

Closed world assumption (CWA):
- Unless an atomic sentence is known to be true, it can be assumed to be false.
- arbitrary atomic sentence is assumed to be false by default, unless specified to be true
- Act as if KB has complete knowledge, so it's either in KB+ or it's not
- KB = KB+ union negative_literals
- KB+ is consistent if KB |=c a but not KB |=c ~a
- KB |=cd a ; where cd means domain closure, no objects exists other than named constants

Circumscription
- strategy is to minimize abnormality (Ab) (minimal entailment), so as few abnormal individuals as possible
- Let Ab be a predicate to handle abnormal cases where defaults don't apply
- Vx [Bird(x) ^ ~AbFly(x) => Flies(x)] if x is a bird and x is not abnormal flier, then it flies; all NORMAL birds fly
- generalization of CWA

Default logic
- KB = where F is a set of first-order-sentences, D is a set of default rules which specifies which assumptions can be made and when
- default rule is Bird(x):Flies(x)/Flies(x), so if we have Bird(x) and ~Flies(x) then assume Flies(x), can be written as Bird(x)=>Flies(x)
- extension - sentences that constitute a reasonable set of beliefs given a default theory

description logics - dl, alc

Description logics
• Formalisms for expressing concepts, their attributes (or
associated roles), and the relationships between them.
• Can be regarded as providing a KR system based on a
structured representation of knowledge.

Description Logic: (p138) - Ch 9
Three types of non-logical symbols:
• atomic concepts:
Dog, Teenager, GraduateStudent
We include a distinguished concept: Thing
• roles: (all are atomic)
:Age, :Parent, :AreaOfStudy
• constants:
johnSmith, chair128
Four types of logical symbols:
• punctuation: [, ], (, )
• positive integers: 1, 2, 3, ...
• concept-forming operators: ALL, EXISTS, FILLS, AND
• connectives: =, =, and →

[AND Company
For example: [EXISTS 7 :Director]
[ALL :Manager [AND Woman
“a company with at least 7 directors,
whose managers are all women with [FILLS :Degree phD]]]
PhDs, and whose min salary is $24/hr” [FILLS :MinSalary $24.00/hour]]

([AND Surgeon Female] = Doctor) is not valid.

C= is subsumed-by

But it is entailed by a KB that contains
(Surgeon = [AND Specialist [FILLS :Specialty surgery]])
(Specialist C= Doctor)

computing subsumption, that is, determining
whether or not KB = (d subsumed-by e) - 'no negation of alpha query)
assumptions:
- KB is acyclic
- d is atomic, only appears once in LHS
- replace
Under these assumptions, it is sufficient to do the following:
• normalization: using the definitions in the KB, put d and e into a special
normal form, d′ and e′
• structure matching: determine if each part of e′ is matched by a part of d′.
- In other words, for every part of the more general concept,
there must be a corresponding part in the more specific one.
p153. [and person [fills :age 27]

computing satisfaction: To determine if KB = (c → e), we use the following procedure:
1. find the most specific concept d such that KB = (c → d)
2. determine whether or not KB = (d C= e), as before.
joe->person , canCorp, joe is manager of cancorp, manager of cancorp is canadian, so you get joe->canadian

computing classification:
- Positioning a new atom in a taxonomy is called classification
- wine example, Wine is at the top root node, then there's white-very-dry-bordeaux-wine

The Logic ALC
Main components:
• Concepts: classes of individuals
• Roles: binary relations between individuals
• Complex concepts using constructors
• Define terminology: TBox
• Give assertions: ABox
Examples:
• Concept names: Person, Female
• Role names: ParentOf, HasHusband
• Individual names: John, Mary

Assertion C(a) (in B&L it's a->C)

MotherWithoutDaughter = Mother ∀ParentOf.¬Female
(P erson M ale)(John)

A Tableaux Algorithm for ALC (Attributive Concept Language with Complements, more expressive DLs)
• Try to prove concept satisfiability by constructing a model.
• A tableau is a graph representing such a model.
• A set of tableaux expansion rules is used to construct the tableau.
• Either a model is constructed or there is an obvious contradiction.
• If tree T contains a clash the concept C is unsatisfiable.

Unfolded: expand every concept name occurring in C

First Order Logic - FOL

Propositional logic is declarative but not expressive, hence we have First Order Logic (FOL), also called Predicate Calculus

Has quantifiers, universal ∀x (usually use ->), existential ∃x (usually use ^)

∃x ∀y is not the same as ∀y ∃x

∃x ∀y Loves(x,y)
“There is a person who loves everyone in the world”
∀y ∃x Loves(x,y)
“Everyone in the world is loved by at least one person”

∀x Likes(x,IceCream) = ¬∃x ¬Likes(x,IceCream)

kinship domain:
object are people
Properties include gender and they are related by relations
such as parenthood, brotherhood,marriage
predicates: Male, Female (unary)
Parent,Sibling,Daughter,Son...
Function:Mother Father

{a/Shoot} <- substitution

Rule Based Reasoning

Entailment means that one thing follows from another:
KB ╞ α

Propositional Logic
--------------------

The proposition symbols P1, P2 etc are sentences
conjunction ^
disjunction V
implication (if-then) a -> b ≡ ~a V b // false iff a=T and b=F
biconditional a <-> b ≡ (a->b) ^ (b->a)

logically equivalent α ≡ ß iff α╞ β and β╞α

for:
1. (a ^ b) V (c V d)
2. (a V c V d) ^ (b V c V d)

We say we pick all the operand and operators after "a" except "^ b" since we are distributing over "^" in phrase "^ b" i.e. "a" operates on "V (c V d)" and "b" operates on the same phrase and the final operator is "^" which will go in the middle.

The same is true for the second example you mentioned...

1. (a ^ b) V (c ^ d) // Distribute over "^" in "a^b"
2. (a V (c ^ d)) ^ (b V (c ^ d)) // Expand
3. ((a V c)^(a V d)) ^ ((b V c)^(b V d)) // all operators outside parentheses are of type "^" so good to remove extra ones
4. (a V c) ^ (a V d) ^ (b V c) ^ (b V d)



A sentence is valid if it is true in all models (truth tables where α=True),

Validity is connected to inference via the Deduction Theorem:
KB ╞ α if and only if (KB ⇒ α) is valid

A sentence is satisfiable if it is true in some model

A sentence is unsatisfiable if it is true in no models

Satisfiability is connected to inference via the following:
KB ╞ α if and only if (KB ∧¬α) is unsatisfiable [] (empty clause)

Interpretation: any assignment of true and false to atoms

Rules of inference


Model checking
⌧truth table enumeration (always exponential in n)
⌧improved backtracking, e.g., Davis--Putnam-Logemann-Loveland (DPLL), Backtracking with constraint propagation, backjumping.
⌧heuristic search in model space (sound but incomplete)
e.g., min-conflicts-like hill-climbing algorithms

Resolution is sound

Resolution is NOT complete:
P and R entails P V R but you cannot infer P V R From (P and R) by resolution

Resolution is complete for refutation: adding (¬P) and (¬R) to (P and R) we can infer the empty clause. (proof by contradiction)

CNF = conjunctive normal form eg. (A V B) ^ C

( P ∧ ¬Q ) ∨ ( ¬R ∨ P ) ≡ ( P ∨ ¬ R ∨ P ) ∧ ( ¬ Q ∨ ¬R ∨ P ) ≡ ( P ∨ ¬R ), (¬Q ∨ ¬R ∨ P )

The set of support: those clauses coming from negation of the theorem or their decendents.

Horn clause: Eg C ^ (B -> A) ^ ( C ^ D -> B) NOT! (C V D -> B)

Forward chaining (data driven) - linear time
Idea: fire any rule whose premises are satisfied in the KB,
add its conclusion to the KB, until query is found

Backward chaining (goal driven) - linear time
Idea: work backwards from the query q:
to prove q by BC,
check if q is known already, or
prove by BC all premises of some rule concluding q
Avoid loops: check if new subgoal is already on the goal stack
Avoid repeated work: check if new subgoal
1. has already been proved true, or
2. has already failed


Efficient propositional inference:
- DPLL 1. early termination 2. purse symbol (same sign for everywhere, so either all nots or positives) 3. unit clause - clause with only a literal
- WalkSAT (incomplete), local search using randomness

Table of logic symbols

http://en.wikipedia.org/wiki/Table_of_logic_symbols

implies; if .. then
⇒

→

⊃

http://en.wikipedia.org/wiki/First-order_logic


Every propositional wff α can be converted into a formula α′ in
Conjunctive Normal Form (CNF) in such a way that |= α ≡ α′.
1. eliminate ⊃ and ≡ using (α ⊃ β) -> (¬α ∨ β) etc.
2. push ¬ inward using ¬(α ∧ β) -> (¬α ∨ ¬β) etc.
3. distribute ∨ over ∧ using ((α ∧ β) ∨ γ) -> ((α ∨ γ) ∧ (β ∨ γ))
4. collect terms using (α ∨ α) -> α etc.


http://en.wikipedia.org/wiki/Conjunctive_normal_form

http://www.enm.bris.ac.uk/ai/enjl/

http://www.enm.bris.ac.uk/ai/enjl/logic1.pdf
• 1. The connectives → and ↔ are eliminated using the equivalences
A ↔ B ≡ ( A → B) ∧ (B → A) and then A → B ≡ (¬ A∨ B)
• 2. Secondly, De Morgan’s Laws are applied as widely as possible
¬( A∧ B) is replaced by (¬ A∨ ¬ B)
¬( A∨ B) is replaced by (¬ A∧ ¬ B)
• 3. Multiple negations are reduced using DNEG e.g. ¬¬ A is replaced by A
• 4. The DISTOR rule is frequently applied

After the above procedures have been applied the original sentence is in conjunctive
normal form. Further simplifications can then be made by applying rule 1 (section 4) to
eliminate tautologies e.g. ((¬ A∨ A) ∧ B) ≡ B and repetitions within a clause can be
suppressed using IDOR e.g. A∨ A∨ A ≡ A. Also, if, in a normal form, a clause Ci is
included in another clause C j , the COR and AOR mean that the clausal brackets can be
removed e.g. (( A∨ B) ∨ D) ≡ ( A∨ B∨ D) ≡ ( A∨ ( B∨ D)) etc. Finally rule 1 can be used to
reduce a normal form containing a logically false clause to a logically false clause. Forms
simplified by the above procedures are said to be pure normal forms.

6. ≡ ((P ∧ ¬R) ∧ Q) ∨ (( ¬P ∨ R) ∨ ¬S)
7. ≡ (¬ ( ¬P ∨R ) ∧ Q ) ∨ ( (¬P ∨ R ) ∨ ¬S)8. ≡ ((¬( ¬P ∨ R ) ∧ Q ) ∨ (¬P ∨ R )) ∨ ¬S
9. ((¬ (¬P ∨ R ) ∧ Q) ∨ ( ¬P ∨ R)) ≡ ( Q ∨ ( ¬P ∨R ))
10. ((¬ (¬P ∨ R ) ∧ Q) ∨ ( ¬P ∨ R)) ∨ ¬S ≡ Q ∨¬P ∨ R ∨ ¬S

Skolemization
∃x∀yR(x,y) |= ∀y∃xR(x,y)
∀y∃xR(x,y) |≠ ∃x∀yR(x,y)

∃x∀y∃zP(x,y,z) to ∀yP(a,y,f(y))

Abbreviations:
(α ⊃ β) for (¬α ∨ β)
safer to read as disjunction than as “if ... then ...”
(α ≡ β) for ((α⊃β) ∧ (β⊃α))

kr - resolution logic

http://en.wikipedia.org/wiki/Resolution_(logic)

A simple example

\frac{a \vee b, \quad \neg a \vee c} {b \vee c}


In English: if a or b is true, and a is false or c is true, then either b or c is true.

If a is true, then for the second premise to hold, c must be true. If a is false, then for the first premise to hold, b must be true.

So regardless of a, if both premises hold, then b or c is true.


Claim: Resolvent is entailed by input clauses.
Suppose I |= (p ∨ α) and I |= (¬p ∨ β)
I |= p
Case 1:
then I | = β, so I |= (α ∨ β).
I |≠ p
Case 2:
then I | = α, so I | = (α ∨ β).
I | = (α ∨ β).
Either way,
{(p ∨ α), (¬p ∨ β)} |= (α ∨ β).
So:

ch 2 - the language of first-order logic

http://en.wikipedia.org/wiki/First-order_logic#Alphabet

Abbreviations:
(a \supset b) for (not a or b)
safer to read as disjunction than as “if ... then ...”
(a three-vertical-lines b) for (((a \supset b)) or ((b \supset a)))

well-formed formulas[3] or wffs

A is a subset of B and conversely B is a superset of A
* B is a proper superset of A; this is written as B\supsetneq A.

kr - ch1, 2

http://users.skynet.be/bs661306/peter/doc/hpv00r03-841.htm
KR (Knowledge Representation) Hypothesis (Smith 1982):
1. there's some structural ingredients to represent knowledge -- knowledge base
2. there's some process to manipulate these ingredients via inference -- reasoning

Notes; Exist structures that:
• we can interpret propositionally
• determine how the system behaves

eg. Expert system, GPS
http://en.wikipedia.org/wiki/General_Problem_Solver
General Problem Solver (GPS) was a computer program created in 1957 by Herbert Simon, J.C. Shaw, and Allen Newell intended to work as a universal problem solver machine. Any formalized symbolic problem can be solved, in principle, by GPS. For instance: theorems proof, geometric problems and chess playing. It was based on Simon and Newell's theoretical work on logic machines. GPS was the first computer program which separated its knowledge of problems (rules represented as input data) from its strategy of how to solve problems (a generic solver engine).


reasoning - Manipulation of symbols encoding propositions to produce representations of new propositions

representation - symbols standing for things in the world

knowledge - taking the world to be one way and not the other, propositions, eg. I know that the sky is blue

entails - eg kb entails alpha, so if the world satisfies kb then it must also (implied that it) satisfy alpha

inference - process of calculating entailments

sound - get only entailments

complete - get all entailments

the language of first order logic

wffs - well-formed formula, St(Bob) V St(Sue) is wff but St(Bob V Sue) is not wff

abbrevations:
logical symbols:
(α ⊃ β) for (¬α ∨ β)
(α ≡ β) for ((α⊃β) ∧ (β⊃α))

x ⊃ y means x -> y means if x then y

non-logical symbols: predicates, functions

a sentence: wff with no free variables (closed)

Substitution: α[v/t] means α with all free occurrences of the v replaced by term t
free occurrence (no scope - ∃ and ∀)

interpretation - Each interpretation assigns to function f a mapping from objects to objects. ℑ = 〈 D, I 〉, D is the domain of discourse (eg people, table), I is an interpretation mapping (eg prop symbols -> true, false)

satisfaction
will write as ℑ,µ = α “α is satisfied by ℑ and µ”
where µ ∈ [Variables → D], as before
or ℑ = α, when α is a sentence
“α is true under interpretation ℑ”
or ℑ = S, when S is a set of sentences

Entailment defined
S |= α iff for every ℑ , if ℑ |= S then ℑ |= α.
Say that S entails α or α is a logical consequence of S:
In other words: for no ℑ , ℑ |= S ∪ {¬α}. S ∪ {¬α} is unsatisfiable

“the elements of S are true under interpretation ℑ”

S = KB = Knowledge base

Special case when S is empty: |= α iff for every ℑ , ℑ |= α.
Say that α is valid. (p.30)

***
include such connections explicitly in S
Key idea ∀x[Dog(x) ⊃ Mammal(x)]
of KR: the rest is just
Get: S ∪ {Dog(fido)} |= Mammal(fido) details...

p33. proof by interpretation, if S |= alpha then I |= S and I= alpha
case1. I |= Green(b), show I |= Green(b) ∧ ¬Green(c) ∧ On(b,c). (based on S, so entailed)
case2. I |= ~Green(b), show I |= Green(a) ∧ ¬Green(b) ∧ On(a,b). (based on S, so entailed)

if I |= alpha, then I is a model of alpha

eg. soap opera world - domains
individuals: john, sleezyTown
basic types: Place, Person
relationships / functions: MarriedTo, DaugherOf

facts = terms
Man(john)
Rich(john)

∀y[Woman(y) ∧ y ≠ jane ⊃ Loves(y,john)]

x ⊃ y means x -> y means if x then y
attributes: Rich, Beautiful

closure: ∀x[Person(x) ⊃ x=jane ∨ x=john ∨ x=jim ...]

Denotation p27
||t||i,u where u in [variables -> d]

Clausal representation p48
Formula = conjunction ^ of clauses { [p, r, s], [p, r, s], [ p ] }
Clause = disjunction V of literals [p, r, s]
Literal = atomic sentence or its negation p
positive literal and negative literal

Resolvent
clauses [w, r, q] and [w, s, ~r] have [w, q, s] as resolvent wrt r.

Resolution is refutation complete

Resolution p53. (uses the process of derivations)
To determine if KB |= a,
1. put KB, ~a into CNF to get S
2. if S->[], the KB V ~a is unsatisfiable and so KB |= a
3. otherwise, KB V ~a is satisfiable and so KB does not entail a

ground if literal contains NO variables eg. Wife(bob,marry)

Generalizing CNF p.57
Generalizing CNF
Resolution will generalize to handling variables
But to convert wffs to CNF, we need three additional steps:
1. eliminate É and º
2. push Ø inward using also Ø"x.a ß $x.Øa etc.
3. standardize variables: each quantifier gets its own variable
e.g. $x[P(x)] Ù Q(x) ß $z[P(z)] Ù Q(x) where z is a new variable
4. eliminate all existentials (discussed later)
5. move universals to the front using ("xa) Ù b ß "x(aÙ b)
where b does not use x
6. distribute Ú over Ù
7. collect terms
Get universally quantified conjunction of disjunction of literals

Answer predicate - A(x)
[~St(x), ~Happy(x), A(x)]
...
[A(bob)]

Skolem - names for individuals claimed to exist, called Skolem

Skolem preserve satisfiability, not equivalence so ExP(x) not equal P(a)!!

*MGU - most general unifier p70. / unification
- finding skolem variables theta given P(f(x), y, g(y)) and P(f(x), z, g(x)), answer is theta = {y/z, z/x} to get P(f(x), x, g(x))

***Note: important to get dependence of variables correct p65
AyExR(x,y) => AyR(f(y),y) so the best way to remember is to put brackets, it's better Ax (for all x) is inside the bracket because it's more flexible
vs. ExAyR(x,y) => AyR(a,y)

strategies:
- directional connectives (forward, backward)
- unit clauses
- set of support (always resolve with at least one clause that's the ancestor of ~q, just unifying with KB is useless)
- clause elimination, tautology (always true), pure clause (only one atom p in the formula)

horn clause = has at MOST one +ve literal (p80)
- as implications: (¬child ∨ ¬male ∨ boy)
- e.g. [¬p1, ¬p2, ..., ¬pn, q]
- e.g. [¬p1, ¬p2, ..., ¬pn] and also [ ] (all negative)
- p1 ∧ p2 ∧ ... ∧ pn ⇒ q (if p1 and p2 and ... and pn then q) or Note:
(¬p1 ∨ ¬p2 ∨ ... ∨ ¬pn ∨ q) or [(p1 ∧ p2 ∧ ... ∧ pn) ⊃ q]

SLD - (Selected literals) (linear form) (definite clauses)
sld derivation / resolution in Horn clauses - can also use a goal tree where the root is the goal and leaves are in the KB

back-chaining - depth first, left-right, back-chaining (strategy used in Prolog), can go to inf. loop

forward-chaining - mark atoms as solved

problem - can give inf. branch of resolvents in FOL

Standardize variables: each quantifier should use a different one

Ordering goals p94.
1. get ParentOf(sam,z): find child of Sam searching downwards
2. get ParentOf(z,sue): find parent of Sue searching upwards
3. get ParentOf(–,–): find parent relations searching in both directions
Search strategies are not equivalent
if more than 2 children per parent, (2) is best