Programmazione Logica e ASP. Forma normale congiuntiva e clausole Un letterale è una formula...

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. In generale ø non è logicamente equivalente a ø’, ma2. ø è insoddisfacibile sse ø’ è insoddisfacibile.

Una Base della conoscenza (KB) è un insieme di clausole.

Risoluzione [I]

Caso proposizionale

con con

( - { }) ( - { })

1. {P, Q} 2. {P, R}

3. {Q, R} 1,2

Il simbolo indica le clausole presenti inizialmente della ase della conoscenza.

Esempio

I simboli e indicano clausole, mentre è uno dei letterali che ne fanno parte (può naturalmente non essere l’unico).

Procedura per Risoluzione Prooposizionale

Premesse...KB ⊦ φ sse KB ⊧ φ

sse KB ∪ {⌝φ} insoddisfacibile sse KB ∪ {⌝φ} incoerente

KB ⊦ φ

Come dimostriamo 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 . Risolvente,

A :- B1, …, Bk . clausola del programma P, e

[Am] i = [A] i 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 lasostituzione 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 generaretutte le possibili soluzioni e quindi deve considerare ad ogni passo dirisoluzione tutte le possibili alternative.

La strategia di ricerca deve garantire questa completezza

Una forma grafica utile per rappresentare la risoluzione SLD e questaforma di non determinismo sono gli alberi SLD.

⌝A1∨ ... ∨ ⌝ Am ∨ B1

[⌝A1,... ,⌝ Am , B1][B1]

A1 ... Am B1

B1

clausola di Hornuna calusola con al più un letterale positivo

Programmi logici: forma generale e terminologia

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.

Alcune inferenze

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 ferroviarioTrainFromTo(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 Reasoningfor 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• ...

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.

but...this is half of the problem...

A1 ... Am B1



Atomi: Ai = P(t) , p , R(t1,t2)

Letterali: Li = ⌝Ai , Ai

Ground: P(a) , p , ⌝ R(a,b) … no variabili!

Termini: X , marco , f(X) , f(marco), f(f(X))

L0 or... or Lk:- Lk+1 ... Lm not Lm+1 ... not Ln rule : head ← body

A1 ... Am B1



A0 :- A1 ... Am not Am+1 ... not An

L0 :- L1 ... Lm not Lm+1 ... not Ln

L0 :-

Ak:- Ak+1 ... Am

fact

:- L0 ... Lm not Lm+1 ... not Ln constraint (⊥)

normal LPs

extended LPs

definite LPs

disjunctive extended LPs

ASP-not

ASP

ASP⌝

A0 or... or Ak:- Ak+1 ... Am not Am+1 ... not An disjunctive LPs ASPor

L0 or... or Lk:- Lk+1 ... Lm not Lm+1 ... not Ln ASP*=ASP⌝,⊥,or


A1 ... Am B1





Ak:- Ak+1 ... Am

normal LPs

extended LPs

definite LPs


ASP-not

ASP

datalog = no simboli di funzione

ASP⌝



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

The project aims at proposing a new approach for the study of thearchaeological stratigrafy by means of Computer Science techniquesand tools

Our main objective, in this phase, are to investigate:

• the possibility of modelling the stratigraphy by means offormal 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, butat the moment we focus mainly on the creation of a fomal modelrather than on the specification of the software requirements.

Why do we care about KR?

PROBLEM SOLUTION

1 1STRATIGRAPHY:

From the spatial relationship between the strata of an excavation find the temporal succession of such strata

STRATIGRAPHY:

A succession of the strata

ASP Alphabets & language ASP alphabet: variables X,Y,... (capital letter notation)connectives {⌝,or,←,not,’,’} (often :- instead of

←)punctuation symbols {‘(’,’)’,’.’}the special symbol ⊥

object constantsfunction symbolspredicate symbols (propositional symbols as 0-ary predicate!)

Term definition:A variable is a term E.g. X YA constant is a term E.g. marcoIf t1,...,tn are terms, f(t1,...,tn) is a term.E.g. f(marco,X)

A term is ground if it does not contain any variable

A l p h a b e t Example Variables (‘Terms’)

X, Y, Z, ...

Constants (‘Terms’)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 Literalscover(u6,u3), filledBy(u4,u8), ...

naf-Literals (‘Atoms’ or ‘Atoms preceeded by not’)..., not cover(X,Y), not fill(X,Y), ...

RulesdirPostTo(Z,Y) :- equalTo(X,Y),cover(Z,X).contemporary(X,Y) :- equalTo(X,Y).

Constraints:- attachTo(X,X).

• Factsequal(X,X).cover(u6,u3).




L0 :-

Ak:- Ak+1 ... Am

fact


normal LPs

extended LPs

definite LPs


ASP-not

ASP

ASP⌝



ASP Alphabets & language

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

• 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 Literalscover(u6,u3), filledBy(u4,u8), ...

• RulesdirPostTo(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) :- us(X),us(Y),

not posteriorTo(X,Y),not -posterior(X,Y).

• Constraints:- attachTo(X,X).


A l p h a b e t And Rules





• RulesdirPostTo(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) :- us(X),us(Y),

not posteriorTo(X,Y),not -posterior(X,Y).




Ground rules:All the rules built by substituting the variables with the set of constants given in the alphabet (all the possible combination!)

us1, us2, us3, ...





• 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).…




Ground rules:All the rules built by substituting the variables with the set of constants given in the alphabet (all the possible combination!)

us1, us2, us3, ...

ASP Semantics: principles

ASP semantics is based on answer sets (close to stable models)

Strategy:

semantics for ASP-not

ASP

ASP⌝

ASP*=ASP⌝,⊥,or


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.


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 non-

classical.

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) reasoningA 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) reasoningA query is cautiously true for a substitution if it

is satisfied in all models of the program.




L0 :-

Ak:- Ak+1 ... Am

fact


normal LPs

extended LPs

definite LPs


ASP-not

ASP

ASP⌝



ASP Alphabets & language

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 ASP⌝

fly(X) :- bird(X), not -fly(X).

-fly(X) :- penguin(X).

bird(tweety).

bird(rocky).

penguin(rocky).

Dottorandi...

-haSoldi(X) :- dottorando(X), not ricco(X).maldive(X) :- ricco(X).-maldive(X) :- -ricco(X).

dottorando(marco).

Generalmente, i dottorandi non sono ricchi. Alle maldive ci va chi è ricco. Marco è un dottorando

Queries: Marco va alle maldive?Chi va alle maldive?

maldive(marco)?not maldive(marco)?-maldive(marco)?maldive(X)?-maldive(X)?

-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).

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

Dottorandi...updating the KB

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).

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.

Dottorandi...updating the KB II

Dottorandi...

-haSoldi(X) :- dottorando(X), not ricco(X).maldive(X) :- ricco(X).-maldive(X) :- -ricco(X).

dottorando(marco).

Generalmente, i dottorandi non sono ricchi. Alle maldive ci va chi è ricco. Marco è un dottorando

Queries: Marco va alle maldive?Chi va alle maldive?

maldive(marco)?not maldive(marco)?-maldive(marco)?maldive(X)?-maldive(X)?

-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).

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

Dottorandi...updating the KB

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).

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.

Dottorandi...updating the KB II

Programmazione Logica e ASP. Forma normale congiuntiva e clausole Un letterale è una formula...

Documents

Transcript of Programmazione Logica e ASP. Forma normale congiuntiva e clausole Un letterale è una formula...