FOLExpr Analyzer

Un riconoscitore di teorie della logica del primo ordine per la loro conversione in forma a clausole

Linguaggi e Modelli Computazionali LS - Prof E.Denti

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 tokenPossibili categorie di token

Possibili keywordsPossibili keywords

Analisi del Problema Dai lucidi del corso di Intelligenza Artificiale

LexerLexer

LexerLexer

Funzioni n-arie e predicati sono

sintatticamente identici, cambia solo la loro semantica nel senso di vero/falso

(fuori dallo scope del progetto)

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 terminaleAtomo

Parser: simbolo

non terminaleAtomo

Parser: simbolo

non terminaleTermine

Parser: simbolo

non terminaleTermine

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 ;

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

terminaleLetterale

Parser: simbolo non

terminaleLetterale

Analisi del Problema Dai lucidi del corso di Intelligenza Artificiale

Interprete: due possibili

manipo1lazioni

Interprete: due possibili

manipo1lazioni

La parte di grammatica derivata direttamente dal testo non va bene ma del

resto siamo ancora in fase di analisi...

La parte di grammatica derivata direttamente dal testo non va bene ma del

resto siamo ancora in fase di analisi...

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 ParserTHEORY ::= ONE_LINE | { ONE_LINE }ONE_LINE ::= FBF semicolon

FBF ::= DISG | FBF (→|↔) DISGDISG ::= CONG | DISG or CONGCONG ::= UNARIO | CONG and UNARIOUNARIO ::= QUANT | LETTERALEQUANT ::= (forall | exists) var UNARIOLETTERALE ::= ATOMO | not UNARIOATOMO ::= TERM | open FBF closeTERM ::= var |

ident { open TERM { comma TERM } close }

funzione e costante:

inglobate in TERM

Non è LL(k)!Ricorsione SX in

FBF, DISG e CONG

Associatività a sx: ok! date le proprietà delle

operazioni logiche

Regole di precedenza descritte nei lucidi

rispettate!

TIPO 2:Self embedding

in ATOMO e 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:

Ora abbiamo un riconoscitore deterministico

Ora la complessità del riconoscitore cresce linearmente con la lunghezza della teoria in ingresso

FBF ::= DISG | FBF (→|↔) DISG DISG ::= CONG | DISG or CONGCONG ::= UNARIO | CONG and UNARIO

FBF ::= DISG | FBF (→|↔) DISG DISG ::= CONG | DISG or CONGCONG ::= UNARIO | CONG and UNARIO

FBF ::= DISG | FBF (→|↔) DISGFBF ::= DISG | FBF (→|↔) DISG

Ad Esempio:

FBF ::= DISG | DISG Z ::= DISG (ε|Z)Z ::= (→|↔) DISG { (→|↔) DISG }

FBF ::= DISG | DISG Z ::= DISG (ε|Z)Z ::= (→|↔) DISG { (→|↔) DISG }

Sostituendo Z in FBF:FBF ::= DISG (ε| (→|↔) DISG { (→|↔) DISG })

La notazione EBNF permette di esprimere ε-rulesFBF ::= DISG [ (→|↔) DISG { (→|↔) DISG }]

Ma [A{A}]={A} quindi se A=(→|↔) DISG FBF ::= DISG { (→|↔) DISG }

Sostituendo Z in FBF:FBF ::= DISG (ε| (→|↔) DISG { (→|↔) DISG })

La notazione EBNF permette di esprimere ε-rulesFBF ::= DISG [ (→|↔) DISG { (→|↔) DISG }]

Ma [A{A}]={A} quindi se A=(→|↔) DISG FBF ::= DISG { (→|↔) DISG }

Sintassi Concreta

THEORY ::= ONE_LINE | { ONE_LINE }ONE_LINE ::= FBF semicolon

FBF ::= DISG { (→|↔) DISG }DISG ::= CONG { or CONG }CONG ::= UNARIO { and UNARIO }UNARIO ::= QUANT | LETTERALEQUANT ::= (forall | exists) var UNARIOLETTERALE ::= ATOMO | not UNARIOATOMO ::= TERM | open FBF closeTERM ::= var |

ident { open TERM { comma TERM } close }

Ora associatività a destra!

Va ancora bene per la semantica delle

operazioni logiche (anche se non serve perchè non calcolo il

valore di verità)

Ora associatività a destra!

Va ancora bene per la semantica delle

operazioni logiche (anche se non serve perchè non calcolo il

valore di verità)

Grammatica JavaCC

Introduzione dei non terminali negazione e var: utile nel visitor VarRenamingVisitor

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

VarRenamingVisitor

VarRenamingVisitor

NegReductionVisitorNegReductionVisitor

Analisi del problema

CongPrenexFormVisitor

QuantificationsAHeadVisitor

SkolemVisitor

Analisi del problema

ForallRemoverVisitorForallRemoverVisitor

•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

•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

Maggiore rapidità di sviluppo - poca efficienza

PARSERPARSERInputString

String A

visita Asyntaxtreeinput

syntaxtreeA String B

visita B

syntaxtreeB

...

. String n

visita n

syntaxtree n

Oggetto VisitResultcontenente 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