Implementação de Tablôs Analíticos em Prolog (versão SWI 5.6.55)

% Autor: Adolfo Neto % Data: 24/6/2008 % Implementação de Tablôs Analíticos prova_e_mostra_resultado(Suposicoes,Objetivo,Resultado):- geraFormulasAssinaladas(Suposicoes, Objetivo, Tablo), tenta_provar_inicio(Tablo,Resultado), ! . %Definição dos operadores :-op(510, fx, [~]). :-op(520,xfy, [/\]). :-op(530,xfy, [\/]). :-op(540,xfy, [->]). :-op(550,xfy, [?]). % se o tablô estiver fechado, encerra aqui esta_fechado(Tablo):- fechado(Tablo),!. esta_fechado(_):- fail,!. tenta_provar_inicio(Tablo,Resultado):- aplicaAlphasRemovendoDuplicatas(Tablo,Tablo2), tenta_provar(Tablo2,Resultado),!. tenta_provar(Tablo,'FECHADO'):- esta_fechado(Tablo),!. tenta_provar(Tablo,Resultado):- aplicaBeta(Tablo,Tablo_B1,Tablo_B2,'SIM'), tenta_provar_inicio(Tablo_B1, 'FECHADO'), tenta_provar_inicio(Tablo_B2, Resultado), ! . tenta_provar(_,'ABERTO'):-!. aplicaAlphasRemovendoDuplicatas(Tablo,Tablo2):- aplicaTodasAsAlphas(Tablo,Tablo2B), list_to_set(Tablo2B,Tablo2). fechado(Tablo):-member(t(X),Tablo),member(f(X),Tablo). geraFormulasAssinaladas([],O,[f(O)]). geraFormulasAssinaladas([C|R],O,[t(C)|X]):- geraFormulasAssinaladas(R,O,X). aplicaAlphas([],[]). aplicaAlphas([C|R],X):- aplicaRegraAlpha(C,X1), aplicaAlphas(R,X2), append(X1,X2,X). aplicaTodasAsAlphas(Tablo1,Tablo2):- aplicaAlphas(Tablo1,X), (not(listas_iguais(X,Tablo1)) -> aplicaTodasAsAlphas(X,Tablo2) ; Tablo2 = X ) . listas_iguais(X,Y):-subset(X,Y),subset(Y,X). aplicaRegraAlpha(t(A/\B), [t(A),t(B)]). aplicaRegraAlpha(f(A\/B), [f(A),f(B)]). aplicaRegraAlpha(f(A->B), [t(A),f(B)]). aplicaRegraAlpha( f(~A), [t(A)] ). aplicaRegraAlpha( t(~A), [f(A)] ). aplicaRegraAlpha(X, [X]). aplicaBeta([],[],[],'NAO'):-fail. aplicaBeta([C|R],X,Y,'SIM'):- aplicaRegraBeta(C,B1,B2) -> append([B1],R,X), append([B2],R,Y) . aplicaBeta([C|R],X,Y,Z):- aplicaBeta(R,X1,Y1,Z) -> append([C],X1,X), append([C],Y1,Y) . aplicaRegraBeta(f(A/\B), f(A), f(B)). aplicaRegraBeta(t(A\/B), t(A), t(B)). aplicaRegraBeta(t(A->B), f(A), t(B)). % Exemplos básicos - Resultado esperado %prova_e_mostra_resultado([a,a->b],b,X). % FECHADO %prova_e_mostra_resultado([a,a->b],a,X). % FECHADO % Exemplos retirados do livro de Da Silva et al %prova_e_mostra_resultado([],(p/\(~p)),X). % ABERTO %prova_e_mostra_resultado([],(p\/(~p)),X). %p.52 []?(p\/(~p)). - FECHADO %prova_e_mostra_resultado([p->q,q->r],(p->r),X). %p.52 [p->q,q->r]?(p->r). - FECHADO %prova_e_mostra_resultado([p,(p/\q)->r],r,X).%p.53 [p,(p/\q)->r]?r. - ABERTO %prova_e_mostra_resultado([p\/q,p->r,q->(r\/s)],r,X).%pp.53-54 [p\/q,p->r,q->(r\/s)]?r. - ABERTO %prova_e_mostra_resultado([p\/q,p->r,q->r],r,X).%p.55 FECHADO %prova_e_mostra_resultado([(~q)->(~p)],p->q,X). %p.55 2.10 (a) FECHADO % Exemplo mais difícil: PHP_3 (FECHADO) %prova_e_mostra_resultado([],(((p00\/p01\/p02)/\(p10\/p11\/p12)/\(p20\/p21\/p22)/\(p30\/p31\/p32))->((p00/\p10)\/(p00/\p20)\/(p00/\p30)\/(p10/\p20)\/(p10/\p30)\/(p20/\p30)\/(p01/\p11)\/(p01/\p21)\/(p01/\p31)\/(p11/\p21)\/(p11/\p31)\/(p21/\p31)\/(p02/\p12)\/(p02/\p22)\/(p02/\p32)\/(p12/\p22)\/(p12/\p32)\/(p22/\p32))),X).