Run Code
|
API
|
Code Wall
|
Misc
|
Feedback
|
Login
|
Theme
|
Privacy
|
Patreon
fCube Prover
%commands to the interpreter are submitted from stdin input ('show input' box below) %'halt.' will be automatically appended to stdin input. %swi-prolog 7.6.4 /************************************************************************************* fCube: an efficient prover for Intuitionistic propositional Logic Copyright (C) 2012 Mauro Ferrari, email: mauro.ferrari@uninsubria.it Camillo Fiorentini email: fiorenti@dsi.unimi.it Guido Fiorino email: guido.fiorino@unimib.it This program is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program. If not, see <http://www.gnu.org/licenses/>. INSTRUCTIONS Syntax: implication: im(,); negation: non(); equivalence: equiv(,); conjuncton: and(,); disjunction: or(,). Example: ((a&b)->~c) is im(and(a,b),non(c)) To decide a formula use the predicate 'decide'. For example 'decide(im(a,non(a))).'; :- op(700, xfy, <=>). :- op(600, xfy, =>). :- op(500, xfy, v). :- op(400, xfy, &). :- op(300, fy, ~). This version requires swi-prolog. *************************************************************************************/ :- use_module(library(lists)). % operator definitions (TPTP syntax) :- op( 500, fy, ~). % negation :- op(1000, xfy, &). % conjunction :- op(1100, xfy, '|'). % disjunction :- op(1110, xfy, =>). % conditional :- op(1120, xfy, <=>). % biconditional /**************************** Ottenuto da fCube-verbose-4.0 ****************************/ % Init rules gnu:- writeln('This is Fcube\nCopyright (C) 2012'), writeln('Mauro Ferrari, email: mauro.ferrari@uninsubria.it,'), writeln('Camillo Fiorentini, email: fiorenti@dsi.unimi.it'), writeln('Guido Fiorino, email: guido.fiorino@unimib.it'), writeln('This program comes with ABSOLUTELY NO WARRANTY.'), writeln('This is free software, and you are welcome to redistribute it'), writeln('under conditions GNU Public License, see <http://www.gnu.org/licenses/> for details.'). decide(X) :- gnu, intDecide(X, _, 1). intDecide(X, COUNTERMODEL, NUMERO) :- writeln('Input Formula:'), printSWFF(swff(f, X)), writeln('\n'), permanenzaSegno([swff(f, X)], StartingSet), writeln('Sign Permanence tried,input formula equivalent to: '), printSWFFSet(StartingSet, 1), orderEquivSet(StartingSet, OrderedStartingSet), time(reapply(OrderedStartingSet, COUNTERMODEL, 1, 1)), !, writeln(' '), write(NUMERO), writeln(' search result = unprovable (fCube-4.1)'), writeln('*** The Counter Model (see also the prolog term ) ***'), writeln('-- root --'), printKripke(COUNTERMODEL, 1), writeln('-- end world --'), writeln('*** Prolog term of the countermodel ***'), writeln(COUNTERMODEL). intDecide(_, [valida], NUMERO) :- writeln(' '), write(NUMERO), writeln(' search result = provable (fCube-4.1)'). /* applica la semplificazione di Massacci, con A lista dei candidati, cioè le formule appena ottenute per applicazione della regola */ semplificazioneCerta(A, B, NewerSet) :- simplification(A, B, NewSet), !, ( coerente(NewSet), permanenzaSegno(NewSet, NewerSet), ! ; NewerSet = NewSet ). semplificazioneBreve(A, B, NewSet) :- simplification(A, B, NewSet), !. semplificazioneBranch(A, B, LastSet) :- semplificazione(A, B, LastSet). semplificazione(A, B, TheMoreNewSet) :- simplification(A, B, NewSet), !, ( coerente(NewSet), permanenzaSegno(NewSet, NewerSet), !, ( coerente(NewerSet), !, clSimplification(NewerSet, TheMoreNewSet), ! ; TheMoreNewSet = NewerSet ) ; TheMoreNewSet = NewSet ). /* Dopo la semplificazione di B abbiamo un nuovo insieme, NewSet, che potrebbe avere atomi costanti. Si calcola gli atomi con segno costante. Tali atomi, se esistono diventano i nuovi candidati per la semplificazione, quindi si procede */ permanenzaSegno(NewSet, NewerSet) :- atomiConSegnoCostanteInSwffSet(NewSet, ListaAtomiConSegnoCostante), !, iteraSemplificazione(ListaAtomiConSegnoCostante, NewSet, NewerSet), !. /* se non ci sono candidati, allora non c'è nulla da semplificare */ iteraSemplificazione([], S, S). /* I candidati in [A|L] vengono concatenati all'insieme ottenuto dalla semplificazione di Massacci. Si ottiene TempSet a cui si applica la semplificazione di Massacci, ottenendo NewTempSet. A questo punto si puo' iterare il procedimento ricalcolando la permanenza del segno. */ iteraSemplificazione([A|L], NewSet, NewerSet) :- append([A|L], NewSet, TempSet), !, simplification([A|L], TempSet, NewTempSet), !, /*chiama permanenza del segno se simplification ha fatto qualche rimpiazzamento*/ chiamaPermanenzaSegno(TempSet, NewTempSet, NewerSet), !. chiamaPermanenzaSegno(TempSet, TempSet, TempSet). chiamaPermanenzaSegno(_, NewTempSet, NewerSet) :- permanenzaSegno(NewTempSet, NewerSet), !. /* NOTA: 1) TRA LE FUNZIONI LEGATE ALLA XMANENZA DEL SEGNO OCCORREREBBE METTERNA UNA CHE FILTRI LE SWFF ATOMICHE DOPPIE IN [A|L] CIOÈ IN ListaAtomiConSegnoCostante */ uguali(X, X). /*findWFFalpha, data una lista mette, se contiene una formula di tipo alpha la mette nella lista a secondo argomento e nel terzo ci mette la prima lista privata della formula alpha. */ findWFFalpha([], [], []). findWFFalpha([H|T], [H], T) :-tipoalpha(H). findWFFalpha([H|T], X, [H|Y]) :-findWFFalpha(T, X, Y). /* formule di tipo 1*/ tipoalpha(swff(t, _ & _)). tipoalpha(swff(t, _ <=> _)). tipoalpha(swff(f, _ | _)). /*tipoalpha(swff(t,im(X,_))):-atom(X).*/ /* valutare se toglierlo e gestire tale formula sempre a parte come caso speciale */ tipoalpha(swff(t, (_ & _) => _)). tipoalpha(swff(t, (_ <=> _) => _)). tipoalpha(swff(t, (_ | _) => _)). tipoalpha(swff(fc, _ | _)). tipoalpha(swff(t, ~ _)). /*formule di tipo 2*/ tipobeta(swff(f, _ & _)). tipobeta(swff(f, _ <=> _)). tipobeta(swff(t, _ | _)). /*formule di tipo 3*/ tipo3(swff(f, _ => _)). tipo3(swff(f, ~ _)). /*formule tipo4*/ tipo4(swff(t, (_ => _) =>_)). tipo4(swff(t, ~ _ => _)). /*formule tipo5*/ tipo5(swff(fc, _ => _)). tipo5(swff(fc, ~ _)). /*formule tipo6*/ tipo6(swff(fc, _ & _)). tipo6(swff(fc, _ <=> _)). /**************************************************** PREDICATI PER LA PERMANENZA DEL SEGNO ****************************************************/ /* Dato un insieme di swff determina la lista di formule atomiche con segno costante. Questo predicato implementa la regola sui segni costanti in un insieme */ atomiConSegnoCostanteInSwffSet(SwffSet, ListOfAtomicSwffs) :- segnoAtomiInSetOfSwff(SwffSet, TempSetOfVarPos, TempSetOfVarNeg), !, list_to_set(TempSetOfVarPos, SetOfVarPos), list_to_set(TempSetOfVarNeg, SetOfVarNeg), atomiConSegnoCost(SetOfVarNeg, SetOfVarPos, SwffAtomsWithConstantSign), subtract(SwffAtomsWithConstantSign, SwffSet, ListOfAtomicSwffs), !. /* I SEGUENTI SONO PREDICATI DI SUPPORTO AL PRECEDENTE */ /* Stabilisce il segno degli atomi in un insieme di formule segnate: il primo argomento è un insieme di swff il secondo argomento è la lista delle variabili segnate True il terzo argomento e' la lista delle variabili segnate False */ segnoAtomiInSetOfSwff([], [], []). /* se la formula in cima alla lista e' atomica */ segnoAtomiInSetOfSwff([swff(_, 1)|T], PositiveInCoda, NegativeInCoda) :- segnoAtomiInSetOfSwff(T, PositiveInCoda, NegativeInCoda). segnoAtomiInSetOfSwff([swff(_, 0)|T], PositiveInCoda, NegativeInCoda) :- segnoAtomiInSetOfSwff(T, PositiveInCoda, NegativeInCoda). segnoAtomiInSetOfSwff([swff(t, X)|T], [X|PositiveInCoda], NegativeInCoda) :- atom(X), segnoAtomiInSetOfSwff(T, PositiveInCoda, NegativeInCoda). segnoAtomiInSetOfSwff([swff(f, X)|T], PositiveInCoda, [X|NegativeInCoda]) :- atom(X), segnoAtomiInSetOfSwff(T, PositiveInCoda, NegativeInCoda). segnoAtomiInSetOfSwff([swff(fc, X)|T], PositiveInCoda, [X|NegativeInCoda]) :- atom(X), segnoAtomiInSetOfSwff(T, PositiveInCoda, NegativeInCoda). segnoAtomiInSetOfSwff([A|T], VarPositive, VarNegative) :- segnoAtomiInSwff(A, VarPosInA, VarNegInA), segnoAtomiInSetOfSwff(T, VarPosInCoda, VarNegInCoda), append(VarPosInA, VarPosInCoda, VarPositive), append(VarNegInA, VarNegInCoda, VarNegative). segnoAtomiInSwff(swff(t, A), VarPosInA, VarNegInA) :- segnoAtomiInSwffTrue(A, VarPosInA, VarNegInA). segnoAtomiInSwff(swff(f, A), VarPosInA, VarNegInA) :- segnoAtomiInSwffFalse(A, VarPosInA, VarNegInA). segnoAtomiInSwff(swff(fc, A), VarPosInA, VarNegInA) :- segnoAtomiInSwffFalse(A, VarPosInA, VarNegInA). /* stabilisce segno degli atomi in una formula segnata. Il segno di un atomo puo' essere positivo o negativo */ /*passo base*/ segnoAtomiInSwffTrue(X, [X], []) :-atom(X). /*passo induttivo*/ segnoAtomiInSwffTrue(X & Y, Z, Atomi) :- segnoAtomiInSwffTrue(X, L, AtomiX), segnoAtomiInSwffTrue(Y, M, AtomiY), append(L, M, Z), append(AtomiX, AtomiY, Atomi). segnoAtomiInSwffTrue(X <=> Y, Z, Z) :- variabili(X, VarX), variabili(Y, VarY), union(VarX, VarY, Z). segnoAtomiInSwffTrue((X | Y), Z, Atomi) :- segnoAtomiInSwffTrue(X, L, AtomiX), segnoAtomiInSwffTrue(Y, M, AtomiY), append(L, M, Z), append(AtomiX, AtomiY, Atomi). segnoAtomiInSwffTrue(X => Y, Z, Atomi) :- segnoAtomiInSwffFalse(X, L, AtomiX), segnoAtomiInSwffTrue(Y, M, AtomiY), append(L, M, Z), append(AtomiX, AtomiY, Atomi). segnoAtomiInSwffTrue(~X, L, Atomi) :- segnoAtomiInSwffFalse(X, L, Atomi). segnoAtomiInSwffFalse(X, [], [X]) :-atom(X). segnoAtomiInSwffFalse(X & Y, Z, Atomi) :- segnoAtomiInSwffFalse(X, L, AtomiX), segnoAtomiInSwffFalse(Y, M, AtomiY), append(L, M, Z), append(AtomiX, AtomiY, Atomi). segnoAtomiInSwffFalse(X <=> Y, Z, Z) :- variabili(X, VarX), variabili(Y, VarY), union(VarX, VarY, Z). segnoAtomiInSwffFalse((X | Y), Z, Atomi) :- segnoAtomiInSwffFalse(X, L, AtomiX), segnoAtomiInSwffFalse(Y, M, AtomiY), append(L, M, Z), append(AtomiX, AtomiY, Atomi). segnoAtomiInSwffFalse(X => Y, Z, Atomi) :- segnoAtomiInSwffTrue(X, L, AtomiX), segnoAtomiInSwffFalse(Y, M, AtomiY), append(L, M, Z), append(AtomiX, AtomiY, Atomi). segnoAtomiInSwffFalse(~X, L, Atomi) :- segnoAtomiInSwffTrue(X, L, Atomi). /*lista le variabili in una swff*/ variabili(X, [X]) :- atom(X). variabili(X & Y, L) :- variabili(X, M), variabili(Y, N), append(M, N, L). variabili(X <=> Y, L) :- variabili(X, M), variabili(Y, N), append(M, N, L). variabili(X | Y, L) :- variabili(X, M), variabili(Y, N), append(M, N, L). variabili(X => Y, L) :- variabili(X, M), variabili(Y, N), append(M, N, L). variabili(~X, L) :- variabili(X, L). /*atomiConSegnoCost,stabilisce l'elenco delle variabili che hanno segno costante: atomiConSegnoCost(SetOfVarNeg,SetOfVarPos,SwffAtomsWithConstantSign) */ atomiConSegnoCost(SetOfVarNeg, SetOfVarPos, SwffAtomsWithConstantSign) :- subtract(SetOfVarPos, SetOfVarNeg, ConstantVarPos), subtract(SetOfVarNeg, SetOfVarPos, ConstantVarNeg), buildPositiveAtomic(ConstantVarPos, ConstantPositiveAtomic), buildNegativeAtomic(ConstantVarNeg, ConstantNegativeAtomic), union(ConstantPositiveAtomic, ConstantNegativeAtomic, SwffAtomsWithConstantSign). buildPositiveAtomic([], []). buildPositiveAtomic([PropVar|Tail], [swff(t, PropVar)|Res]) :- buildPositiveAtomic(Tail, Res). buildNegativeAtomic([], []). buildNegativeAtomic([PropVar|Tail], [swff(fc, PropVar)|Res]) :- buildNegativeAtomic(Tail, Res). /* STAMPE printSWFFSet stampa una lista di formule. Il secondo parametro e' l'allineamento printSWFF stampa una formula segnata,cioe' un termine che comincia con swff; printWFF stampa una formula proposizionale */ printSWFFSet([], _). printSWFFSet([X|Y], SPAZIO) :- !, tab(SPAZIO*3), printSWFF(X), !, writeln(';'), printSWFFSet(Y, SPAZIO), !. printSWFF(swff(S, 0)) :-upcase_atom(S, K), write(K), write(' 0'). printSWFF(swff(S, 1)) :-upcase_atom(S, K), write(K), write(' 1'). printSWFF(swff(S, X)) :-upcase_atom(S, K), write(K), write(' '), printWFF(X). printWFF(X) :-atom(X), write(X). printWFF(X => Y) :-write('('), printWFF(X), !, write(' => '), printWFF(Y), !, write(')'). printWFF(X | Y) :-write('('), printWFF(X), !, write(' | '), printWFF(Y), !, write(')'). printWFF(X & Y) :-write('('), printWFF(X), !, write('&'), printWFF(Y), !, write(')'). printWFF(~ X) :-write('~'), printWFF(X), !. printWFF(X <=> Y) :-write('('), printWFF(X), !, write(' <=> '), printWFF(Y), !, write(')'). /**************************************************************** SEMPLIFICAZIONI BOOLEANE DI UNA FORMULA valTerm(termine,valore): valuta ricorsivamente un termine: se termine è atomico allora vale se stesso; se termine è non atomico viene valutato seguendo la tavola di verità del connettivo principale. ************************************************************************************************/ /*passo base: il valore di un termine atomico è se stesso */ valTerm(0, 0). valTerm(1, 1). valTerm(X, X) :-atom(X). /*passo induttivo: valore di un termine and */ valTerm(X & Y, RISP) :- valTerm(X, VALX), !, andTable(VALX, Y, RISP) /*guarda la tabella di verita' dell'AND*/, !. valTerm(X <=> Y, RISP) :- valTerm(X, VALX), valTerm(Y, VALY), equivTable(VALX, VALY, RISP), /*guarda la tabella di verita' dell'EQUIV*/ !. valTerm(X | Y, RISP) :- valTerm(X, VALX), !, /*valuta il termine di sx*/ orTable(VALX, Y, RISP) /*guarda la tabella di verita' dell'OR*/, !. valTerm(X => Y, RISP) :-valTerm(X, VALX), !, /*valuta il termine di sx*/ imTable(VALX, Y, RISP) /*guarda la tabella di verita' dell'OR*/, !. valTerm(~X, RISP) :-valTerm(X, VALX), !, nonTable(VALX, RISP). nonTable(0, 1). nonTable(1, 0). nonTable(VALX, ~ VALX). andTable(0, _, 0). /*se il congiunto di sx vale 0 allora la risposta vale 0 */ andTable(1, Y, RISP) :-valTerm(Y, RISP), !. /* se il congiunto di sx vale 1 allora la risposta vale il valore del congiunto di dx*/ andTable(VALX, Y, RISP) :-valTerm(Y, VALY), !, /*se il congiunto di sx è un termine qualsiasi allora si valuta il congiunto di dx */ andTable2(VALX, VALY, RISP). /* e si guarda la tabella dell'and lungo la colonna del secondo congiunto*/ andTable2(_, 0, 0). /* se il congiunto di dx vale 0,la risposta è 0 */ andTable2(VALX, 1, VALX). /* se vale 1,la risposta è il valore del congiunto di sx */ andTable2(VALX, VALX, VALX). andTable2(VALX, VALY, VALX & VALY). /* altrimenti il valore è l'and del valore dei 2 congiunti */ orTable(1, _, 1). /*se il congiunto di sx vale 1 allora la risposta vale 1 */ orTable(0, Y, RISP) :-valTerm(Y, RISP). /* se il congiunto di sx vale 1 allora la risposta vale il valore del congiunto di dx*/ orTable(VALX, Y, RISP) :-valTerm(Y, VALY), !, /*se il congiunto di sx è un termine qualsiasi allora si valuta il congiunto di dx */ orTable2(VALX, VALY, RISP). /* e si guarda la tabella dell'and lungo la colonna del secondo congiunto*/ orTable2(_, 1, 1). /* se il congiunto di dx vale 1,la risposta è 1 */ orTable2(VALX, 0, VALX). /* se vale 0,la risposta è il valore del congiunto di sx */ orTable2(VALX, VALX, VALX). orTable2(VALX, VALY, VALX | VALY). /* altrimenti il valore è l'and del valore dei 2 congiunti */ /*Semplificazioni per l'implica*/ /*se l'antecedente vale 0 allora l'implicazione e' una tautologia,quindi la risposta vale 1 */ imTable(0, _, 1). /* se l'antecedente vale 1 allora la risposta vale il valore del conseguente*/ imTable(1, Y, RISP) :- valTerm(Y, RISP), !. /*se l'antecedente è un termine qualsiasi,allora si valuta il conseguente */ imTable(VALX, Y, RISP) :- valTerm(Y, VALY), !, /*si decide in base al valore del conseguente*/ imTable2(VALX, VALY, RISP). /* se il conseguente vale: */ imTable2(_, 1, 1). /* 1,la risposta è 1 */ imTable2(VALX, 0, ~ VALX). /* 0,siamo nel caso VALX -> false,cioe' ~ VALX*/ imTable2(VALX, VALX, 1). /* come l'antecedente,siamo nel caso VALX->VALX,una tautologia */ imTable2(VALX, VALY, VALX => VALY). /* una wff,allora il valore è VALX->VALY */ /********************************************************** valutazione di una swff **********************************************************/ valSWFF(swff(S, X), swff(S, Y)) :-valTerm(X, Y). /*********************************************************** SOSTITUZIONE DI MASSACCI DI UNA FORMULA SEGNATA DENTRO UN'ALTRA FORMULA SEGNATA ***********************************************************/ /* data T X e S Y,esegue S Y[X/1],dove S è il segno di Y data Fc X e S Y,esegue S Y[X/0],dove ... */ massacci(swff(t, X), swff(S, Y), swff(S, RISP)) :-massacciTrue(X, Y, RISP). massacci(swff(fc, X), swff(S, Y), swff(S, RISP)) :-massacciFalsoCerto(X, Y, RISP). /* data F X e S Y,esegue S Y{X/0}, dove { } indica un rimpiazzamento che si ferma se si trova un connettivo implica o non e S e' il segno T o F MA NON Fc perche' Fc e' sinomimo di T non */ massacci(swff(f, X), swff(t, Y), swff(t, RISP)) :-massacciFalso(X, Y, RISP). massacci(swff(f, X), swff(f, Y), swff(f, RISP)) :-massacciFalso(X, Y, RISP). massacci(swff(f, _), swff(fc, Y), swff(fc, Y)). /* nelle formule Fc non vi è rimpiazzamento */ massacciTrue(X, X, 1). massacciTrue(_, 1, 1). massacciTrue(_, 0, 0). massacciTrue(_, Y, Y) :-atom(Y). massacciTrue(X, SX & DX, Y & Z) :- massacciTrue(X, SX, Y), massacciTrue(X, DX, Z). massacciTrue(X, SX <=> DX, Y <=> Z) :- massacciTrue(X, SX, Y), massacciTrue(X, DX, Z). massacciTrue(X, SX | DX, Y | Z) :- massacciTrue(X, SX, Y), massacciTrue(X, DX, Z). massacciTrue(X, SX => DX, Y => Z) :- massacciTrue(X, SX, Y), massacciTrue(X, DX, Z). massacciTrue(X, ~ SX, ~ Y) :- massacciTrue(X, SX, Y). /* data F X e S Y,esegue S Y[X/0] */ massacciFalsoCerto(X, X, 0). massacciFalsoCerto(_, 0, 0). massacciFalsoCerto(_, 1, 1). massacciFalsoCerto(_, Y, Y) :- atom(Y). massacciFalsoCerto(X, SX & DX, Y & Z) :- massacciFalsoCerto(X, SX, Y), !, massacciFalsoCerto(X, DX, Z), !. massacciFalsoCerto(X, SX <=> DX, Y <=> Z) :- massacciFalsoCerto(X, SX, Y), !, massacciFalsoCerto(X, DX, Z), !. massacciFalsoCerto(X, SX | DX, Y | Z) :- massacciFalsoCerto(X, SX, Y), !, massacciFalsoCerto(X, DX, Z), !. massacciFalsoCerto(X, SX => DX, Y => Z) :- massacciFalsoCerto(X, SX, Y), !, massacciFalsoCerto(X, DX, Z), !. massacciFalsoCerto(X, ~ SX, ~ Y) :- massacciFalsoCerto(X, SX, Y), !. /* data F X e S Y,esegue S Y{X/0} */ massacciFalso(X, X, 0). massacciFalso(_, 0, 0). massacciFalso(_, 1, 1). massacciFalso(_, Y, Y) :-atom(Y). massacciFalso(X, SX & DX, Y & Z) :- massacciFalso(X, SX, Y), !, massacciFalso(X, DX, Z), !. massacciFalso(X, SX | DX, Y | Z) :- massacciFalso(X, SX, Y), !, massacciFalso(X, DX, Z), !. massacciFalso(_, SX => DX, SX => DX). /* su implica e non il rimpiazzamento si ferma */ massacciFalso(_, SX <=> DX, SX <=> DX). /* su implica equiv e non il rimpiazzamento si ferma */ massacciFalso(_, ~ SX, ~ SX). /* * simplification(ListaCandidati,InsiemeDiSwff,InsiemeRisultato): * ListaCandidati e' l'insieme delle formule per cui si deve tentare il rimpiazzamento in * InsiemediSwff. Il risultato del rimpiazzamneto produce InsiemeRisultato. * Tipicamente la ListaCandidati e' la lista delle nuove formule generate in InsiemeDi Swff per * applicazione di una regola */ simplification([], X, X). simplification(_, X, X) :- not(coerente(X)), !. simplification([H|CANDIDATES], SWFFSET, NEWSET) :- substitute(H, SWFFSET, NEWSWFFSETFORH, NEWCANDIDATESFORH), append(CANDIDATES, NEWCANDIDATESFORH, NEWCANDIDATES), simplification(NEWCANDIDATES, NEWSWFFSETFORH, TEMPNEWSET), riprovaSimplification(H, NEWSWFFSETFORH, TEMPNEWSET, NEWSET), !. riprovaSimplification(_, NEWSWFFSETFORH, NEWSWFFSETFORH, NEWSWFFSETFORH). /* inutile tentare */ riprovaSimplification(_, _, TEMPNEWSET, TEMPNEWSET) :- not(coerente(TEMPNEWSET)). riprovaSimplification(H, _, TEMPNEWSET, NEWSET) :- simplification([H], TEMPNEWSET, NEWSET), !. /* * substitute(F,SETOFSWFF,NEWSETOFSWFF,SETOFCANDIDATES) * F formula da rimpiazzare; * SETOFSWFF insieme in cui eseguire il rimpiazzamento; * NEWSETOFSWFF insieme di formule risultante; * SETOFCANDIDATES nuovi candidati da usare per eseguire un nuovo rimpiazzamento. */ substitute(swff(_, 0), SETOFSWFF, SETOFSWFF, []) :- !. substitute(swff(_, 1), SETOFSWFF, SETOFSWFF, []) :- !. substitute(F, SETOFSWFF, SETOFSWFF, []) :- /* * se F non appartiene all'insieme non si fanno sostituzioni */ not(memberchk(F, SETOFSWFF)), !. substitute(F, SETOFSWFF, NEWSETOFSWFF, SETOFCANDIDATES) :- /* * se F appartiene all'insieme si fanno sostituzioni */ goToSubstitute(F, SETOFSWFF, NEWSETOFSWFF, SETOFCANDIDATES). /* goToSubstitute(F,[H|T],[RISP|NI],NEWCANDIDATES) rimpiazza F in [H|T]. TheReplacementResult[RISP|NI] e' il risultato del rimpiazzamento. NEWCANDIDATES sono le nuove swff generate dal rimpiazzamento di F in [H|T] */ goToSubstitute(_, [], [], []). goToSubstitute(F, [F|T], [F|NI], NC) :- !, goToSubstitute(F, T, NI, NC). goToSubstitute(F, [H|T], TheReplacementResult, NEWCANDIDATES) :- /* * esegue il rimpiazzamento H[F/val],risultato in RR */ massacci(F, H, RR), !, /* * semplificazione di RR,risultato in RISP */ valSWFF(RR, RISP), /* * TODO: se RISP e' formula contraddittoria * allora TheReplacementResult = [RISP | T] e * NEWCANDIDATES = [] * altrimenti passo ricorsivo di rimpiazzamento di F in T. * possiamo così evitare la chiamata a coerente fatta sopra. */ goToSubstitute(F, T, NI, NC), !, buidReplacementResult(RISP, NI, TheReplacementResult), !, /* * Se RISP <> da H, * allora RISP e' un nuovo candidato */ updatecandidates(NC, H, RISP, NEWCANDIDATES). /* forse qui va un ! */ buidReplacementResult(swff(t, 1), NI, NI). buidReplacementResult(swff(f, 0), NI, NI). buidReplacementResult(swff(fc, 0), NI, NI). buidReplacementResult(RISP, NI, [RISP|NI]). /* * Se H non e' stata modificata dal rimpiazzamento,allora non e' una formula candidata */ updatecandidates(NC, H, H, NC) :- !. /* * inutile mettere queste formule tra i candidati */ updatecandidates(NC, _, swff(t, 1), NC). updatecandidates(NC, _, swff(f, 0), NC). updatecandidates(NC, _, swff(fc, 0), NC). /* * inutile mettere queste formule tra i candidati,l'insieme è inconsistente */ updatecandidates(_, _, swff(t, 0), []). updatecandidates(_, _, swff(f, 1), []). updatecandidates(_, _, swff(fc, 1), []). updatecandidates(NC, _, RIS, [RIS|NC]). /************************************************************** Predicati usati per implementare la regolarita' **************************************************************/ /* valore della wfff X nella lista di swff M che funge da modello: NOTA BENE: formule del tipo swff(t,1) etc NON VENGONO CONSIDERATE */ realizzata(swff(t, WFF), M) :- atom(WFF), !, memberchk(swff(t, WFF), M). /*una F-atomica è realizzata se la corrispondente T non appartiene al modello*/ realizzata(swff(f, WFF), M) :- atom(WFF), !, not(memberchk(swff(t, WFF), M)). realizzata(swff(t, SX & DX), M) :- realizzata(swff(t, SX), M), !, realizzata(swff(t, DX), M), !. realizzata(swff(t, SX <=> DX), M) :- realizzata(swff(t, SX => DX), M), !, realizzata(swff(t, DX => SX), M), !. realizzata(swff(t, SX | _), M) :- realizzata(swff(t, SX), M), !. realizzata(swff(t, _ | DX), M) :- realizzata(swff(t, DX), M), !. realizzata(swff(t, _ => DX), M) :- realizzata(swff(t, DX), M), !. realizzata(swff(t, SX => _), M) :- realizzata(swff(f, SX), M), !. realizzata(swff(t, ~ WFF), M) :- realizzata(swff(f, WFF), M), !. realizzata(swff(f, SX | DX), M) :- realizzata(swff(f, SX), M), !, realizzata(swff(f, DX), M), !. realizzata(swff(f, SX & _), M) :- realizzata(swff(f, SX), M), !. realizzata(swff(f, _ & DX), M) :- realizzata(swff(f, DX), M), !. realizzata(swff(f, SX <=> DX), M) :- realizzata(swff(f, (SX => DX) & (DX => SX)), M), !. realizzata(swff(f, SX => DX), M) :- realizzata(swff(t, SX), M), !, realizzata(swff(f, DX), M), !. realizzata(swff(f, ~ WFF), M) :- realizzata(swff(t, WFF), M), !. /********************************************************************************* PREDICATI PER IMPLEMENTARE L'INTUIZIONISMO *********************************************************************************/ /* reapply(RESULT,MODEL) VERIFICA L'INSIEME RESULT PRIMA DI TENTARE DI COSTRUIRE IL CONTROMODELLO se RESULT E' coerente lo suddivide in 2 insiemi. BACK e RESTO. reapply fallisce se RESULT rappresenta una formula valida */ reapply(SET, MODEL, SPAZIO, IdxNewAtom) :- coerente(SET), !, buildBack(SET, BACK, RESTO), !, intControModello(BACK, RESTO, ModelOfTheRule, SPAZIO+1, WhichBranch, IdxNewAtom), !, /*SIBLINGS=nosiblings significa che */ kripke(SET, BACK, WhichBranch, ModelOfTheRule, MODEL), !. /*una delle formule di tipo 4 è stata*/ /*espansa con il ramo safe.*/ /*Questo ha rilevanza per come si*/ /*costruisce il contromodello*/ /* reapply(_,_,SPAZIO,_):- tab(3*SPAZIO-3),writeln('CLOSED SET'),fail. */ /* COSTRUISCE CONTROMODELLO INTUIZIONISTA intControModello(BACK,RESTO,COUNTERMODEL,SPAZIO,jumpbranch | safebranch,IdxNewAtom): costruisce il contromodello a BACK unione RESTO. Se il contromodello non esiste allora COUNTERMODEL contiene [no countermodel]. intControModello viene chiamato su un insieme coerente. SPAZIO: variabile usata per la stampa; jumpbranch | safebranch : specifica se la conclusione di rule ha Sc o no. L'informazione e' usata da continuaIterazione per trattare T->-> e T->non; IdxNewAtom e' un intero che serve a generare sistematicamente nuovi atomi per T->->. */ intControModello([], RESTO, Contromodello, _SPAZIO, safebranch, _) :- /* tab(3*SPAZIO-3), writeln('Open set,searching for a backtraking point...\n\n'), */ filtraNonAtomiche(RESTO, Contromodello). /* se non ci sono regole da applicare allora dato che RESTO è coerente,il contromodello è RESTO e la conclusione è considerata safe */ intControModello([swff(fperm, list(Wff, Atoms))], RESTO, MODEL, SPAZIO, WhichBranch, IdxNewAtom) :- !, /* nota che adesso rule è a 5 parametri */ rule(swff(fperm, list(Wff, Atoms)), RESTO, RESULT, WhichBranch, IdxNewAtom), write('Main SWFF: '), printSWFF(swff(f, Wff)), write(' with constant atoms: '), write(Atoms), writeln('\n'), printSWFFSet(RESULT, SPAZIO), writeln('\n'), succ(IdxNewAtom, NextIdx), reapply(RESULT, RightSuccessor, SPAZIO, NextIdx), !, filtraNonAtomiche(RightSuccessor, AtomicRightSuccessor), rimuoviAtomiOpposti(Atoms, AtomicRightSuccessor, RightSuccessorFiltered), !, union(Atoms, RightSuccessorFiltered, LeftSuccessor), /*adesso il fratello e' costruito correttamente*/ /*filtra le non Atomiche dall'insieme nodo che e' padre*/ filtraNonAtomiche([swff(f, Wff)|RESTO], RESTOFiltrato), /*incolla i due modelli in uno*/ union(RESTOFiltrato, [LeftSuccessor, AtomicRightSuccessor], MODEL). intControModello([H], RESTO, MODEL, SPAZIO, WhichBranch, IdxNewAtom) :- !, /* nota che adesso rule è a 5 parametri */ rule(H, RESTO, RESULT, WhichBranch, IdxNewAtom), write('Main SWFF: '), printSWFF(H), writeln('\n'), printSWFFSet(RESULT, SPAZIO), writeln(' '), succ(IdxNewAtom, NextIdx), reapply(RESULT, MODEL, SPAZIO, NextIdx), !. intControModello([H, T|BACK], RESTO, MODEL, SPAZIO, WhichBranch, IdxNewAtom) :- append([T|BACK], RESTO, SET), intControModello([H], SET, MODELH, SPAZIO, HWhichBranch, IdxNewAtom), !, /* ci domandiamo se davvero*/ continuaIterazione([T|BACK], [H|RESTO], MODELH, MODEL, SPAZIO, HWhichBranch, IdxNewAtom, WhichBranch), !. /* abbiamo bisogno di fare*/ /* backtracking su [T|BACK]*/ /* se H e' di tipo 4 ed il contromodello MODELH e' stato ottenuto applicando il ramo safe, allora non c'e' bisogno di alcuna iterazione ed il contromodello restituito è [] */ continuaIterazione(_, [H|_], MODELH, MODELH, _, safebranch, _, safebranch) :- tipo4(H). /* se l'intero insieme di formule sia realizzato da MODELH, allora questo è il modello dell'intero insieme e non c'e' bisogno di andare avanti con l'iterazione. L'applicazione della regola puo' essere considerata safe */ /* nota che questa condizione se attivata riguarda H di tipo 3 o 4. Nel caso di tipo 4 riguarda l'applicazione non safe della regola */ continuaIterazione([T|BACK], [_|RESTO], MODELH, NEWMODELH, _, jumpbranch, _, safebranch) :- /*ricostruisce l'insieme nodo,non considera H*/ append([T|BACK], RESTO, Set), /*estrae le formule segnate F */ falseSWFF(Set, FSWFF), /*se tutte le F-swff di SET sono classiche e*/ tutteClassiche(FSWFF), /*realizzate fermiamo il backtrack*/ insiemeRealizzato(FSWFF, MODELH), conservaTatomiche(RESTO, FilteredSet), append(FilteredSet, MODELH, NEWMODELH). /*altrimenti lo proseguiamo. Nota che quando fermiamo il backtrack è come se avessimo applicato una regola safe */ /* se il contromodello MODELH e' stato ottenuto applicando il ramo Sc, allora andiamo avanti con il backtrack */ continuaIterazione([T|BACK], [H|RESTO], MODELH, MODEL, SPAZIO, jumpbranch, IdxNewAtom, WhichBranch) :- writeln('Found a backtacking point:\n'), union([H, T|BACK], RESTO, NodeSet), printSWFFSet(NodeSet, SPAZIO-1), writeln(' '), intControModello([T|BACK], [H|RESTO], MODELRESTO, SPAZIO, WhichBranch, IdxNewAtom), !, gluesiblings(WhichBranch, BACK, MODELH, MODELRESTO, MODEL), !. gluesiblings(jumpbranch, [], MODELH, MODELRESTO, [MODELH, MODELRESTO]). gluesiblings(jumpbranch, _, MODELH, MODELRESTO, MODEL) :- append([MODELH], MODELRESTO, MODEL). gluesiblings(safebranch, _, _, MODELRESTO, MODELRESTO). /* falseSWFF(Set,FSWFF),estrae le formule segnate F */ falseSWFF([], []). falseSWFF([swff(f, X)|T], [swff(f, X)|R]) :- !, falseSWFF(T, R), !. falseSWFF([_|T], R) :- !, falseSWFF(T, R), !. /* tutteClassiche(FSWFF),stabilisce se tutte le F-swff di SET sono classiche */ tutteClassiche([]). tutteClassiche([H|T]) :- isSwffClassic(H, 1), tutteClassiche(T), !. /* insiemeRealizzato(FSWFF,MODELH),stabilisce se MODELH realizza le formule classiche di FSWFF */ insiemeRealizzato([], _). insiemeRealizzato([H|T], MODELH) :- realizzata(H, MODELH), insiemeRealizzato(T, MODELH), !. /************************************************************************ COSTRUZIONE DI UNA PARTE DEL CONTROMODELLO kripke(SET,BACK,WhichBranch,ModelOfTheRule,MODEL) SET è l'insieme di formule. Ha un ruola solo quando è un saturato, BACK nei casi in cui WhichBranch= jumpbranch permette di sapere se TheModelOfRESULT è una lista che rappresenta esattamente uno stato oppure una lista in cui ogni componente è una lista che rappresenta uno stato WhichBranch vale safebranch se RESULT è ottenuto da un ramo safe, vale jumpbranch se RESULT è ottenuto da un ramo di jump TheModelOfRESULT il modello relativo a RESULT MODEL il modello restituito, ************************************************************************/ kripke(_, _, safebranch, MODEL, MODEL). kripke(SET, [_], jumpbranch, TheModelOfRESULT, MODEL) :- filtraNonAtomiche(SET, FilteredSet), append(FilteredSet, [TheModelOfRESULT], MODEL). kripke(SET, [_, _|_], jumpbranch, TheModelOfRESULT, MODEL) :- filtraNonAtomiche(SET, FilteredSet), append(FilteredSet, TheModelOfRESULT, MODEL). kripke(_, _, _, _, _) :- writeln('CHIAMATA A KRIPKE NON CORRISPONDE'), abort. /* STAMPA IL MODELLO DI KRIPKE */ printKripke([], _). printKripke([swff(S, WFF)|T], SPAZIO) :- printSWFFSet([swff(S, WFF)], SPAZIO), !, printKripke(T, SPAZIO), !. printKripke([[X|Y]|Z], SPAZIO) :- writeln('-- end world -- '), printKripke([X|Y], SPAZIO+1), !, printKripke(Z, SPAZIO), !. printKripke([[]|Z], SPAZIO) :- writeln(' '), printKripke([swff(t, emptyNode)], SPAZIO+1), !, printKripke(Z, SPAZIO), !. printKripke(_, _) :- writeln('printKripke NON CORRISPONDE'), abort. /* coerente e' vero se la lista e' vuota oppure oppure ha solo un elemento oppure Y e' coerente e Y non contiene una formula di segno opposto a X */ coerente([]). coerente(L) :- not(memberchk(swff(t, 0), L)), not(memberchk(swff(f, 1), L)), not(memberchk(swff(fc, 1), L)). /* buildBack(SET,BACK,RESTO): costruisce l'insieme di backtrack. Se SET contiene almeno una swff di tipo 1 o 2 allora BACK ha solo 1 formula. Se non contiene formule di tipo 1 o 2 allora vengono collezionate in BACK tutte quelle di tipo 3 e 4. Se questi tipi di swff non sono presenti in SET,allora si cerca una formula di tipo 5 o 6. Se neppure formule di questo tipo esistono allora SET non è espandibile. */ buildBack(SET, [B|ACK], RESTO) :- cercaTipiAlphaBeta(SET, [B|ACK], RESTO). /* se cercaPermanenceFormula(SET,[B|ACK],RESTO) ha successo, allora B contiene una F-> formula a cui applicare una delle permanence rules */ buildBack(SET, [swff(fperm, list(X, TheConstantAtoms))], RESTO) :- cercaPermanenceFormula(SET, [swff(f, X)], RESTO, TheConstantAtoms). buildBack(SET, [B|ACK], RESTO) :- cercaBack(SET, [B|ACK], RESTO). buildBack(SET, [B|ACK], RESTO) :- cercaTipi5e6(SET, [B|ACK], RESTO). buildBack(SET, [], SET). /* attenzione: questo caso unfica anche con tutti gli altri precedenti,non è in esclusione */ /* glueModels: incolla i contromodelli */ glueModels(RADICE, SX, DX, [RADICE, SX, DX]). /* STABILISCE SE UNA SWFF E' CLASSICA */ isSwffClassic(swff(f, WFF), RISP) :- isWffClassic(WFF, RISP), !. isSwffClassic(swff(t, WFF), RISP) :- isWffClassic(WFF, RISP), !. isSwffClassic(swff(fc, _), 0). /* le Fc non sono classiche */ isWffClassic(1, 1) :- writeln('isWFFClassic chiamato con wff uguale a 1'). isWffClassic(0, 1) :- writeln('isWFFClassic chiamato con wff uguale a 0'). /* le formule 1 e 0 sono classiche,questo caso non dovrebbe mai verificarsi */ isWffClassic(WFF, 1) :-atom(WFF), !. isWffClassic(LEFT & RIGHT, 1) :- isWffClassic(LEFT, 1), !, isWffClassic(RIGHT, 1), !. isWffClassic(LEFT | RIGHT, 1) :- isWffClassic(LEFT, 1), !, isWffClassic(RIGHT, 1), !. isWffClassic(WFF, 0) :- not(isWffClassic(WFF, 1)), !. /* in tutti gli altri casi non è wff classica */ /* cercaTipiAlphaBeta(X,BACK,RESTO): cerca una formula di tipo 1 o 2 da espandere. Restituisce in BACK una formula e in RESTO le restanti formule di X cioè X=BACK unione RESTO */ cercaTipiAlphaBeta(X, BACK, RESTO) :- cercaTipiAlphaBetaModel(X, X, BACK, RESTO). /* cercaTipiAlphaBetaModel usa il primo argomento come modello,quindi non viene mai modificato */ /*passi base*/ cercaTipiAlphaBetaModel(_, [], [], []). cercaTipiAlphaBetaModel(MODEL, [swff(S, 1)|T], BACK, RESTO) :- cercaTipiAlphaBetaModel(MODEL, T, BACK, RESTOdiT), append(RESTOdiT, [swff(S, 1)], RESTO). cercaTipiAlphaBetaModel(MODEL, [swff(S, 0)|T], BACK, RESTO) :- cercaTipiAlphaBetaModel(MODEL, T, BACK, RESTOdiT), append(RESTOdiT, [swff(S, 0)], RESTO). cercaTipiAlphaBetaModel(MODEL, [swff(S, A)|T], BACK, RESTO) :- atom(A), !, cercaTipiAlphaBetaModel(MODEL, T, BACK, RESTOdiT), append(RESTOdiT, [swff(S, A)], RESTO). /*Arrivati qui sappiamo che A non è atomica */ /* CASO T->atom: si potrebbe trattare come caso speciale e tirar via dall'insieme di formule di tipo alpha, cosi' da non farlo corrispondere anche al caso seguente: L'insieme BACK conterra' una T (p->A) se T p è in X */ cercaTipiAlphaBetaModel(MODEL, [swff(t, X => Y)|B], [swff(t, X => Y)], B) :- atom(X), memberchk(swff(t, X), MODEL). cercaTipiAlphaBetaModel(_, [A|B], [A], B) :- tipoalpha(A). /*arrivati qua sappimo che A è di tipo beta*/ cercaTipiAlphaBetaModel(MODEL, [A|B], BACK, RESTO) :- tipobeta(A), /* A classica ma non realizzata,*/ isSwffClassic(A, 1), /* A e' swff tipo beta da espandere*/ not(realizzata(A, MODEL)), !, /* vediamo se troviamo una swff alpha*/ findWFFalpha(B, BACKdiB, RESTOdiB), /* predicato di supporto*/ sistema(A, B, BACKdiB, RESTOdiB, BACK, RESTO). cercaTipiAlphaBetaModel(_, [A|B], BACK, RESTO) :- tipobeta(A), /* Arrivati qui sappiamo che A e' di tipo beta */ isSwffClassic(A, 0), !, /* Arrivati qui sappiamo che A non e' classica*/ /* quindi e' da espandere*/ /* vediamo se troviamo una swff alpha*/ findWFFalpha(B, BACKdiB, RESTOdiB), /* predicato di supporto*/ sistema(A, B, BACKdiB, RESTOdiB, BACK, RESTO). /*arrivati qua sappiamo che A è di tipo beta ed è realizzata dal modello sottostante, quindi non c'e' bisogno di espanderla,cerchiamo un'altra formula nell'insieme B*/ cercaTipiAlphaBetaModel(MODEL, [A|B], BACK, RESTO) :- cercaTipiAlphaBetaModel(MODEL, B, BACK, RESTOdiB), append(RESTOdiB, [A], RESTO). /*in B non c'e' wff di tipo alpha. Allora l'insieme di backtrack è fatto dalla wff A,che è di tipo beta, la parte restante è nell'insieme B */ sistema(A, B, [], _, [A], B). /*se una wff di tipo alpha è stata trovata in B,allora l'insieme di backtracking è fatto dalla formula alpha appena trovata,RESTO è A+RESTOdiB*/ sistema(A, _, BACKdiB, RESTOdiB, BACKdiB, RESTO) :- append([A], RESTOdiB, RESTO). /* cercaBack(X,BACK,RESTO) mette in BACK le formule di X che sono di tipo 3 e 4,le restanti le mette in RESTO. Si comporta come segue: colleziona in T3 le formule di tipo3 di X,colleziona in T4 le formule di tipo 4 di X, costruisce l'insieme di backtracking secondo la seguente strategia: se T3 ha una F-formula che è l'unica F-formula di X, allora non c'e' biogno di fare backtrack e quindi BACK=T3; se X non contiene F-formule allora BACK conterra esattamente una formula di T4. Se i precedenti casi non valgono allora BACK=T3 unione T4. */ cercaBack(X, BACK, RESTO) :- prendeTipo3(X, T3, R3), prendeTipo4(R3, T4, R4), costruisciBack(T3, T4, R4, BACK, RESTO). prendeTipo3([], [], []). /* l'insieme di ricerca è vuoto */ prendeTipo3([A|T], [A|T3], R3) :- tipo3(A), !, prendeTipo3(T, T3, R3). /*se arriviamo qui A non è di tipo 3,quindi le swff di tipo 3 si trovano in T e A e' una delle formule di RESTO */ prendeTipo3([A|T], T3, [A|R3]) :- prendeTipo3(T, T3, R3). prendeTipo4([], [], []). /* l'insieme di ricerca è vuoto */ prendeTipo4([A|T], [A|T4], R4) :- tipo4(A), !, prendeTipo4(T, T4, R4). /*se arriviamo qui A non è di tipo 4,quindi le swff di tipo 4 si trovano in T e A e' una delle formule di RESTO */ prendeTipo4([A|T], T4, [A|R4]) :- prendeTipo4(T, T4, R4). costruisciBack([A], T4, R4, [A], RESTO) :- haZeroFFormule(R4), /* L'insieme X ha esattamente una swff di tipo 3 */ !, append(T4, R4, RESTO). costruisciBack([], [A|T4], R4, [A], RESTO) :- haZeroFFormule(R4), /* X ha zero F-swff,in BACK metto una swff di tipo 4 */ !, append(T4, R4, RESTO). /* qui si deve gestire anche il caso che X non abbia swff di tipo 3 e 4 */ costruisciBack(T3, T4, R4, BACK, R4) :- append(T3, T4, BACK). /* cercaTipi5e6(X,BACK,RESTO) cerca una formula di tipo 5 o 6 da espandere. Restituisce in BACK una formula e in RESTO le restanti formule di X cioè X=BACK unione RESTO */ /*passi base*/ cercaTipi5e6([], [], []). cercaTipi5e6([swff(S, 1)|T], BACK, RESTO) :- cercaTipi5e6(T, BACK, RESTOdiT), append(RESTOdiT, [swff(S, 1)], RESTO). cercaTipi5e6([swff(S, 0)|T], BACK, RESTO) :- cercaTipi5e6(T, BACK, RESTOdiT), append(RESTOdiT, [swff(S, 0)], RESTO). cercaTipi5e6([swff(S, A)|T], BACK, RESTO) :- atom(A), !, cercaTipi5e6(T, BACK, RESTOdiT), append(RESTOdiT, [swff(S, A)], RESTO). /*Arrivati qui sappiamo che A non è atomica, verifichiamo non sia una T(p->B) cioe' una swff che si comporta come un'atomica perche' nell'insieme manca T p */ cercaTipi5e6([swff(t, A => Y)|T], BACK, RESTO) :- atom(A), !, cercaTipi5e6(T, BACK, RESTOdiT), append(RESTOdiT, [swff(t, A => Y)], RESTO). cercaTipi5e6([A|B], [A], B) :- tipo5(A). /*arrivati qua sappimo che A non e' di tipo 5*/ cercaTipi5e6([A|B], BACK, RESTO) :- tipo6(A), /*trovata una swff tipo 6 da espandere*/ /*vediamo se troviamo una swff tipo 5*/ findWFFtipo5(B, BACKdiB, RESTOdiB), /*predicato di supporto*/ sistema(A, B, BACKdiB, RESTOdiB, BACK, RESTO). /* arrivati qui sappiamo che A non e' neppure di tipo 6,quindi sara' del tipo swff(t,im(p,H)), cioè una formula che si comporta come un'atomica */ cercaTipi5e6([A|B], BACK, [A|RESTOdiB]) :- cercaTipi5e6(B, BACK, RESTOdiB). findWFFtipo5([], [], []). findWFFtipo5([H|T], [H], T) :- tipo5(H). findWFFtipo5([H|T], X, [H|Y]) :- findWFFtipo5(T, X, Y). /* REGOLE INTUIZIONISTE rule(H,S,RESULT,safebranch | jumpbranch): H e' la main swff a cui applicare la regola; S e' l'insieme; NEWS e' l'insieme rislutato dopo la semplificazione safebranch se la conclusione non ha Sc,altrimenti jumpbranch */ /*regola T and*/ rule(swff(t, X & Y), S, NEWS, safebranch, _) :- !, estraiListaTAnd(X & Y, ListaAnd), union(ListaAnd, S, S1), semplificazioneBreve(ListaAnd, S1, NEWS). rule(swff(t, X <=> Y), S, NEWS, safebranch, _) :- !, semplificazioneCerta([swff(t, X => Y), swff(t, Y => X)], [swff(t, X => Y), swff(t, Y => X)|S], NEWS). /*regola T or */ rule(swff(t, X | Y), S, NEWS, safebranch, _) :- !, estraiListaTOr(X | Y, ListaOr), trattaListaTor(ListaOr, S, NEWS). /*regola T im Atom */ rule(swff(t, A => Y), S, NEWS, safebranch, _) :- atom(A), !, semplificazioneCerta([swff(t, Y)], [swff(t, Y)|S], NEWS). /*regola T im and*/ rule(swff(t, (A & B) => Y), S, NEWS, safebranch, _) :- !, semplificazioneBreve([swff(t, A => (B => Y))], [swff(t, A => (B => Y))|S], NEWS). /*regola T im equiv*/ rule(swff(t, (A <=> B) => Y), S, NEWS, safebranch, _) :- !, semplificazioneCerta([swff(t, ((A => B) & (B => A)) => Y)], [swff(t, ((A => B) & (B => A)) => Y)|S], NEWS). /*regola T im or*/ rule(swff(t, (A | B) => Y), S, NEWS, safebranch, _) :- !, semplificazioneBreve([swff(t, A => Y), swff(t, B => Y)], [swff(t, A => Y), swff(t, B => Y)|S], NEWS). /*regola T im im*/ rule(swff(t, (_ => _) => C), S, NEWS, safebranch, _) :- semplificazione([swff(t, C)], [swff(t, C)|S], NEWS), write('Right branch of T->->,'). /*regola T im im*/ rule(swff(t, (A => B) => C), S, NEWS, jumpbranch, _) :- atom(B), !, messageOnClosedSet([swff(t, (A => B) => C)|S]), write('Left branch of T->->,'), partecerta(S, SCERTO), !, semplificazione([swff(t, A), swff(f, B), swff(t, B => C)], [swff(t, A), swff(f, B), swff(t, B => C)|SCERTO], NEWS). /*regola T im im*/ rule(swff(t, (A => B) => C), S, NEWS, jumpbranch, IdxNewAtom) :- !, messageOnClosedSet([swff(t, (A => B) => C)|S]), write('Left branch of T->->,'), partecerta(S, SCERTO), !, atom_concat(newAt, IdxNewAtom, NewAtom), semplificazione([swff(t, A)], [swff(t, A), swff(f, NewAtom), swff(t, B => NewAtom), swff(t, NewAtom => C)|SCERTO], NEWS). /*regola T im non*/ rule(swff(t, ~ _ => C), S, NEWS, safebranch, _) :- semplificazione([swff(t, C)], [swff(t, C)|S], NEWS), write('Right branch of T->not,'). /*regola T im non*/ rule(swff(t, ~ A => B), S, NEWS, jumpbranch, _) :- !, messageOnClosedSet([swff(t, ~ A => B)|S]), write('Left branch of T->not,'), partecerta(S, SCERTO), !, semplificazione([swff(t, A)], [swff(t, A)|SCERTO], NEWS). /*regola T non */ rule(swff(t, ~X), S, NEWS, safebranch, _) :- !, semplificazioneBreve([swff(fc, X)], [swff(fc, X)|S], NEWS). /* F or*/ rule(swff(f, X | Y), S, NEWS, safebranch, _) :- !, estraiListaFOr(X | Y, ListaOr), union(ListaOr, S, S1), semplificazioneBreve(ListaOr, S1, NEWS). rule(swff(f, X & _), S, NEWS, safebranch, _) :- write('Left branch of F and,'), semplificazioneBranch([swff(f, X)], [swff(f, X)|S], NEWS). rule(swff(f, X & Y), S, NEWS, safebranch, _) :- !, messageOnClosedSet([swff(f, X & Y)|S]), write('Rigth branch of F and,'), semplificazioneBranch([swff(f, Y)], [swff(f, Y)|S], NEWS). rule(swff(f, X <=> Y), S, NEWS, safebranch, _) :- write('Left branch of F equiv,'), semplificazioneBranch([swff(f, X => Y)], [swff(f, X => Y)|S], NEWS). rule(swff(f, X <=> Y), S, NEWS, safebranch, _) :- !, messageOnClosedSet([swff(f, X <=> Y)|S]), write('Right branch of F equiv,'), semplificazioneBranch([swff(f, Y => X)], [swff(f, Y => X)|S], NEWS). /* F im */ rule(swff(f, X => Y), S, NEWS, jumpbranch, _) :- !, write('F->,'), partecerta(S, SCERTO), !, semplificazione([swff(t, X), swff(f, Y)], [swff(t, X), swff(f, Y)|SCERTO], NEWS). /* Fperm im: implementa le regole permanence per F-> */ rule(swff(fperm, list(XL => XR, ConstantAtoms)), S, NEWS, safebranch, _) :- !, writeln(''), write('Permanence rule applied to the F-> swff: '), printSWFF(swff(f, XL => XR)), mainConsequent(ConstantAtoms, swff(f, XL => XR), SetWithTheNewFimplica), union(SetWithTheNewFimplica, S, NEWS). /* F non */ rule(swff(f, ~X), S, NEWS, jumpbranch, _) :- !, write('F non,'), partecerta(S, SCERTO), !, semplificazione([swff(t, X)], [swff(t, X)|SCERTO], NEWS). /* Fperm non: implementa le regole permanence per F-non */ rule(swff(fperm, list(~X, ConstantAtoms)), S, NEWS, safebranch, _) :- !, write('Permanence rule applied to the F~ swff: '), printSWFF(swff(f, ~X)), mainConsequent(ConstantAtoms, swff(f, ~X), SetWithTheNewFimplica), union(SetWithTheNewFimplica, S, NEWS). /* Fc or*/ rule(swff(fc, X | Y), S, NEWS, safebranch, _) :- !, semplificazioneBreve([swff(fc, X), swff(fc, Y)], [swff(fc, X), swff(fc, Y)|S], NEWS). /* Fc and */ rule(swff(fc, X & _), S, NEWS, jumpbranch, _) :- partecerta(S, SCERTO), semplificazioneCerta([swff(fc, X)], [swff(fc, X)|SCERTO], NEWS). /* Fc and */ rule(swff(fc, X & Y), S, NEWS, jumpbranch, _) :- !, messageOnClosedSet([swff(fc, X & Y)|S]), partecerta(S, SCERTO), semplificazioneCerta([swff(fc, Y)], [swff(fc, Y)|SCERTO], NEWS). /* Fc equiv */ rule(swff(fc, X <=> Y), S, NEWS, jumpbranch, _) :- partecerta(S, SCERTO), semplificazioneCerta([swff(fc, X => Y)], [swff(fc, X => Y)|SCERTO], NEWS). /* Fc equiv */ rule(swff(fc, X <=> Y), S, NEWS, jumpbranch, _) :- !, messageOnClosedSet([swff(fc, X <=> Y)|S]), partecerta(S, SCERTO), semplificazioneCerta([swff(fc, Y => X)], [swff(fc, Y => X)|SCERTO], NEWS). /* Fc im */ rule(swff(fc, X => Y), S, NEWS, jumpbranch, _) :- !, partecerta(S, SCERTO), !, semplificazioneBreve([swff(t, X), swff(fc, Y)], [swff(t, X), swff(fc, Y)|SCERTO], NEWS). /* Fc non */ rule(swff(fc, ~X), S, NEWS, jumpbranch, _) :- !, write('Fc non,'), partecerta(S, SCERTO), !, semplificazioneBreve([swff(t, X)], [swff(t, X)|SCERTO], NEWS). /* partecerta: produce Sc dato S. Non vengono copiati T e Fc atomiche */ partecerta([], []). /* passo base */ partecerta([swff(t, X)|T], RESTO) :- atom(X), !, partecerta(T, RESTO). partecerta([swff(t, X)|T], [swff(t, X)|RESTO]) :- partecerta(T, RESTO), !. partecerta([swff(fc, X)|T], RESTO) :- atom(X), !, partecerta(T, RESTO), !. partecerta([swff(fc, X)|T], [swff(fc, X)|RESTO]) :- partecerta(T, RESTO), !. partecerta([swff(f, _)|T], RESTO) :- partecerta(T, RESTO), !. /* PREDICATI DI SUPPORTO */ haZeroFFormule([]). /* Un insieme vuoto ha zero F-swff */ haZeroFFormule([swff(t, _)|L]) :- haZeroFFormule(L). haZeroFFormule([swff(fc, _)|L]) :- haZeroFFormule(L). appartenenza(X, L, 1) :- memberchk(X, L), !. appartenenza(X, L, 0) :- not(memberchk(X, L)). wff(X) :- wffIsCorrect(X), printWFF(X). wffIsCorrect(X) :-atom(X). wffIsCorrect(X & Y) :- wffIsCorrect(X), wffIsCorrect(Y). wffIsCorrect(X <=> Y) :- wffIsCorrect(X), wffIsCorrect(Y). wffIsCorrect(X | Y) :- wffIsCorrect(X), wffIsCorrect(Y). wffIsCorrect(X => Y) :- wffIsCorrect(X), wffIsCorrect(Y). wffIsCorrect(~X) :- wffIsCorrect(X). /**************************************** * * * PREDICATI PER IL PRUNING * * * ****************************************/ /* Predicato specializzato usato per calcolare il contesto congiuntivo di una T-and */ ccTAnd(0, [swff(t, 0)]). /* aggiunto nella versione V13 */ ccTAnd(1, [swff(t, 1)]). /* aggiunto nella versione V13 */ ccTAnd(F, [swff(t, F)]) :- atom(F). ccTAnd(X & Y, SET) :- ccTAnd(X, XC), ccTAnd(Y, YC), append(XC, YC, SET). ccTAnd(WFF, [swff(t, WFF)]). /* Predicato specializzato usato per calcolare il contesto congiuntivo di una F-or */ ccFor(0, [swff(f, 0)]). /* aggiunto nella versione V13 */ ccFor(1, [swff(f, 1)]). /* aggiunto nella versione V13 */ ccFor(F, [swff(f, F)]) :- atom(F). ccFor(X | Y, SET) :- ccFor(X, XC), ccFor(Y, YC), append(XC, YC, SET). ccFor(WFF, [swff(f, WFF)]). pruningSetSwff([], []). pruningSetSwff([H|T], [HP|TP]) :- pruning(H, HP), pruningSetSwff(T, TP), !. /* CONTESTO CONGIUNTIVO DI UNA FORMULA cc(F,I),dove: F e' una formula segnata; I e' un insieme rappresentante il contesto congiuntivo */ cc(swff(S, 0), [swff(S, 0)]). /* aggiunto nella versione V13 */ cc(swff(S, 1), [swff(S, 1)]). /* aggiunto nella versione V13 */ cc(swff(S, F), [swff(S, F)]) :- atom(F). /* caso T a&B */ cc(swff(t, X & Y), C) :- cc(swff(t, X), XC), !, cc(swff(t, Y), YC), !, append(XC, YC, C). cc(swff(t, X <=> Y), C) :- cc(swff(t, (X =>Y) & (Y => X)), C), !. cc(swff(f, X | Y), C) :- cc(swff(f, X), XC), !, cc(swff(f, Y), YC), !, append(XC, YC, C). cc(swff(t, X | Y), [swff(t, X | Y)|C]) :- cc(swff(t, X), XC), cc(swff(t, Y), YC), intersection(XC, YC, C). cc(swff(f, X & Y), [swff(f, X & Y)|C]) :- cc(swff(f, X), XC), cc(swff(f, Y), YC), intersection(XC, YC, C). cc(swff(f, X <=> Y), [swff(f, X <=> Y)|C]) :- cc(swff(f, X => Y), XC), cc(swff(f, Y => X), YC), intersection(XC, YC, C). cc(swff(t, X => Y), [swff(t, X => Y)]). cc(swff(f, X => Y), [swff(f, X => Y)]). /* Vecchia Regola cc(swff(t,~X),[swff(t,~X)]). T~ e' regola che non salta,quindi il suo cc puo' stare con i cc di altre formule. Vedi anche commento relativo a pruning. */ cc(swff(t, ~X), XC) :- cc(swff(fc, X), XC). cc(swff(f, ~X), [swff(f, ~X)]). cc(swff(fc, X & Y), [swff(fc, X & Y)]). cc(swff(fc, X <=> Y), [swff(fc, X <=> Y)]). cc(swff(fc, X | Y), C) :- cc(swff(fc, X), XC), cc(swff(fc, Y), YC), append(XC, YC, C). cc(swff(fc, X => Y), [swff(fc, X => Y)]). cc(swff(fc, ~X), [swff(fc, ~X)]). /* pruning(Swff,PrunedSwff) */ pruning(swff(S, 1), swff(S, 1)). pruning(swff(S, 0), swff(S, 0)). pruning(swff(S, X), swff(S, X)) :- atom(X). pruning(swff(t, X <=> Y), PRUNED) :- pruning(swff(t, (X => Y) & (Y => X)), PRUNED). pruning(swff(t, X & Y), PRUNED) :- /*calcola il contesto congiuntivo della formula */ ccTAnd(X & Y, CCX), !, list_to_set(CCX, CCXSET), pruningSetSwff(CCXSET, CCXSetPruned), simplification(CCXSetPruned, CCXSetPruned, RES), !, list_to_set(RES, SET), /* La formula di input e' di segno T, quindi in SET ci devono essere solo sottoformule con segno T */ fromSetTotSwff(SET, H), /*esegue semplificazioni booleane*/ valSWFF(H, PRUNED). pruning(swff(t, X | Y), PRUNED) :- pruning(swff(t, X), swff(t, HX)), !, pruning(swff(t, Y), swff(t, HY)), !, cc(swff(t, HX | HY), CCX), !, list_to_set(CCX, CCXSET), simplification(CCXSET, [swff(t, (HX | HY))|CCXSET], RES), !, list_to_set(RES, SET), fromSetTotSwff(SET, H), !, valSWFF(H, PRUNED). pruning(swff(f, X | Y), PRUNED) :- ccFor(X | Y, CCX), !, list_to_set(CCX, CCXSET), pruningSetSwff(CCXSET, CCXSetPruned), simplification(CCXSetPruned, CCXSetPruned, RES), !, list_to_set(RES, SET), fromSetTofSwff(SET, H), !, valSWFF(H, PRUNED). pruning(swff(f, X <=> Y), PRUNED) :- pruning(swff(f, (X => Y) & (Y => X)), PRUNED). pruning(swff(f, X & Y), PRUNED) :- pruning(swff(f, X), swff(f, HX)), !, pruning(swff(f, Y), swff(f, HY)), !, cc(swff(f, HX & HY), CCX), !, list_to_set(CCX, CCXSET), simplification(CCXSET, [swff(f, HX & HY)|CCXSET], RES), !, list_to_set(RES, SET), fromSetTofSwff(SET, H), !, valSWFF(H, PRUNED). pruning(swff(f, X => Y), PRUNED) :- /*semplifica sottoformula sx*/ pruning(swff(t, X), HX), !, pruning(swff(f, Y), HY), !, /*calcola i contesti congiuntivi*/ cc(HX, CCX), !, cc(HY, CCY), !, union(CCX, CCY, L), list_to_set(L, LSET), /*applica la semplificazione*/ simplification(LSET, LSET, RES), !, list_to_set(RES, SET), /*si prepara a ricostruire la swff*/ convertFcIntoTSWff(SET, SETOK), !, estraeTSWff(SETOK, TSwffs), subtract(SETOK, TSwffs, FSwffs), /*costruisce antecedente*/ fromSetTotSwff(TSwffs, swff(t, TH)), !, /*costruisce conseguente*/ fromSetTofSwff(FSwffs, swff(f, FH)), !, /*esegue valutazione booleana*/ valSWFF(swff(f, TH => FH), PRUNED). pruning(swff(t, X => Y), PRUNED) :- pruning(swff(f, X), swff(f, HX)), !, pruning(swff(t, Y), swff(t, HY)), !, valSWFF(swff(t, HX => HY), PRUNED). pruning(swff(f, ~X), PRUNED) :- pruning(swff(t, X), swff(t, HX)), !, valSWFF(swff(f, ~ HX), PRUNED). pruning(swff(t, ~X), PRUNED) :- pruning(swff(fc, X), swff(fc, HX)), !, valSWFF(swff(t, ~ HX), PRUNED). pruning(swff(fc, ~X), PRUNED) :- pruning(swff(t, X), swff(t, HX)), !, valSWFF(swff(fc, ~ HX), PRUNED). pruning(swff(fc, X => Y), PRUNED) :- pruning(swff(t, X), HX), !, pruning(swff(fc, Y), HY), !, /*calcola i contesti congiuntivi*/ cc(HX, CCX), !, cc(HY, CCY), !, union(CCX, CCY, L), list_to_set(L, LSET), /*applica la semplificazione*/ simplification(LSET, LSET, RES), !, list_to_set(RES, SET), /*si prepara a ricostruire la swff*/ estraeTSWff(SET, TSwffs), !, subtract(SET, TSwffs, FcSwffs), /*costruisce antecedente*/ fromSetTotSwff(TSwffs, swff(t, TH)), !, /*costruisce conseguente*/ fromSetTofcSwff(FcSwffs, swff(fc, FH)), !, /*esegue valutazione booleana*/ valSWFF(swff(fc, TH => FH), PRUNED). pruning(swff(fc, X | Y), PRUNED) :- pruning(swff(fc, X), swff(fc, HX)), !, pruning(swff(fc, Y), swff(fc, HY)), !, cc(swff(fc, HX | HY), CCX), !, list_to_set(CCX, CCXSET), simplification([swff(fc, HX), swff(fc, HY)|CCXSET], [swff(fc, HX), swff(fc, HY)|CCXSET], RES), !, list_to_set(RES, SET), fromSetTofcSwff(SET, H), !, valSWFF(H, PRUNED). pruning(swff(fc, X <=> Y), PRUNED) :- pruning(swff(fc, (X => Y) & (Y => X)), PRUNED). pruning(swff(fc, X & Y), PRUNED) :- pruning(swff(fc, X), swff(fc, HX)), !, pruning(swff(fc, Y), swff(fc, HY)), !, valSWFF(swff(fc, HX & HY), PRUNED). /******************************* Versione piu' "aggressiva",non so se corretta. Inoltre,bisogna considerare se vogliamo calcolare il cc di un insieme S di formule. Con l'attuale implementazione di pruningSetSwff la parte qui sotto potrebbe essere corretta. Se la fc-wff e' una sottoformula di un albero allora e' sottoformula segnata di una formula certa e tutte le formule del contesto congiuntivo a cui essa potenzialemte appartiene sono certe, quindi il salto della regola Fc AND non fa sparire formule del contesto congiuntivo cc(swff(fc,and(HX,HY)),CCX),!, list_to_set(CCX,CCXSET), simplification(CCXSET,[swff(f,and(HX,HY))|CCXSET],RES),!, list_to_set(RES,SET), fromSetTofSwff(SET,H),!, valSWFF(H,PRUNED). ********************************************** */ pruning(X, Y) :- write('chiamata a pruning('), write(X), write(','), write(Y), write(') fallita'), abort. estraeTSWff([], []). estraeTSWff([swff(t, X)|T], [swff(t, X)|RES]) :- estraeTSWff(T, RES), !. estraeTSWff([swff(f, _)|T], RES) :- estraeTSWff(T, RES), !. estraeTSWff([swff(fc, _)|T], RES) :- estraeTSWff(T, RES), !. /* caso aggiunto in V13*/ estraeTSWff(_, _) :- writeln('*** CASO NON PREVISTO IN estraeTSWff ***'), abort. /*fromSetTotSwff([],_):- writeln('ERRORE IN fromSetTotSwff'),abort.*/ fromSetTotSwff([], swff(t, 1)). /* modificato in V13 */ fromSetTotSwff([swff(t, X)], swff(t, X)). fromSetTotSwff([swff(fc, X)], swff(t, ~X)). /* caso aggiunto in V13 */ fromSetTotSwff([swff(t, X)|RES], swff(t, X & Y)) :- fromSetTotSwff(RES, swff(t, Y)), !. fromSetTotSwff([swff(fc, X)|RES], swff(t, ~X & Y)) :- fromSetTotSwff(RES, swff(t, Y)), !. /* caso aggiunto in V13*/ fromSetTotSwff(X, _) :- write('ERRORE IN fromSetTotSwff('), write(X), write(')'), abort. /*fromSetTofSwff([],_):- writeln('ERRORE IN fromSetTofSwff'),abort.*/ fromSetTofSwff([], swff(f, 0)). fromSetTofSwff([swff(f, X)], swff(f, X)). fromSetTofSwff([swff(f, X)|RES], swff(f, X | Y)) :- fromSetTofSwff(RES, swff(f, Y)), !. fromSetTofSwff(X, _) :- write('ERRORE IN fromSetTofSwff('), write(X), write(')'), abort. /*fromSetTofcSwff([],_):- writeln('ERRORE IN fromSetTofSwff'),abort.*/ fromSetTofcSwff([], swff(fc, 0)). fromSetTofcSwff([swff(fc, X)], swff(fc, X)). fromSetTofcSwff([swff(fc, X)|RES], swff(fc, X | Y)) :- fromSetTofcSwff(RES, swff(fc, Y)), !. fromSetTofcSwff(X, _) :- write('ERRORE IN fromSetTofSwff('), write(X), write(')'), abort. convertFcIntoTSWff([], []). convertFcIntoTSWff([swff(fc, X)|T], [swff(t, ~X)|R]) :- convertFcIntoTSWff(T, R), !. convertFcIntoTSWff([swff(t, X)|T], [swff(t, X)|R]) :- convertFcIntoTSWff(T, R), !. convertFcIntoTSWff([swff(f, X)|T], [swff(f, X)|R]) :- convertFcIntoTSWff(T, R), !. convertFcIntoTSWff(X, _) :- write('ERRORE IN convertFcIntoTSWff('), write(X), write(')'), abort. /* PERMANENZA DEL SEGNO PER FORMULE CLASSICHE */ /* Preso Set ne esegue la semplificazione classica, il risultato è in NewSet. */ clSimplification(Set, NewSet) :- buildFalseAtomicSwffs(Set, SetOfFalseAtomicSwffs), union(Set, SetOfFalseAtomicSwffs, SimpSet), simplification(SetOfFalseAtomicSwffs, SimpSet, NewSet). /* Costruisce le swff atomiche date le variabili con segno costante nella parte classica di Set */ buildFalseAtomicSwffs(Set, SetOfFalseAtomicSwffs) :- clVarsOfASet(Set, Posive, Negative), subtract(Negative, Posive, TheFalseVars), fromFalseVarsToFalseAtomicSwffs(TheFalseVars, SetOfFalseAtomicSwffs). /* Dato l'insieme a primo argomento calcola le variabili positive e quelle negative che compaiono nella parte classica,mettendole a secondo e terzo argomento */ clVarsOfASet([], [], []). clVarsOfASet([A|T], PositiveVars, NegativeVars) :- clVarsInSWFF(A, PosVarsInA, NegVarsInA), clVarsOfASet(T, PosVarsInT, NegVarsInT), union(PosVarsInA, PosVarsInT, PositiveVars), union(NegVarsInA, NegVarsInT, NegativeVars). clVarsInSWFF(swff(t, A), PosVarsInA, NegVarsInA) :- clVarsInSWFFTrue(A, PosVarsInA, NegVarsInA), !. clVarsInSWFF(swff(f, A), [], []) :- atomic(A), !. clVarsInSWFF(swff(f, A), PosVarsInA, NegVarsInA) :- clVarsInSWFFFalse(A, PosVarsInA, NegVarsInA), !. clVarsInSWFF(swff(fc, _), [], []). /* data la swff,mette le variabili classiche positive nell'insieme a primo argomento,quelle negative a secondo. */ clVarsInSWFFTrue(1, [], []). clVarsInSWFFTrue(0, [], []). clVarsInSWFFTrue(X, [X], []) :- atom(X). clVarsInSWFFTrue(X & Y, PosVars, NegVars) :- clVarsInSWFFTrue(X, PVarsX, NVarsX), clVarsInSWFFTrue(Y, PVarsY, NVarsY), union(PVarsX, PVarsY, PosVars), union(NVarsX, NVarsY, NegVars). clVarsInSWFFTrue(X <=> Y, PosVars, NegVars) :- clVarsInSWFFTrue(X, PVarsX, NVarsX), clVarsInSWFFTrue(Y, PVarsY, NVarsY), union(PVarsX, PVarsY, PosVars), union(NVarsX, NVarsY, NegVars). clVarsInSWFFTrue(X | Y, PosVars, NegVars) :- clVarsInSWFFTrue(X, PVarsX, NVarsX), clVarsInSWFFTrue(Y, PVarsY, NVarsY), union(PVarsX, PVarsY, PosVars), union(NVarsX, NVarsY, NegVars). clVarsInSWFFTrue(_ => Y, PosVars, NegVars) :- clVarsInSWFFTrue(Y, PosVars, NegVars). clVarsInSWFFTrue(~ _, [], []). clVarsInSWFFFalse(1, [], []). clVarsInSWFFFalse(swff(f, 0), [], []). clVarsInSWFFFalse(X, [], [X]) :- atom(X). clVarsInSWFFFalse(X & Y, PosVars, NegVars) :- clVarsInSWFFFalse(X, PVarsX, NVarsX), clVarsInSWFFFalse(Y, PVarsY, NVarsY), union(PVarsX, PVarsY, PosVars), union(NVarsX, NVarsY, NegVars). clVarsInSWFFFalse(X | Y, PosVars, NegVars) :- clVarsInSWFFFalse(X, PVarsX, NVarsX), clVarsInSWFFFalse(Y, PVarsY, NVarsY), union(PVarsX, PVarsY, PosVars), union(NVarsX, NVarsY, NegVars). clVarsInSWFFFalse(_ => _, [], []). clVarsInSWFFFalse(_ <=> _, [], []). clVarsInSWFFFalse(~ _, [], []). fromFalseVarsToFalseAtomicSwffs([], []). /* Se non ci sono variabili classiche costanti nulla è costruito */ fromFalseVarsToFalseAtomicSwffs([A|T], [swff(f, A)|SetOfFalseAtomicSwffsInT]) :- fromFalseVarsToFalseAtomicSwffs(T, SetOfFalseAtomicSwffsInT). cercaPermanenceFormula(Set, [TheMainPremise], Resto, [Atom|MoreAtoms]) :- partecerta(Set, Sc), /* Sc e' la parte certa di S */ length(Sc, SizeSc), SizeSc > 0, subtract(Set, Sc, Sf), /* Sf contiene solo F-formule */ length(Sf, SizeSf), /* se c'e' solo una F-formula allora */ SizeSf > 1, /* l'eventuale applicazione di F-> e F-not è invertibile */ prendeTipo3(Sf, Tipo3, _), /*_ contiene solo F-atomic formulas*/ findMainPremise(Sc, Tipo3, TheMainPremise, [Atom|MoreAtoms]), subtract(Set, [TheMainPremise], Resto). findMainPremise(Sc, [Swff|_], Swff, TheConstantAtoms) :- atomiConSegnoCostanteInSwffSet([Swff|Sc], [Atom|MoreAtoms]), atomiConSegnoCostanteInSwffSet([Swff], [SwffAtom|SwffMoreAtoms]), intersection([Atom|MoreAtoms], [SwffAtom|SwffMoreAtoms], [HeadAtom|TailAtoms]), list_to_set([HeadAtom|TailAtoms], TheConstantAtoms), !. findMainPremise(Sc, [_|TailTipo3], Swff, TheConstantAtoms) :- findMainPremise(Sc, TailTipo3, Swff, TheConstantAtoms). /* Per ogni atomo in Atoms,rimuove l'eventuale opposto in RightSuccessor. Opposti indesiderati vengono generati da PermanenzaSegno. */ rimuoviAtomiOpposti(Atoms, Model, FilteredModel) :- atomiOpposti(Atoms, AtomiOpposti), modelloFiltrato(Model, AtomiOpposti, FilteredModel). modelloFiltrato([], _, []). /* * * Versione 2.0 * */ modelloFiltrato([swff(_, Wff)|T], AtomiOpposti, FilteredModel) :- not(atomic(Wff)), !, modelloFiltrato(T, AtomiOpposti, FilteredModel). modelloFiltrato([swff(S, Wff)|T], AtomiOpposti, FilteredModel) :- memberchk(swff(S, Wff), AtomiOpposti), !, modelloFiltrato(T, AtomiOpposti, FilteredModel). modelloFiltrato([swff(S, Wff)|T], AtomiOpposti, [swff(S, Wff)|FilteredModel]) :- modelloFiltrato(T, AtomiOpposti, FilteredModel). modelloFiltrato([[X|Y]|Z], AtomiOpposti, [FilteredFirst|FilteredTail]) :- !, modelloFiltrato([X|Y], AtomiOpposti, FilteredFirst), !, modelloFiltrato(Z, AtomiOpposti, FilteredTail), !. modelloFiltrato([[]|Z], AtomiOpposti, [FilteredFirst|FilteredTail]) :- modelloFiltrato([], AtomiOpposti, FilteredFirst), modelloFiltrato(Z, AtomiOpposti, FilteredTail). atomiOpposti([], []). atomiOpposti([swff(t, X)|TailAtoms], [swff(fc, X)|TailOpposti]) :- atomiOpposti(TailAtoms, TailOpposti). atomiOpposti([swff(fc, X)|TailAtoms], [swff(t, X)|TailOpposti]) :- atomiOpposti(TailAtoms, TailOpposti). mainConsequent([], H, [H]). mainConsequent([SignedAtom|TailOfAtoms], TheSwff, SetWithTheNewFimplica) :- substitute(SignedAtom, [SignedAtom, TheSwff], Res, _), checkTheSubstitute(SignedAtom, TailOfAtoms, Res, SetWithTheNewFimplica). checkTheSubstitute(SignedAtom, TailOfAtoms, Res, SetWithTheNewFimplica) :- subtract(Res, [SignedAtom], [TheNewSwff]), !, mainConsequent(TailOfAtoms, TheNewSwff, SetWithTheNewFimplica). checkTheSubstitute(_, _, _, []). /*equivTable(X,X,1).*/ equivTable(0, 0, 1). equivTable(0, 1, 0). equivTable(0, X, ~X). equivTable(1, 0, 0). equivTable(1, 1, 1). equivTable(1, X, X). equivTable(X, 0, ~X). equivTable(X, 1, X). equivTable(X, Y, X <=> Y). filtraNonAtomiche([], []) :- !. /* Nel modello teniamo le atomiche */ filtraNonAtomiche([swff(S, Wff)|T], [swff(S, Wff)|Result]) :- atomic(Wff), !, filtraNonAtomiche(T, Result). /* Eliminiamo le NON atomiche */ filtraNonAtomiche([swff(_, _)|T], Result) :- !, filtraNonAtomiche(T, Result). /* Se arriviamo qui il primo elemento della lista è una lista e quindi non filtriamo nulla */ filtraNonAtomiche(H, H). messageOnClosedSet(_). /*:- writeln('\nBack to the branching point:\n'), printSWFFSet(SetToPrint,1), writeln(' ').*/ conservaTatomiche([], []) :- !. /* Nel modello teniamo le T-atomiche */ conservaTatomiche([swff(t, Wff)|T], [swff(t, Wff)|Result]) :- atomic(Wff), !, conservaTatomiche(T, Result). /* Eliminiamo le NON atomiche */ conservaTatomiche([swff(_, _)|T], Result) :- !, conservaTatomiche(T, Result). /* Se arriviamo qui il primo elemento della lista è una lista e quindi non filtriamo nulla */ conservaTatomiche(_, _) :- writeln('*** ERRORE IN conservaTatomiche ***'), abort. estraiListaTAnd(X & Y, ListaAnd) :- !, estraiListaTAnd(X, ListaX), estraiListaTAnd(Y, ListaY), union(ListaX, ListaY, ListaAnd). estraiListaTAnd(X, [swff(t, X)]). estraiListaTOr((X | Y), ListaAnd) :- !, estraiListaTOr(X, ListaX), estraiListaTOr(Y, ListaY), union(ListaX, ListaY, ListaAnd). estraiListaTOr(X, [swff(t, X)]). estraiListaFOr((X | Y), ListaOr) :- !, estraiListaFOr(X, ListaX), estraiListaFOr(Y, ListaY), union(ListaX, ListaY, ListaOr). estraiListaFOr(X, [swff(f, X)]). estraiListaFAnd(X & Y, ListaOr) :- !, estraiListaFAnd(X, ListaX), estraiListaFAnd(Y, ListaY), union(ListaX, ListaY, ListaOr). estraiListaFAnd(X, [swff(f, X)]). trattaListaTor([swff(t, X)], S, NEWS) :- semplificazioneBranch([swff(t, X)], [swff(t, X)|S], NEWS), write('Branch of T or,Disjunct: '), printWFF(X), write(' of '). trattaListaTor([swff(t, X), swff(t, Y)|ListaOr], S, NEWS) :- ( semplificazioneBranch([swff(t, X)], [swff(t, X)|S], NEWS), write('Branch of T or,Disjunct: '), printWFF(X), write(' of ') ; messageOnClosedSet([swff(t, X)|S]), trattaListaTor([swff(t, Y)|ListaOr], S, NEWS) ). orderEquiv(X <=> Y, Res) :- orderEquiv(X, ResX), orderEquiv(Y, ResY), ( ResX @< ResY, !, Res = (ResX <=> ResY) ; Res = (ResY <=> ResX) ). orderEquiv(X & Y, Res) :- orderEquiv(X, ResX), orderEquiv(Y, ResY), ( ResX @< ResY, !, Res = (ResX & ResY) ; Res = (ResY & ResX) ). orderEquiv((X | Y), Res) :- orderEquiv(X, ResX), orderEquiv(Y, ResY), ( ResX @< ResY, !, Res = (ResX | ResY) ; Res = (ResY | ResX) ). orderEquiv(X => Y, ResX => ResY) :- orderEquiv(X, ResX), orderEquiv(Y, ResY). orderEquiv(~X, ~ ResX) :- orderEquiv(X, ResX). orderEquiv(X, X) :- atom(X). orderEquivSet([], []). orderEquivSet([swff(Sign, H)|T], [swff(Sign, H1)|T1]) :- orderEquiv(H, H1), orderEquivSet(T, T1).
run
|
edit
|
history
|
help
0
Astar
ARREGLOS
decisiones anidadas
Tarea1 Polizona
Intento de tarea 1
Arreglos
primerprograma
Object with array
Amish
prolog 2da operación