Programmazione Logica e ASP
Forma normale congiuntiva e clausole
Un letterale è una formula atomica o la negazione di una formula atomica.
Una clausola è una disgiunzione di letterali:
A1  ...  An  B1  ...  Bm
[con Ai , Bj atomi]
equivalentemente, puo essere rappresentata in forma implicativa:
B1  ...  Bm  A1  ...  An
Una formula in forma normale congiuntiva è una congiunzione di clausole.
Qualsiasi formula proposizionale può essere convertita in una formula
proposizionale in forma normale congiuntiva logicamente equivalente.
Qualsiasi formula ben formata della logica dei predicati ø può essere
convertita in una formula ben formata della logica dei predicati in forma
normale congiuntiva ø’. Si osservi che,
1.
2.
In generale ø non è logicamente equivalente a ø’, ma
ø è insoddisfacibile sse ø’ è insoddisfacibile.
Una Base della conoscenza (KB) è un insieme di clausole.
Risoluzione [I]
Caso proposizionale


 
con  
con
( - { })  (  - { })
I simboli  e  indicano clausole, mentre  è uno dei letterali che ne
fanno parte (può naturalmente non essere l’unico).
Esempio
1. {P, Q}
2. {P, R}


3. {Q, R}
1,2
Il simbolo  indica le clausole presenti
inizialmente della ase della conoscenza.
Procedura per Risoluzione Prooposizionale
Premesse...
KB ⊦ φ
sse KB ⊧ φ
sse KB ∪ {⌝φ} insoddisfacibile
sse KB ∪ {⌝φ} incoerente
Come dimostriamo KB ⊦ φ ?
KB ⊦ φ
Esecuzione di un Programma [P]
Una computazione corrisponde al tentativo di dimostrare,
tramite la regola di risoluzione, che una formula (goal)
segue logicamente da un insieme di formule (programma);
cioè, che la formula e’ un teorema.
Si deve determinare una sostituzione per le variabili del goal
(detto anche “query”) per cui il goal segue logicamente dal
programma.
Dato un programma P e una query:
:- S (t1, t2, …, tm) .
se x1, x2, …, xn sono le variabili che compaiono in t1, t2, …, tm il
significato logico della query e’: x1 x2 … xn S (t1, t2, …, tm)
e l’obiettivo e’ quello di trovare una sostituzione
 = [x1 / a1, x2 / a2 , …, xn/an]
dove ai sono termini tale per cui P
[S (t1, t2, …, tm)]

Risoluzione SLD
Operativamente...
La Risoluzione SLD seleziona un atomo Am dal goal Gi secondo
un determinato criterio, e lo unifica se possibile con la testa
della clausola Ci attraverso la sostituzione più generale:
MOST GENERAL UNIFIER (MGU)
Il nuovo risolvente e’ ottenuto da Gi riscrivendo l’atomo selezionato con
la parte destra della clausola Ci ed applicando la sostituzione i.
Più in dettaglio:
:- A1, …, Am-1, Am, Am+1, …,Ak .
A :- B1, …, Bk .
[Am] i = [A] i
Risolvente,
clausola del programma P, e
allora la risoluzione SLD deriva il nuovo
risolvente
:- [A1, …, Am-1, B1, …, Bq , Am+1, …, Ak] i .
Derivazione SLD
Una derivazione SLD per un goal G0 dall’insieme di clausole
definite P e’ una sequenza di clausole goal
G0 , …, Gn , una sequenza di rinomine di clausole del
programma C1 , …, Cn , e una sequenza di sostituzioni MGU
1 ,…, n tali che Gi+1 è derivato da Gi e da Ci+1 attraverso la
sostituzione n.
La sequenza può essere anche infinita.
Esistono tre tipi di derivazioni:
SUCCESSO, se per
n finito Gn è uguale alla clausola vuota Gn= :-–
FALLIMENTO FINITO, se per n finito non è più possibile derivare
un nuovo risolvente da Gn e Gn non è
uguale a :-–
FALLIMENTO INFINITO, se è sempre possibile derivare nuovi
risolventi tutti diversi dalla clausola
vuota.
Non Determinismo
Nella risoluzione SLD, così come è stata enunciata, si hanno due
forme di non determinismo.
La prima forma di non determinismo è legata alla selezione di un
atomo Am del goal da unificare con la testa di una clausola, e viene
gestita definendo una particolare regola di calcolo.
La seconda forma di non determinismo è legata alla scelta di quale
clausola del programma P utilizzare in un passo di risoluzione, e
viene gestita definendo una strategia di ricerca.
Strategia di Ricerca
Questa forma di non determinismo implica che possano esistere più
soluzioni alternative per uno stesso goal, corrispondenti alle diverse
scelte delle clausole con cui tentare l’unificazione.
La risoluzione SLD (completezza), deve essere in grado di generare
tutte le possibili soluzioni e quindi deve considerare ad ogni passo di
risoluzione tutte le possibili alternative.
La strategia di ricerca deve garantire questa completezza
Una forma grafica utile per rappresentare la risoluzione SLD e questa
forma di non determinismo sono gli alberi SLD.
Programmi logici:
forma generale e terminologia
clausola di Horn
una calusola con al più un letterale positivo
⌝A1∨ ... ∨ ⌝ Am ∨ B1
[⌝A1,... ,⌝ Am , B1]
[B1]
A1  ...  Am  B1
 B1
Alcune inferenze
1.
Mario è un architetto oppure è un geometra.
Se Mario fosse architetto, allora Mario sarebbe laureato.
Mario non è laureato.
Quindi: Mario è un geometra
.
2.
Giovanni Paolo II è siciliano.
Tutti i siciliani sono giardinieri.
Quindi: Giovanni Paolo II è giardiniere.
3.
Tutti i cigni osservati sinora in Europa sono bianchi.
Tutti i cigni osservati sinora in Nord America sono bianchi.
Tutti i cigni osservati sinora in Sud America sono bianchi […]
Non sono mai stati osservati cigni che non fossero bianchi.
Quindi: Tutti i cigni sono bianchi.
4.
L’assassino ha sporcato di fango il tappeto.
Chiunque fosse entrato dal giradino avrebbe sporcato di fango il tappeto.
Quindi: L’assassino è entrato dal giardino.
5.
Gli uccelli, salvo eccezioni/in genere, sono in grado di volare.
Titti è un uccello.
Quindi: Titti è in grado di volare.
Ragionamento non monotono
Una nozione di inferenza e’ monotona se e solo se Г ⊢p
implica Г ∪ A⊢p
 La monotonia e’ la proprieta’ matematica di una funzione f tale per cui
se x ≤ y , allora f(x) ≤ f(y)
. .
 La non monotonia e’ una proprieta’ definita per negazione (l’assenza
della monotonia).
FOL è monotona...
Al crescere della KB l’insieme di inferenze può solo continuare crescere
Prolog e ASP permettono di eseguire inferenze non
monotone
 Il ragionamento non monotono permette di trattare inferenze
ragionando sull’assenza di informazioni.
 Al crescere di una KB, ci può essere l’esigenza di ritrattare le
inferenze fatte sulla base di ciò che non si conosce
Ragionamento non monotono
E.g.
 Supponiamo di codificare nella logica del primo ordine
un orario ferroviario
TrainFromTo(X,CittàPartenza,CittàArrivo,OrarioPart)
 Proviamo a chiederci...
∃x TrainFromTo(X,Milano,Roma,14.50)
...supponiamo non esista. In FOL dovremmo dimostrare:
⌝∃x TrainFromTo(X,Milano,Roma,14.50)
 Dovremmo dimostrare
∀x⌝TrainFromTo(X,Milano,Roma,14.50)
Il fatto che non esista una dimostrazione di
∃x TrainFromTo(X,Milano,Roma,14.50)
non implica che ne esista una per ⌝∃x
TrainFromTo(X,Milano,Roma,14.50)
Formal Knowledge Representation and Automated Reasoning
for the Study of Archaeological Stratigraphy
M. Cattani, G. Mantegari, A. Mosca, M. Palmonari
Department of Archaeology, University of Bologna (Italy)
Department of Informatics, Systems and Communication,
University of Milan Bicocca (Italy)
Computerized stratigraphy has a long research history and brought to the creation of
some succesfull softwares (e.g. ArchEd, Stratify) which can guarantee a quite satisfiable
management of the stratigraphic sequences.
Some problems concern:
• the difficulty to manage large/huge datasets
• the difficulty to integrate a digital matrix representation with other softwares (e.g. GIS)
• the difficulty to handle multilinear stratigraphic sequences
• the difficulty to manage uncertain or insufficient knowledge
• ...
but...this is half of the problem...
At a more general level, which concerns the model itself, some other issues can be
found. For example the Harris model has been criticized from different points of view (see
the Harris-Carver debate) but it still represent the principal methology for modelling and
representing the stratigraphic sequence.
The project aims at proposing a new approach for the study of the
archaeological stratigrafy by means of Computer Science techniques
and tools
Our main objective, in this phase, are to investigate:
• the possibility of modelling the stratigraphy by means of
formal knowledge representation
• the possibility of performing automated reasoning with respect to:
• the spatial component
• the temporal component
We are not interested, in this phase, to the
visualization of the stratigraphic sequence.
In our vision, the graphical representation is just the last
step and, provided the logical model is adequate and the
automatic reasoning works well, it is a minor problem.
Of course we aim at realizing a software or a set of tools, but
at the moment we focus mainly on the creation of a fomal model
rather than on the specification of the software requirements.
Programmi logici:
forma generale e terminologia
A1  ...  Am  B1
clausola di Horn
una calusola con al più un letterale positivo
Termini: X , marco , f(X) , f(marco), f(f(X))
Atomi: Ai = P(t) , p , R(t1,t2)
Letterali: Li = ⌝Ai , Ai
Ground: P(a) , p , ⌝ R(a,b) … no variabili!
Programmi logici:
forma generale e terminologia
A1  ...  Am  B1
clausola di Horn
una calusola con al più un letterale positivo
disjunctive extended LPs
L0 or... or Lk:- Lk+1 , ... , Lm , not Lm+1 , ... , not Ln
L0 ::- L0 , ... , Lm , not Lm+1 , ... , not Ln
Ak:- Ak+1 , ... , Am
A0 :- A1 , ... , Am , not Am+1 , ... , not An
rule : head ← body
fact
constraint (⊥)
definite LPs
ASP-not
normal LPs
ASP
extended LPs
ASP⌝
A0 or... or Ak:- Ak+1 , ... , Am , not Am+1 , ... , not An disjunctive LPs
ASPor
L0 :- L1 , ... , Lm , not Lm+1 , ... , not Ln
L0 or... or Lk:- Lk+1 , ... , Lm , not Lm+1 , ... , not Ln
ASP*=ASP⌝,⊥,or
Programmi logici:
forma generale e terminologia
A1  ...  Am  B1
clausola di Horn
una calusola con al più un letterale positivo
disjunctive extended LPs
L0 or... or Lk:- Lk+1 , ... , Lm , not Lm+1 , ... , not Ln
rule : head ← body
datalog = no simboli di funzione
Ak:- Ak+1 , ... , Am
A0 :- A1 , ... , Am , not Am+1 , ... , not An
definite LPs
ASP-not
normal LPs
ASP
extended LPs
ASP⌝
A0 or... or Ak:- Ak+1 , ... , Am , not Am+1 , ... , not An disjunctive LPs
ASPor
L0 :- L1 , ... , Lm , not Lm+1 , ... , not Ln
L0 or... or Lk:- Lk+1 , ... , Lm , not Lm+1 , ... , not Ln
ASP*=ASP⌝,⊥,or
The Answer set framework
Answer set framework:
- Axiom alphabet and language
- Knowledge Base
- Query alphabet and language
- Entailment relation between a KB (a set
of axioms) and a query
ASP Alphabets & language
ASP alphabet:
variables
connectives
punctuation symbols
the special symbol
X,Y,... (capital letter notation)
{⌝,or,←,not,’,’} (often :- instead of ←)
{‘(’,’)’,’.’}
⊥
object constants
function symbols
predicate symbols
(propositional symbols as 0-ary predicate!)
Term definition:
A variable is a term
A constant is a term
If t1,...,tn are terms, f(t1,...,tn) is a term.
E.g. X Y
E.g. marco
E.g. f(marco,X)
A term is ground if it does not contain any
variable
Variables (‘Terms’)
X, Y, Z, ...
Constants (‘Terms’)
A l p h a b e t Example
us1, us2, us3, ...
Unary Predicates (‘Atoms’)
cutUnit(X), trench(X), wall(X), ...
Binary Predicates (‘Atoms’)
cover(X,Y), fill(X,Y), cut(X,Y), ...
Positive & Negative Literals (‘Atoms’ or ‘Classically Negated Atoms’)
wall(X), cut(X,Y),..., cover(X,Y), fill(X,Y), ...
Ground Literals
cover(u6,u3), filledBy(u4,u8), ...
naf-Literals (‘Atoms’ or ‘Atoms preceeded by not’)
..., not cover(X,Y), not fill(X,Y), ...
Rules
dirPostTo(Z,Y)
:- equalTo(X,Y),cover(Z,X).
contemporary(X,Y) :- equalTo(X,Y).
Constraints
:- attachTo(X,X).
• Facts
equal(X,X).
cover(u6,u3).
ASP Alphabets & language
disjunctive extended LPs
L0 or... or Lk:- Lk+1 , ... , Lm , not Lm+1 , ... , not Ln
L0 ::- L0 , ... , Lm , not Lm+1 , ... , not Ln
Ak:- Ak+1 , ... , Am
A0 :- A1 , ... , Am , not Am+1 , ... , not An
rule : head ← body
fact
constraint (⊥)
definite LPs
ASP-not
normal LPs
ASP
extended LPs
ASP⌝
A0 or... or Ak:- Ak+1 , ... , Am , not Am+1 , ... , not An disjunctive LPs
ASPor
L0 :- L1 , ... , Lm , not Lm+1 , ... , not Ln
L0 or... or Lk:- Lk+1 , ... , Lm , not Lm+1 , ... , not Ln
ASP*=ASP⌝,⊥,or
ASP Semantics
For ASP Datalog the Herbrand Base can be easily built
(it is finite!)
AS ground programs: principles
ASP rules:
L0 or... or Lk:- Lk+1 , ... , Lm , not Lm+1 , ... , not Ln
A rule is said to be ground if all the literals of the rule are gorund
The answer set language given by a alphabet consists of the set of
all ground rules contructed from the symbols of the alphabet
A answer set program Π: a set of rules
A program Π identifies an alphabet used by Π (predicates, constants,
function symbols)
ground(Π): the set of goround rules obtained with the alphabet used
in Π
Intensional part of KB: axioms with body, constraints
Extensional part of KB: the set of facts
Alphab
• Unary Predicates (‘Atoms’)
cutUnit(X), trench(X), wall(X), ...
e t And Rules
• Binary Predicates (‘Atoms’)
cover(X,Y), fill(X,Y), cut(X,Y), ...
• Positive & Negative Literals (‘Atoms’ or ‘Classically Negated Atoms’)
wall(X), cut(X,Y),..., cover(X,Y), fill(X,Y), ...
• Ground Literals
cover(u6,u3), filledBy(u4,u8), ...
• Rules
dirPostTo(Z,Y)
:- equalTo(X,Y),cover(Z,X).
contemporary(X,Y) :- equalTo(X,Y).
contemporary(X,Y) v
posteriorTo(X,Y) v
posteriorTo(Y,X) :-
• Constraints
:- attachTo(X,X).
• Facts
equal(X,X).
cover(u6,u3).
us(X),us(Y),
not posteriorTo(X,Y),
not -posterior(X,Y).
Alphab
• Unary Predicates (‘Atoms’)
cutUnit(X), trench(X), wall(X), ...
e t And Rules
• Binary Predicates (‘Atoms’)
cover(X,Y), fill(X,Y), cut(X,Y), ...
Ground rules:
• Positive & Negative Literals (‘Atoms’ or ‘Classically Negated Atoms’)
All the rules built
by substituting
the variables
with the
set of
wall(X),
cut(X,Y),...,
cover(X,Y),
fill(X,Y),
constants given in the alphabet (all the possible combination!)
• Ground Literals
cover(u6,u3), filledBy(u4,u8),
...us2, us3, ...
us1,
• Rules
dirPostTo(Z,Y)
:- equalTo(X,Y),cover(Z,X).
contemporary(X,Y) :- equalTo(X,Y).
contemporary(X,Y) v
posteriorTo(X,Y) v
posteriorTo(Y,X) :-
• Constraints
:- attachTo(X,X).
• Facts
equal(X,X).
cover(u6,u3).
us(X),us(Y),
not posteriorTo(X,Y),
not -posterior(X,Y).
...
Alphab
• Unary Predicates (‘Atoms’)
cutUnit(X), trench(X), wall(X), ...
e t And Rules
• Binary Predicates (‘Atoms’)
cover(X,Y), fill(X,Y), cut(X,Y), ...
Ground rules:
• Positive & Negative Literals (‘Atoms’ or ‘Classically Negated Atoms’)
All the rules built
by substituting
the variables
with the
set of
wall(X),
cut(X,Y),...,
cover(X,Y),
fill(X,Y),
constants given in the alphabet (all the possible combination!)
• Ground Literals
cover(u6,u3), filledBy(u4,u8),
...us2, us3, ...
us1,
• Rules
contemporary(X,Y) :- equalTo(X,Y).
contemporary(us1,us2) :- equalTo(us1,us2).
contemporary(us1,us3) :- equalTo(us1,us3).
contemporary(us2,us3) :- equalTo(us2,us3).
…
• Constraints
:- attachTo(X,X).
• Facts
equal(X,X).
cover(u6,u3).
...
ASP Semantics: principles
ASP semantics is based on answer sets
(close to stable models)
Strategy:
semantics for
 ASP-not
 ASP
 ASP⌝
 ASP*=ASP⌝,⊥,or
ASP Semantics: principles
Informally, an answer set S of a ground program
Π is a set of ground literals such that every rule
is satisfied by S,
i.e., for any rule in Π
A  B1, …, Bm, not C1, …, not Cn.
if Bjs are satisfied (Bjs are in S) and Cjs are not
satisfied (not Cj is satisfied if Cj is not in S), then
A is in S.
ASP Semantics: principles
Which are the answer sets for a program Π?
Informally, given a program Π:
generate ground(Π)
generate all the possible models s1,…, sn for Π,
for all si check if ground(Π) is satisfied by si
for all si satisfying ground(Π), check which of them are
minimal
these are answer sets for Π
 What is meant to be a model?
 Via Herbrand base, literal set (for true negation)
 Program transformation for programs with not
How ASP differs from …
Prolog: ordering matters in Prolog; can not handle cycles
with “not”; has extra-logical features; does not have
disjunction and classical negation; and is not
declarative.
Logic Programming: is a class of languages and many
FOL:
 Classical logic is monotonic.
  in AnsProlog, which helps in expressing causality, is not
reverse implication.
 Disjunction symbol “or” in AnsProlog is non-classical.
 The negation as failure symbol “not” in AnsProlog is nonclassical.
formally...
formally...
L0 :- L1 , ... , Lm , not Lm+1 , ... , not Ln
ASP: Gelfond-Lifshitz transformation
In order to give the semantics to a ASP program (containing not) we
have to apply the Gelfond-Lifshitz transformation to the program.
Then proceed as usual….
Brave vs. Cautious Reasoning
BRAVE (credolous) reasoning
A query is bravely true for a substitution if it is
satisfied in at least one model of the program.
• E.g. P(X)? if P(a)?,P(b)?...
CAUTIOUS (skeptical) reasoning
A query is cautiously true for a substitution if it
is satisfied in all models of the program.
ASP Alphabets & language
disjunctive extended LPs
L0 or... or Lk:- Lk+1 , ... , Lm , not Lm+1 , ... , not Ln
L0 ::- L0 , ... , Lm , not Lm+1 , ... , not Ln
Ak:- Ak+1 , ... , Am
A0 :- A1 , ... , Am , not Am+1 , ... , not An
rule : head ← body
fact
constraint (⊥)
definite LPs
ASP-not
normal LPs
ASP
extended LPs
ASP⌝
A0 or... or Ak:- Ak+1 , ... , Am , not Am+1 , ... , not An disjunctive LPs
ASPor
L0 :- L1 , ... , Lm , not Lm+1 , ... , not Ln
L0 or... or Lk:- Lk+1 , ... , Lm , not Lm+1 , ... , not Ln
ASP*=ASP⌝,⊥,or
OR programs
p | q :- s.
c :- p.
c :- q.
s.
p? (cautiously / bravely)
Tweety ASP
fly(X) :- bird(X), not ab(X).
ab(X) :- penguin(X).
bird(X) :- penguin(X).
bird(tweety).
penguin(skippy).
-fly(tweety)?
fly(X)?
Tweety
fly(X) :- bird(X), not -fly(X).
-fly(X) :- penguin(X).
bird(tweety).
bird(rocky).
penguin(rocky).
⌝
ASP
Dottorandi...
Generalmente, i dottorandi non sono ricchi.
Alle maldive ci va chi è ricco.
Marco è un dottorando
Queries: Marco va alle maldive?
Chi va alle maldive?
-haSoldi(X) :- dottorando(X), not ricco(X).
maldive(X) :- ricco(X).
-maldive(X) :- -ricco(X).
dottorando(marco).
maldive(marco)?
not maldive(marco)?
-maldive(marco)?
maldive(X)?
-maldive(X)?
Dottorandi...
Generalmente, i dottorandi non sono ricchi.
Alle maldive ci va chi è ricco.
Marco è un dottorando
Queries: Marco va alle maldive?
Chi va alle maldive?
-haSoldi(X) :- dottorando(X), not ricco(X).
maldive(X) :- ricco(X).
-maldive(X) :- -ricco(X).
dottorando(marco).
maldive(marco)?
not maldive(marco)?
-maldive(marco)?
maldive(X)?
-maldive(X)?
Dottorandi...updating the KB
Si diventa ricchi ribando e/o vincendo il totip.
I ladri rubano, ma generalmente, i dottorandi no;
tuttavia le persone stressate possono diventare
dei ladri.
Marco è stressato
-ruba(X) :- dottorando(X), not ruba(X).
ricco(X) :- vinceTotip(X).
ricco(X) :- ruba(X).
ruba(X) :- ladro(X).
ladro(X) :- stressato(X), not -ladro(X).
stressato(marco).
Dottorandi...updating the KB II
Un altro modo per diventare ricchi è ricevere regali. Per ricevere un
regalo occorre che qualcuno lo faccia il regalo. In genere (se non so il
contrario?) se una persona è amico/a di un’altra persona ed è una
persona generosa le fa un regalo.
Maria è un amica di Marco molto generosa.
ricco(X) :- riceveRegalo(X).
riceveRegalo(X) :- faRegalo(Y,X).
faRegalo(X,Y) :- generoso(X), amico(X,Y), not -faRegalo(X,Y).
generoso(maria).
amico(maria,marco).
-ruba(X) :- faRegalo(Y,X).
Dottorandi...
Generalmente, i dottorandi non sono ricchi.
Alle maldive ci va chi è ricco.
Marco è un dottorando
Queries: Marco va alle maldive?
Chi va alle maldive?
-haSoldi(X) :- dottorando(X), not ricco(X).
maldive(X) :- ricco(X).
-maldive(X) :- -ricco(X).
dottorando(marco).
maldive(marco)?
not maldive(marco)?
-maldive(marco)?
maldive(X)?
-maldive(X)?
Dottorandi...updating the KB
Si diventa ricchi ribando e/o vincendo il totip.
I ladri rubano, ma generalmente, i dottorandi no;
tuttavia le persone stressate possono diventare
dei ladri.
Marco è stressato
-ruba(X) :- dottorando(X), not ruba(X).
ricco(X) :- vinceTotip(X).
ricco(X) :- ruba(X).
ruba(X) :- ladro(X).
ladro(X) :- stressato(X), not -ladro(X).
stressato(marco).
Dottorandi...updating the KB II
Un altro modo per diventare ricchi è ricevere regali. Per ricevere un
regalo occorre che qualcuno lo faccia il regalo. In genere (se non so il
contrario?) se una persona è amico/a di un’altra persona ed è una
persona generosa le fa un regalo.
Maria è un amica di Marco molto generosa.
ricco(X) :- riceveRegalo(X).
riceveRegalo(X) :- faRegalo(Y,X).
faRegalo(X,Y) :- generoso(X), amico(X,Y), not -faRegalo(X,Y).
generoso(maria).
amico(maria,marco).
-ruba(X) :- faRegalo(Y,X).