Linguaggi e Modelli Computazionali LS - Prof E.Denti
FOLExpr Analyzer
Un riconoscitore di teorie della
logica del primo ordine per la loro
conversione in forma a clausole
Scopo del Lavoro


Ricevere in input teorie in logica del primo ordine
(First Order Logic)
Riconoscerne la correttezza sintattica
 Basandosi
sulle regole specificate nel corso di
Intelligenza Artificiale della Prof.Mello
 Progettando una grammatica che generi il linguaggio
che comprende le espressioni della logica del primo
ordine (organizzate in teorie)
 Implementando un riconoscitore per il linguaggio

Eseguire analisi e trasformazioni sintattiche
come la trasformazione in forma a clausole
 Secondo
l’algoritmo a 8 step studiato nel corso
Analisi del Problema

I lucidi del corso di Intelligenza Artificiale introducono la logica del
primo ordine, descrivendola come linguaggio

partendo infatti dalla sintassi, in particolare dal suo alfabeto.
Possibili categorie di token
Possibili keywords
Analisi del Problema

Dai lucidi del corso di Intelligenza Artificiale
Lexer
Lexer
Funzioni n-arie e
predicati sono
sintatticamente
identici, cambia solo la
loro semantica nel
senso di vero/falso
(fuori dallo scope del
progetto)
Analisi del Problema

Dai lucidi del corso di Intelligenza Artificiale
Parser:
simbolo
non
terminale
Termine
Parser:
simbolo
non
terminale
Atomo
Analisi del Problema

Dai lucidi del corso di Intelligenza Artificiale
NON TERMINALE FBF:
Potrebbe essere lo scopo
della grammatica, ma per
analizzare TEORIE, prima
avremo bisogno di:
•TEORIA :: LINEA {LINEA}
•LINEA ::= FBF ;
Analisi del Problema

Dai lucidi del corso di Intelligenza Artificiale
Attenersi in modo troppo
stretto alle regole
specificate nel linguaggio
umano si potrebbe giungere a
una grammatica ambigua come
questa:
•TEORIA :: LINEA {LINEA}
•LINEA ::= FBF ;
•FBF ::= FBF (→|↔|Λ|V) FBF
•FBF ::= ~ FBF | ("|$) var FBF
•FBF ::= ATOMO
Parser: simbolo
non terminale
Letterale
Analisi del Problema

Dai lucidi del corso di Intelligenza Artificiale
La parte di grammatica derivata
direttamente dal testo non va
bene ma del resto siamo ancora
in fase di analisi...
Interprete: due
possibili
manipo1lazioni
Analisi del Problema

Dai lucidi del corso di Intelligenza Artificiale
Interprete:
Ci sarà un visitor
per questo
Interprete:
Oltre che
trasformazioni,
si potrebbero fare
anche analisi come
questa
Analisi del Problema

Altre analisi sintattiche da poter fare con l’interprete
Grammatica iniziale: Il Parser
THEORY ::= ONE_LINE | { ONE_LINE }
ONE_LINE ::= FBF semicolon
Associatività a sx: ok! date
le proprietà delle
operazioni logiche
Regole di precedenza
FBF ::= DISG | FBF (→|↔) DISG
descritte nei lucidi
DISG ::= CONG | DISG or CONG
rispettate!
CONG ::= UNARIO | CONG and UNARIO
UNARIO ::= QUANT | LETTERALE
Non è LL(k)!
Ricorsione SX in
QUANT ::= (forall | exists) var UNARIO
FBF, DISG e CONG
LETTERALE ::= ATOMO | not UNARIO
ATOMO ::= TERM | open FBF close
TIPO 2:
TERM ::= var |
Self embedding
in ATOMO e TERM
ident { open TERM { comma TERM } close }
funzione e costante:
inglobate in TERM
Se volessimo FBF vuote:
FBF → DISG | FBF(→|↔)DISG | ε
il linguaggio resterebbe di tipo2 perchè si potrebbe
eliminare del tutto l’ε-rule:
LINE → FBF ; | ;
FBF→ DISG | FBF(→|↔)DISG
Verso una grammatica LL(1)

Per poter applicare l’analisi ricorsiva discendente
si può eliminare la ricorsione sinistra da:
FBF ::= DISG | FBF (→|↔) DISG
DISG ::= CONG | DISG or CONG
CONG ::= UNARIO | CONG and UNARIO

Ad Esempio:
FBF ::= DISG | FBF (→|↔) DISG
FBF ::= DISG | DISG Z ::= DISG (ε|Z)
Z ::= (→|↔) DISG { (→|↔) DISG }
Sostituendo Z in FBF:
FBF ::= DISG (ε| (→|↔) DISG { (→|↔) DISG })
La notazione EBNF permette di esprimere ε-rules
FBF ::= DISG [ (→|↔) DISG { (→|↔) DISG }]
Ma [A{A}]={A} quindi se A=(→|↔) DISG
FBF ::= DISG { (→|↔) DISG }


Ora abbiamo un
riconoscitore
deterministico
Ora la complessità del
riconoscitore cresce
linearmente con la
lunghezza della teoria
in ingresso
Sintassi Concreta
THEORY ::= ONE_LINE | { ONE_LINE }
ONE_LINE ::= FBF semicolon
Ora associatività a
destra!
Va ancora bene per la
semantica delle
operazioni logiche
(anche se non serve
perchè non calcolo il
valore di verità)
FBF ::= DISG { (→|↔) DISG }
DISG ::= CONG { or CONG }
CONG ::= UNARIO { and UNARIO }
UNARIO ::= QUANT | LETTERALE
QUANT ::= (forall | exists) var UNARIO
LETTERALE ::= ATOMO | not UNARIO
ATOMO ::= TERM | open FBF close
TERM ::= var |
ident { open TERM { comma TERM } close }
Grammatica JavaCC
Introduzione dei non
terminali negazione e
var: utile nel visitor
VarRenamingVisitor
L’interprete
Analisi del problema

Dimostrazioni in logica dei predicati basate su procedure come

Principio di risoluzione
 Forward chaining e Backward Chaining (usato dal prolog)
 che operano (prop. di correttezza e completezza) su teorie in forma a clausole



Necessario uno step
preliminare di
trasformazione in
clausole
Algoritmo 8 passi
Ogni passo un
Visitor
ClosedFormVisitor
ImplicReductionVisitor
Analisi del problema
NegReductionVisitor
VarRenamingVisitor
Analisi del problema
QuantificationsAHeadVisitor
CongPrenexFormVisitor
SkolemVisitor
Analisi del problema
ForallRemoverVisitor
•Visitors in serie: assumono di essere
applicati solo ad espressioni con
determinate caratteristiche cioè già
visitate e trasformate da visitor
precedenti
• Visitor indipendenti: applicabili
sempre, non fanno assunzioni
Architettura

Catena di visitor (dall’analisi)


Compilatore di espressioni della logica del primo ordine in clausole
del primo ordine
Manca la costruzione dell’AST


Dump della stringa, modifiche dove servono
maggior sfruttamento possibile del tool javacc

syntax
tree
input
Maggiore rapidità di sviluppo - poca efficienza
visita A
String A
Input
String
syntax
treeA
visita B
String B
PARSER
syntax
treeB
....
visita n
String n
syntax
tree n
Oggetto VisitResult
contenente stringa e
syntaxtree
Architettura

CompilerVisitor, VisitRsult e Factory
Architettura

Schema globale
Un esempio di Visitor
Limiti – Caratteristiche non
supportate - Future Work

Concettualmente
Sintassi astratta
 Implementazione dell’unificazione e del principio di
risoluzione
 Piano collaudo


Implementazione
Visitor che genera l’AST e trasformazioni degli altri
visitor sull’AST, non sul output del parser
 Multithreading – soprattutto per GUI e pattern
Observer

Fine