A avaliação da disciplina é realizada por exame final, sendo que a realização de fichas práticas ao longo do semestre permite a dispensa de parte desse exame (30%).
Temos então duas modalidades de avaliação:
Modalidade A: exame final com peso 70% e avaliação prática com peso 30% (ambas com nota mínima de 9 valores)
Modalidade B: exame final com peso 100%.
As melhorias de nota serão sempre realizadas na modalidade B.
Classificações finais superiores a 16 devem ainda contar com a realização de um pequeno projecto prático, cuja avaliação será incorporada na nota final com um peso de 20%.
Durante o período lectivo far-se-ão dois testes: um sensivelmente a meio do semestre e outro no final. Ambos os testes incluem uma componente teórica e outra prática (Prolog). O peso relativo de cada uma dessas componentes será aproximadamente 70 e 30%.
Opcionalmente, os alunos podem ainda realizar um pequeno projecto prático, cuja avaliação será incorporada na nota final com um peso de 20%. Nas notas finais superiores a 16 valores esta componente será sempre considerada (querendo dizer que a nota é majorada a 16 valores se não se realizar o dito projecto).
A avaliação da disciplina consiste nas seguintes componentes:
Realização de uma prova individual escrita com nota mínima de 8 valores (90%)
Participação nas aulas (teórico-)práticas (10%)
Opcionalmente, os alunos podem ainda realizar um pequeno projecto prático, cuja avaliação será incorporada na nota final com um peso de 20%. Nas notas finais superiores a 16 valores esta componente será sempre considerada (querendo dizer que a nota é majorada a 16 valores se não se realizar o dito projecto).
Sumários
Os sumários da disciplina estão disponíveis no calendário.
Aulas Práticas
Os guiões das aulas práticas estão disponíveis aqui.
Proof Theory and Automated Deduction. Jean Goubault-Larrecq & Ian Mackie , Kluwer Academic Publishers, 1997.
First Order Logic and Automated Theorem Proving. Melvin Fitting, Graduate Texts in Computer Science. Springer-Verlag, 1996.
Critérios de Avaliação
A avaliação tem uma componente teórica e uma componente prática, ambas
obrigatórias. A nota final será calculada com base na seguinte
fórmula:
Nota Final = NT * 0.7 + NP * 0.3
sendo
NT a nota teórica (nota mínima de 9 valores), obtida através da realização de uma prova individual escrita;
NP a nota prática (nota mínima de 9 valores), resultante da avaliação de um trabalho prático (realizado em grupos de 3 alunos) e da avaliação contínua realizada ao longo das aulas laboratoriais e que terá por base a resolução de fichas de trabalho;
Quem desejar realizar um projecto prático no âmbito desta disciplina deve contactar um dos docentes. O objectivo desse contacto é o de obter informação/apontadores adicionais sobre os vários projectos e decidir o projecto concreto a ser realizado.
Algumas ideias para projectos práticos:
Animador de uma pequena linguagem funcional com tipos.
Codificação da máquina abstracta de Krivine em C .
Estudo sobre o impacto da operação de substituição na avaliação de lambda-termos .
Inferência/verificação de tipos numa linguagem point-free .
"Design by Contract and Java Modeling Language": apresentação do conceito e clausulas básicas do JML (requires, ensures, invariant).
Universo de ferramentas para JML. Características do ESC/Java2 e da verificação de asserções em tempo de execução (jmlc/jmlrac).
Teórico-prática: exercício de utilização do plugin Eclipse do ESC/Java2 (análise estática simples).
20/11/2008
"JML - beyond the basics": especificação de casos multiplos e de comportamento excepcional; invariantes de ciclo; frame-confitions; dificuldades com aliasing de referências.
Teórico-prática: exercício de modelação em JML.
27/11/2008
"Abstract modeling in JML": herança de especificações; datagroups e abstracção; campos "ghost" e "model"; tipos abstractos para modelação.
Teórica-prática: acompanhamento do projecto JML.
04/12/2008
"Unit Testing and JmlUnit": objectivos e características dos testes unitários; utilização do JUnit; integração com verificação de asserções JML e ferramenta JML-Unit.
Existem meta-predicados que permitem coleccionar todas as soluções para um dado
objectivo de prova (ver User's Manual ou o help).
findall(?Template,:Goal,?Bag) : Bag é a lista de instâncias de Template encontradas nas provas de Goal. A ordem da lista corresponde à ordem em que são encontradas as respostas. Se não existirem instanciações para Template, Bag unifica com a lista vazia.
bagof(?Template,:Goal,?Bag) : Semelhante a findall, mas se Goal falhar, bagof falha.
setof(?Template,:Goal,?Set) : Semelhante a bagof, mas a lista é ordenada e sem repetições.
Exemplo:
| ?- findall(X, member(X,[1,2,3]), L).
L = [1,2,3]
yes
Utilize o predicado findall para determinar todas as soluções para o problema das N rainhas com N=8.
Aula 7: Estratégia Gerar e Testar.
Estratégia Gerar e Testar
O mecanismo de backtracking do PROLOG torna possível codificar, de forma directa, a estratégia de gerar e testar para encontrar a solução de um determinado problema. Segundo esta estratégia, o problema é decomposto em duas fases:
Gera-se "soluções cadidatas" para o problema.
Verifica-se se a "solução candidata" satisfaz os requisitos do problema (e é, portanto, uma "solução efectiva").
Podemos assim identificar o padrão com a seguinte regra PROLOG:
resolve(X) :- gera(X), testa(X).
Note-se o papel preponderante do backtracking para encontrar uma dada solução para resolve(X): o predicado gera(X) instancia X com uma possível solução. No caso de testa(X) falhar (a solução proposta não satisfaz os requisitos impostos pelo problema), o mecanismo de backtracking permite que gera(X) instancie uma nova alternativa, até que se encontre a solução pretendida.
O predicado gera acaba normalmente por se revelar o ponto crítico na aplicação desta estratégia: por um lado, pretende-se que ele cubra todas as possíveis soluções para o problema (caso contrário, podemos nunca gerar a solução requerida). Por outro, e por questões de eficiência, vamos pretender que ele produza o mínimo de soluções erradas (para minimizar o espaço de busca) -- na prática, este esforço de minimização traduz-se por eliminar candidatos notoriamente errados e por encontrar codificações apropriadas para as possíveis soluções.
Vejamos um exemplo concreto: pretende-se encontrar um divisor para um dado número N (diferente de 1 e N).
fromToL(L,U,[]) :- U < L, !.
fromToL(L,U,[L|X]) :- L1 is L+1, fromToL(L1,U,X).
gera(N,X) :- fromToL(2,N-1,L), member(X,L).
testa(N,X) :- N mod X =:= 0.
divisor(N,X) :- gera(N,X), testa(N,X).
Mas o programa apresentado pode ser consideravelmente optimizado se observarmos que nos é suficiente encontrar um divisor entre 2 e sqrt(N) (se X>sqrt(N) é um divisor de N, então também será N/X<sqrt(N)). Dessa forma teríamos:
divisor2(N,X) :- fromtoL(2,sqrt(N),L), member(X,L), N mod X =:= 0.
Verifique ambos os programas para um número primo elevado (e.g. 209953, 331777, 472393, ...)
Utilize a estratégia generate & test para determinar a raiz de um natural, definida da seguinte forma: um número natural X é a raiz de N quando X2<=N e (X+1)2>N
Problema das N rainhas.
Um exemplo clássico de programação em PROLOG consiste em escrever um predicado que permita resolver o problema das n rainhas. Esse problema consiste em dispor n rainas num tabuleiro de damas com dimensão n*n, sem que qualquer rainha se encontre ameaçada por outra. Como um exemplo de uma solução temos (num tabuleiro 4*4):
Q
Q
Q
Q
Note que cada linha e cada coluna deve conter uma, e só uma, rainha (porquê?).
Dito isto, verificamos que uma forma expedita de representar as soluções para este problema consiste em utilizar uma lista que informe qual a coluna em que é colocada a rainha de cada uma das linhas (a solução do exemplo seria [3,1,4,2], querendo dizer que a rainha da primeira linha aparece na terceira coluna, a da segunda linha na primeira coluna, etc.) -- desta forma, aparece uma rainha em cada linha "por construção". A restrição de aparecer uma única rainha por cada coluna é traduzida por deverem aparecer na lista todos os números de 1 a 4, ou seja, a lista deve ser uma permutação de [1,2,3,4]. Temos assim resolvido o sub-problema de gerar soluções candidatas: são simplesmente permutações da lista [1..N].
Na fase de teste, falta unicamente verificar que nenhuma rainha está no alcance da diagonal de uma outra. Para isso notamos que:
Duas rainhas estão numa diagonal / sse a soma da linha e coluna da posição de cada uma delas for igual;
Duas rainhas estão numa diagonal \ sse a diferença da linha e coluna da posição de cada uma delas for igual.
Com base no que foi referido, codifique um predicado nrainhas(+N,?X) que determine uma solução para o problema das N-rainhas.
Aula 6: Manipulação de fórmulas lógicas proposicionais em Prolog.
Definição de Operadores em Prolog.
O Prolog permite definir operadores prefixos, sufixos ou infixos. Para tal devemos utilizar o predicado pré-definido op(_Prec_,=_Type_,=_Name_=)=. O argumento Name é o nome do operador definido; Prec é um número entre 0 e 1200 que determinará a sua precedência e Type determina o seu tipo e associatividade. Por exemplo, o operador de soma binário + está definido como op(700, yfx, +). A precedência 700 irá determinar que tenha menos precedência do que a multiplicação (definida com precedência 500 - note que um número menor indica maior precedência do operador), e o tipo yfx caracteriza o operador como infixo e associativo à esquerda. Outras possibilidades para o tipo dos operadores são: xfy, xfx para operadores infixos associativos à direita e sem associatividade; fx, fy para operadores prefixos e xf, yf para operadores sufixos.
Alguns dos operadores pré-definidos do Prolog são:
Faça um pequeno predicado que lhe permita confirmar a maior precedência do operador * face ao operador +.
Manipulação de fórmulas lógicas proposicionais em Prolog.
A definição de operadores permite que a sintaxe do Prolog se aproxime do domínio onde se está a trabalhar. Considere que se pretendem representar fórmulas da Lógica Proposicional em Prolog. Em vez de considerar termos como or(not(p), and( and(p, r), not(q))), podemos utilizar operadores que nos permitam aproximar a sua representação da utilizada habitualmente. Assim definimos:
Estamos a utilizar os operadores de conjunção e disjunção do Prolog (se preferir, pode definir os operadores /\ e \/). Assim, a fórmula apresentada atrás pode ser escrita como (~p ; p , r, ~q) (note o papel da precedência e associatividade).
Defina um predicado que, dado uma fórmula proposicional, determine a Forma Normal Negativa (FNN).
Pretende-se definir um programa que permita verificar se uma dada fórmula é uma contradição pelo método de Davis Putnam. Para o efeito, considere os seguintes predicatos que convertem uma FNN na respectiva Forma Normal Conjuntiva (FNC), e que colocam esta última na sua forma matricial (como uma lista de listas) :
% -----------------------------------------------------------------
% fnc(+NNF,?FNC)
%
% NNF é uma forma normal negatiiva e FNC a respectiva forma normal conjuntiva
cnf(((A,B);C), (F1,F2)) :- !, cnf((A;C),F1), cnf((B;C),F2).
cnf((A;(B,C)), (F1,F2)) :- !, cnf((A;B),F1), cnf((A;C),F2).
cnf((A;B), F) :- !, cnf(A, A1), cnf(B, B1),
(/*IF*/ (A1=(C,D); B1=(C,D)) ->
/*THEN*/ cnf((A1;B1), F) ;
/*ELSE*/ F=(A1;B1) ).
cnf((A,B), (A1,B1)) :- !, cnf(A, A1), cnf(B, B1).
cnf(Lit, Lit).
% -----------------------------------------------------------------
% matCNF(+FNC,?MAT)
%
% FNC é uma forma normal conjuntiva e MAT é a sua representação sob a forma
% de matriz (lista de listas de literais).
matCNF((A,B),M) :- !, matCNF(A,MA), matCNF(B,MB), append(MA,MB,M).
matCNF((A;B),C) :- !, matCNF(A,[CA]), matCNF(B,[CB]), union2(CA,CB,C).
matCNF(~Lit, [[-Lit]]) :- !.
matCNF(Lit, [[Lit]]).
union2([],L,[L]).
union2([X|L1],L2,L3) :- member2(X,L2), !, union2(L1,L2,L3).
union2([X|_],L2,[]) :- (-Xn=X;-X=Xn), member2(Xn,L2), !.
union2([X|L1],L2,L3) :- union2(L1,[X|L2],L3).
member2(X,[Y|_]) :- X==Y, !.
member2(X,[_|T]) :- member2(X,T).
Aula 5: Utilização de cut e negação por falha.
O predicado pré-definido cut (!) permite eliminar ramos nas árvores de derivação de predicados Prolog. Operacionalmente, o cut pode ser caracterizado da seguinte forma: _"Durante o processo de prova, a 1a passagem pelo cut é sempre
verdadeira (com sucesso). Se por backtracking se voltar ao cut,
então o cut faz falhar o predicado que está na cabeça da regra."_
A utilização do cut está normalmente associada a questões de eficiência: os ramos da árvore que são eliminados acabariam eventualmente por falhar, e assim poupamos trabalho ao motor de inferência do Prolog. Esta utilização do cut é considerada benigna, porque não se afecta o significado dos predicados. Tomemos como exemplo um predicado que verifique se o terceiro argumento é o mínimo dos dois primeiros. Podería ser definido como:
minimo(X,Y,Y) :- X >= Y.
minimo(X,Y,X) :- X < Y.
Mas podemos facilmente observar que, uma vez verificado que X>=Y, não faz sentido tentar verificar que X<Y. Assim sendo, faz sentido colocar um cut no final da primeira cláusula:
minimo(X,Y,Y) :- X >= Y, !.
minimo(X,Y,X) :- X < Y.
Estaria correcto eliminar também o predicado X<Y na segunda cláusula? Justifique com exemplos apropriados.
É importante referir que certas utilizações do cut alteram propositadamente o comportamento do programa (tipicamente para impedir que a execução do programa entre em ciclo). Essas utilizações são normalmente consideradas "mais perigosas" porque obriga a que o programador detenha uma ideia muito precisa sobre o processo de construção da derivação por parte do Prolog.
Relembre as seguintes alternativas para calcular o multiplicação de naturais:
a(zero, Y, Y).
a(suc(X), Y, suc(Z)) :- a(X,Y,Z).
m1(zero, _, zero).
m1(suc(X), Y, Z) :- a(Y, W, Z), m1(X,Y,W).
m2(zero, _, zero).
m2(suc(X), Y, Z) :- m2(X,Y,W), a(Y, W, Z).
Seria possível impedir a computação infinita de m2 por intermédio da introdução de cuts?
A introdução de cuts também faria sentido para m1? Onde? Justifique.
Considere o seguinte programa que pretende inserir o primeiro argumento (um número) na lista ordenada passada no segundo argumento.
Mostre, avaliando um objectivo apropriado, que o programa está incorrecto.
Como o poderá corrigir?
Negação por falha.
Por vezes pretende-se garantir que um dado predicado não é válido. A utilização do cut (em conjunção com o predicado pré-definido fail que falha sempre) permite codificar uma forma restrita de negação: a "negação por falha". Considere o seguinte predicado:
neg(X) :- X, !, fail.
neg(X).
Note que neg(X) falha sempre que o Prolog consiga construir uma derivação para X. Por outro lado, sucede se falhar na construção dessa derivação (entra na segunda cláusula, que é trivialmente satisfeita). Obs.: o predicado pré-definido do Prolog \+ corresponde ao predicado neg apresentado.
Verifique o resultado de neg em predicados já definidos.
Como explica a resposta às questões estudante_solteiro(paulo) e estudante_solteiro(X)
Aula 4: Árvores de Prova. Tipos algébricos
Árvores de Prova em Prolog
Operacionalmente, o Prolog segue uma estratégia top down, depth-first para encontrar soluções das questões colocadas. O processo de Unificação permite concretizar as questões colocadas definindo as condições em que a questão inicial é satisfeita (a substituição obtida). Quando o motor de inferência se depara com uma situação de "falha", retrocede na árvore de prova por forma a tentar novas alternativas.
Relembre o predicado member que verifica se um elemento pertence a uma lista. Construa a árvore de procura de soluções para a questão member(X,[1,2,3]).
Considere agora o predicado takeout/3 referido na última aula. Construa a árvore de procura de soluções para a questão takeout(X,[1,2,3],Y).
Tipos algébricos em Prolog
A utilização de termos permite a manipulação em Prolog de valores de tipos algébricos (que em Haskell seriam declarados com data). Por exemplo, árvores binárias podem ser representadas por termos como vazia, nodo(vazia, vazia), etc.
Defina um predicado que verifique se uma lista é uma travessia in-order de uma árvore.
Defina predicados que determinem:
uma árvore é uma Árvore Binária de Procura
uma lista está ordenada.
Note no entanto que em Prolog não existe a noção de tipo. De facto nada nos impede de considerar termos como vazia(nodo,vazia(nodo)).
Aula 3: Continuação da manipulação de listas
Defina last/2 que verifique se o último elemento de uma lista é um dado.
Defina append/3 que concatene duas listas.
Utilize o predicado append para definir os predicados prefixo e sufixo que verificam se uma lista é prefixo ou sufixo doutra.
Defina split/4 que separe os elementos de uma lista nos menores e maiores que um dado valor.
Utilize o predicado takeout para definir um predicado que determine se uma lista é permutação de uma outra.
Aula 2: Utilização de termos, introdução à manipulação de Listas.
Termos Estruturados
Para além dos tipos primitivos, o Prolog admite termos estruturados da forma f(t1,t2,...,tn), onde f é o functor do termo e t1,...tn são sub-termos.
Uma aplicação típica de termos estruturados é para organizar a informação contida num programa. Por exemplo, podemos armazenar datas com termos da forma "data(25,abril,2007)". O seguinte predicado extrai o dia duma data armazenada dessa forma:
diaData(D,data(D,_,_)).
Defina o predicado valData/1 que verifique se uma data é correcta.
Nada nos impede de considerarmos termos arbitrariamente complicados. Em particular, podemos considerar termos de natureza recursiva como a representação dos naturais com os construtores zero e suc (i.e. zero, suc(zero), suc(suc(zero)), etc.).
Defina o predicado nat/1 que verifique se um termo é um natural na representação referida.
Defina soma/3 que verifique se o terceiro argumento é a soma dos dois primeiros.
Mostre como usar o predicado soma/3 para calcular a subtração de dois naturais.
Defina predicados int2nat/2 e nat2int/2 que convertam naturais em inteiros e vice-versa.
Introdução às Listas em Prolog
Um exemplo de um tipo estruturado que está pré-definido no Prolog são as listas. A sintaxe mais prática é [] que denota a lista vazia e [H|T] que denota a lista com cabeça H e cauda T.
Defina member/2 que verifica se um elemento pertence a uma lista.
Utilize o predicado member para determinar quais dos elementos da lista [3,5,4,6,5,7] são pares.
Aula 9: Implementação do algoritmo Davis-Putnam em Prolog.
Pretende-se definir um programa que permita verificar se uma dada fórmula é uma contradição pelo método de Davis Putnam. Para o efeito, considere os seguintes predicatos que convertem uma FNN na respectiva Forma Normal Conjuntiva (FNC), e que colocam esta última na sua forma matricial (como uma lista de listas) :
% -----------------------------------------------------------------
% fnc(+NNF,?FNC)
%
% NNF é uma forma normal negatiiva e FNC a respectiva forma normal conjuntiva
cnf(((A /\ B) \/ C), (F1 /\ F2)) :- !, cnf((A \/ C),F1), cnf((B \/ C),F2).
cnf((A \/ (B /\ C)), (F1,F2)) :- !, cnf((A \/ B),F1), cnf((A \/ C),F2).
cnf((A \/ B), F) :- !, cnf(A, A1), cnf(B, B1),
(/*IF*/ (A1=(C /\ D); B1=(C /\ D)) ->
/*THEN*/ cnf((A1 \/ B1), F) ;
/*ELSE*/ F=(A1 \/ B1) ).
cnf((A /\ B), (A1 /\ B1)) :- !, cnf(A, A1), cnf(B, B1).
cnf(Lit, Lit).
% -----------------------------------------------------------------
% matCNF(+FNC,?MAT)
%
% FNC é uma forma normal conjuntiva e MAT é a sua representação sob a forma
% de matriz (lista de listas de literais).
matCNF((A /\ B),M) :- !, matCNF(A,MA), matCNF(B,MB), append(MA,MB,M).
matCNF((A \/ B),C) :- !, matCNF(A,[CA]), matCNF(B,[CB]), union2(CA,CB,C).
matCNF(~Lit, [[-Lit]]) :- !.
matCNF(Lit, [[Lit]]).
union2([],L,[L]).
union2([X|L1],L2,L3) :- member2(X,L2), !, union2(L1,L2,L3).
union2([X|_],L2,[]) :- (-Xn=X;-X=Xn), member2(Xn,L2), !.
union2([X|L1],L2,L3) :- union2(L1,[X|L2],L3).
member2(X,[Y|_]) :- X==Y, !.
member2(X,[_|T]) :- member2(X,T).
Exercícios:
Defina um predicado que determine a forma normal disjuntiva.
Defina o predicado de split/3 que determine o particionamento de uma FN.
Defina o predicado davisPutnam/1 que verifique se uma fórmula proposicional é inconsistente.
Aula 8: Manipulação de fórmulas de lógica proposicional em Prolog.
Definição de Operadores em Prolog.
O Prolog permite definir operadores prefixos, sufixos ou infixos. Para tal devemos utilizar o predicado pré-definido op(Prec,Type,Name). O argumento Name é o nome do operador definido; Prec é um número entre 0 e 1200 que determinará a sua precedência e Type determina o seu tipo e associatividade. Por exemplo, o operador de soma binário + está definido como op(700, yfx, +). A precedência 700 irá determinar que tenha menos precedência do que a multiplicação (definida com precedência 500 - note que um número menor indica maior precedência do operador), e o tipo yfx caracteriza o operador como infixo e associativo à esquerda. Outras possibilidades para o tipo dos operadores são: xfy, xfx para operadores infixos associativos à direita e sem associatividade; fx, fy para operadores prefixos e xf, yf para operadores sufixos.
Alguns dos operadores pré-definidos do Prolog são:
Faça um pequeno predicado que lhe permita confirmar a maior precedência do operador * face ao operador +.
Manipulação de fórmulas de lógica proposicional em Prolog.
A definição de operadores permite que a sintaxe do Prolog se aproxime do domínio onde se está a trabalhar. Considere que se pretendem representar fórmulas da Lógica Proposicional em Prolog. Em vez de considerar termos como or(not(p), and( and(p, r), not(q))), podemos utilizar operadores que nos permitam aproximar a sua representação da utilizada habitualmente. Assim definimos:
que denotam os operadores de implicação, disjunção, conjunção e negação. Assim, a fórmula apresentada atrás pode ser escrita como (~p \/ p /\ r /\ ~q) (note o papel da precedência e associatividade).
Exercícios:
Defina o predicado props(+Form,-Props) que calcule o conjunto de símbolos de proposições utilizados na fórmula dada.
Defina o predicado val(+Form,+Mod) que verifique se a fórmula é válida no modelo passado como argumento.
Como poderia reformular a definição do predicado val por forma a que não seja necessário instanciar o modelo (ou seja, construir o predicado valM(+Form, ?Mod).
Defina o predicado nnf(+Form, -NNF) que determine a forma normal negativa de uma fórmula.
Aula 7: Predicados de Segunda Ordem e outros predicados primitivos disponibilizados pelo Prolog
Predicados de segunda ordem
Existem meta-predicados que permitem coleccionar todas as soluções para um dado
objectivo de prova (ver User's Manual ou o help).
findall(?Template,:Goal,?Bag) : Bag é a lista de instâncias de Template encontradas nas provas de Goal. A ordem da lista corresponde à ordem em que são encontradas as respostas. Se não existirem instanciações para Template, Bag unifica com a lista vazia.
bagof(?Template,:Goal,?Bag) : Semelhante a findall, mas se Goal falhar, bagof falha.
setof(?Template,:Goal,?Set) : Semelhante a bagof, mas a lista é ordenada e sem repetições.
Exemplo:
| ?- findall(X, member(X,[1,2,3]), L).
L = [1,2,3]
yes
Relacionados com os apresentados, encontramos outros predicados de ordem superior, como o bem conhecido map (do haskell). No Prolog o predicado maplist implementa a funcionalidade análoga.
Exercícios:
Teste os predicados apresentados codificando exemplos apropriados.
Utilize o predicado findall para determinar todas as soluções para o problema das N rainhas com N=8.
Outras características do Prolog
Manipulação da base de conhecimento: O Prolog permite manipular dinamicamente a base de conhecimento (inserir ou remover factos ou regras). Para isso disponibiliza os predicados assert, retract, rectractall (e variantes...).
Input/Output: tal como qualquer linguagem com o mínimo de preocupações práticas, é possível realizar operações de Input/Output. Para o efeito dispõe-se dos predicados write, read (entre outros, e com muitas variantes...); open e close para maniputação de ficheiros, etc...
Exercícios:
Consulte a documentação relativa aos predicados referidos e teste cada um deles com exemplos apropriados.
Extenda o programa das N rainhas com um predicado runQueens que interrogue o utilizador sobre o número de rainhas a considerar e imprima no écran todas as soluções admissíveis.
Aula 6: Estratégia Gerar e Testar.
Estratégia Gerar e Testar
O mecanismo de backtracking do PROLOG torna possível codificar, de forma directa, a estratégia de gerar e testar para encontrar a solução de um determinado problema. Segundo esta estratégia, o problema é decomposto em duas fases:
Gera-se "soluções cadidatas" para o problema.
Verifica-se se a "solução candidata" satisfaz os requisitos do problema (e é, portanto, uma "solução efectiva").
Podemos assim identificar o padrão com a seguinte regra PROLOG:
resolve(X) :- gera(X), testa(X).
Note-se o papel preponderante do backtracking para encontrar uma dada solução para resolve(X): o predicado gera(X) instancia X com uma possível solução. No caso de testa(X) falhar (a solução proposta não satisfaz os requisitos impostos pelo problema), o mecanismo de backtracking permite que gera(X) instancie uma nova alternativa, até que se encontre a solução pretendida.
O predicado gera acaba normalmente por se revelar o ponto crítico na aplicação desta estratégia: por um lado, pretende-se que ele cubra todas as possíveis soluções para o problema (caso contrário, podemos nunca gerar a solução requerida). Por outro, e por questões de eficiência, vamos pretender que ele produza o mínimo de soluções erradas (para minimizar o espaço de busca) -- na prática, este esforço de minimização traduz-se por eliminar candidatos notoriamente errados e por encontrar codificações apropriadas para as possíveis soluções.
Vejamos um exemplo concreto: pretende-se encontrar um divisor para um dado número N (diferente de 1 e N).
fromToL(L,U,[]) :- U < L, !.
fromToL(L,U,[L|X]) :- L1 is L+1, fromToL(L1,U,X).
gera(N,X) :- fromToL(2,N-1,L), member(X,L).
testa(N,X) :- N mod X =:= 0.
divisor(N,X) :- gera(N,X), testa(N,X).
Mas o programa apresentado pode ser consideravelmente optimizado se observarmos que nos é suficiente encontrar um divisor entre 2 e sqrt(N) (se X>sqrt(N) é um divisor de N, então também será N/X<sqrt(N)). Dessa forma teríamos:
divisor2(N,X) :- fromtoL(2,sqrt(N),L), member(X,L), N mod X =:= 0.
Verifique ambos os programas para um número primo elevado (e.g. 209953, 331777, 472393, ...)
Utilize a estratégia generate & test para determinar a raiz de um natural, definida da seguinte forma: um número natural X é a raiz de N quando X2<=N e (X+1)2>N
Problema das N rainhas.
Um exemplo clássico de programação em PROLOG consiste em escrever um predicado que permita resolver o problema das n rainhas. Esse problema consiste em dispor n rainas num tabuleiro de damas com dimensão n*n, sem que qualquer rainha se encontre ameaçada por outra. Como um exemplo de uma solução temos (num tabuleiro 4*4):
Q
Q
Q
Q
Note que cada linha e cada coluna deve conter uma, e só uma, rainha (porquê?).
Dito isto, verificamos que uma forma expedita de representar as soluções para este problema consiste em utilizar uma lista que informe qual a coluna em que é colocada a rainha de cada uma das linhas (a solução do exemplo seria [3,1,4,2], querendo dizer que a rainha da primeira linha aparece na terceira coluna, a da segunda linha na primeira coluna, etc.) -- desta forma, aparece uma rainha em cada linha "por construção". A restrição de aparecer uma única rainha por cada coluna é traduzida por deverem aparecer na lista todos os números de 1 a 4, ou seja, a lista deve ser uma permutação de [1,2,3,4]. Temos assim resolvido o sub-problema de gerar soluções candidatas: são simplesmente permutações da lista [1..N].
Na fase de teste, falta unicamente verificar que nenhuma rainha está no alcance da diagonal de uma outra. Para isso notamos que:
Duas rainhas estão numa diagonal / sse a soma da linha e coluna da posição de cada uma delas for igual;
Duas rainhas estão numa diagonal \ sse a diferença da linha e coluna da posição de cada uma delas for igual.
Com base no que foi referido, codifique um predicado nrainhas(+N,?X) que determine uma solução para o problema das N-rainhas.
Aula 5: Utilização de cut e negação por falha.
O predicado pré-definido cut (!) permite eliminar ramos nas árvores de derivação de predicados Prolog. Operacionalmente, o cut pode ser caracterizado da seguinte forma: _Durante o processo de prova, a 1a passagem pelo cut é sempre
verdadeira (com sucesso). Se por backtracking se voltar ao cut,
então o cut faz falhar o predicado que está na cabeça da regra._
A utilização do cut está normalmente associada a questões de eficiência: os ramos da árvore que são eliminados acabariam eventualmente por falhar, e assim poupamos trabalho ao motor de inferência do Prolog. Esta utilização do cut é considerada benigna (green cut), porque não se afecta o significado dos predicados. Tomemos como exemplo um predicado que verifique se o terceiro argumento é o mínimo dos dois primeiros. Podería ser definido como:
minimo(X,Y,Y) :- X >= Y.
minimo(X,Y,X) :- X < Y.
Mas podemos facilmente observar que, uma vez verificado que X>=Y, não faz sentido tentar verificar que X<Y. Assim sendo, faz sentido colocar um cut no final da primeira cláusula:
minimo(X,Y,Y) :- X >= Y, !.
minimo(X,Y,X) :- X < Y.
Estaria correcto eliminar também o predicado X<Y na segunda cláusula? Justifique com exemplos apropriados.
É importante referir que certas utilizações do cut alteram propositadamente o comportamento do programa (tipicamente para impedir que a execução do programa entre em ciclo). Essas utilizações são normalmente consideradas "mais perigosas" (red cuts) porque obrigam a que o programador detenha uma ideia muito precisa sobre o processo de construção da derivação por parte do Prolog.
Mostre, avaliando um objectivo apropriado, que o programa está incorrecto.
Como o poderá corrigir?
Negação por falha.
Por vezes pretende-se garantir que um dado predicado não é válido. A utilização do cut (em conjunção com o predicado pré-definido fail que falha sempre) permite codificar uma forma restrita de negação: a "negação por falha". Considere o seguinte predicado:
neg(X) :- X, !, fail.
neg(X).
Note que neg(X) falha sempre que o Prolog consiga construir uma derivação para X. Por outro lado, sucede se falhar na construção dessa derivação (entra na segunda cláusula, que é trivialmente satisfeita). Obs.: o predicado pré-definido do Prolog \+ corresponde ao predicado neg apresentado.
Verifique o resultado de neg em predicados já definidos.
Construa a árvore de procura de soluções para a questão takeout(X,[1,2,3],Y).
Utilize o predicado takeout para definir um predicado que determine se uma lista é permutação de uma outra.
Tipos Algébricos
A utilização de termos permite a manipulação em Prolog de valores de tipos algébricos (que em Haskell seriam declarados com data). Um primeiro exemplo disso já foi ilustrado na última aula quando se manipularam naturais (zero, suc(zero), etc.). Para sistematizar, vejamos agora como manipular um outro tipo algébrico bem conhecido: as árvores binárias. Uma escolha óbvia para representar os seus valores será considerar o átomo vazia para representar a árvore vazia e termos da forma nodo(X,E,D) para representar nodos intermédios (com valor X, sub-árvore esquerda E e sub-árvore direita D). Temos então como exemplos de termos: vazia, nodo(4, vazia, vazia), etc.
Note no entanto que em Prolog não existe a noção de tipo (e.g. não podemos, à priori, condicionar um dado argumento de um predicado a ser uma árvore binária --- a única alternativa será definir-se um predicado que suceda para termos que tenham a estrutura prescrita...)
Defina um predicado arvBin/1 que verifique se o termo dado é uma árvore binária (e.g. deve falhar para termos como vazia(nodo,vazia(nodo))).
Defina um predicado que verifique se uma lista é uma travessia in-order de uma árvore.
Defina predicados que determinem:
uma árvore é uma Árvore Binária de Procura
uma lista está ordenada.
Aula 3: Árvores de derivação do Prolog.
Considere-se a definição do predicado member/2
member(X,[X|_]).
member(X,[_|T]) :- member(X,T).
Este predicado foi definido na última aula com o objectivo de verificar se um elemento está contido numa lista. De facto, podemos utiliza-lo como:
Mas podemos também utiliza-lo com variáveis não instanciadas com o objectivo de determinar quais os elementos de uma lista:
?- member(X,[1,2,3]).
X = 1 ;
X = 2 ;
X = 3 ;
fail.
Ou até para determinar soluções a questões mais complicadas, como (mais um exemplo da última aula):
?- member(X,[3,5,4,6,5,7]), X mod 2 =:= 0.
X = 4 ;
X = 6 ;
fail.
O objectivo desta aula é o de se perceber como é que o Prolog consegue chegar às soluções apresentadas (substituições de variáveis que validam o objectivo).
Inferência do Prolog
Um objectivo em Prolog consiste numa lista de predicados. O resultado da "execução" desse objectivo num interpretador consiste numa substituição que verifique esses predicados. O processo construção da substituição é normalmente designado por inferência, e pode ser justificado construindo uma árvore como se descreve:
Na raiz da árvore, coloca-se a lista de predicados. O Prolog irá processar cada predicado dessa lista por ordem.
Para cada predicado, o Prolog irá procurar encontrar na base de conhecimento uma instância dum facto ou duma regra cuja cabeça unifique com esse predicado. Esta procura processa-se também pela ordem pela qual as definições ocorrem na base de conhecimento.
Quando é encontrada uma regra nas condições referidas, cria-se um descendente na árvore contendo a lista já afectada pela substituição resultante da unificação (relembre que o resultada na unificação é uma substituição das variáveis) e onde o predicado em análise é substituído pelo lado direito da regra (ou simplesmente desaparece, no caso dos factos). É habitual anotarmos os arcos da árvore com as substituições resultantes das unificações.
Quando existe mais do que uma possibilidade para a referida unificação (e.g. várias regras são aplicáveis), traduz-se por uma ramificação da árvore de inferência.
Operacionalmente, o Prolog trata esta ramificação pelo mecanismo de backtracking (travessia depth-first da árvore).
Quando a lista de predicados fica vazia, cria-se uma folha na árvore denotada como true --- representa um resultado apresentado ao utilizador (a substituição calculada ao longo do caminho).
Quando não existe qualquer regra na base de conhecimento que unifique com o primeiro predicado da lista, cria-se uma folha denotada por fail .
A árvore de derivação para o objectivo "member(X,[1,2]), X mod 2 ==0" será:
Exercícios:
Considere a seguinte definição do predicado factorial:
fact(1,0).
fact(R,X) :- X2 is X-1, fact(R2,X2), R is X*R2.
Apresente a árvore de inferência para o objectivo fact(R,2).
Comente os resultados obtidos. Explique, em particular, que problemas aponta à solução apresentada.
Como pode ultrapassar os problemas detectados.
Considere o seguinte predicado:
nat2int(zero,0).
nat2int(suc(X),N) :- nat2int(X,N2), N is N2+1.
Apresente a árvore de inferência para o objectivo nat2int(suc(suc(zero)),X).
Apresente a árvore de inferência para o objectivo nat2int(X,2).
Comente os resultados obtidos.
Consegue propor alguma forma de ultrapassar os problemas detectados?
Tracing e Debug
Uma forma expedita de detectar problemas em programas Prolog consiste em utilizar o mecanismo de tracing. Esse mecanismo permite "monitorizar" determinados predicados durante o processo de inferência. Considere-se novamente o objectivo considerado atrás que faz uso do predicado member/2:
?- trace(member).
% member/2: [call, redo, exit, fail]
true.
[debug] ?- member(X,[1,2]), X mod 2 =:= 0.
T Call: (8) member(_G318, [1, 2])
T Exit: (8) member(1, [1, 2])
T Redo: (8) member(_G318, [1, 2])
T Call: (9) member(_G318, [2])
T Exit: (9) member(2, [2])
T Exit: (8) member(2, [1, 2])
X = 2 ;
T Redo: (9) member(_G318, [2])
T Call: (10) member(_G318, [])
T Fail: (10) member(_G318, [])
fail.
Note que o Prolog sinalizada diferentes eventos relativos ao predicado observado:
Call: o predicado em "resolução";
Exit: o predicado foi resolvido com sucesso (pode por isso ser removido da lista de objectivos);
Redo: nova visita ao predicado (por backtracking);
Fail: predicado falha definitivamente (já não existem mais alternativas para o backtracking).
Exercício:
Interprete o resultado do trace apresentado na árvore de inferência apresentada acima.
Realize análises de traces para as restantes árvores construídas nesta aula...
Aula 2: Operações aritméticas e Manipulação de listas.
Operações aritméticas
Já vimos que o Prolog aceita termos que representem expressões matemáticas, como 3+4*2. Mas quando manipulamos esses termos estamos normalmente interessados em avaliar essas expressões (i.e. calcular o seu resultado). O Prolog disponibiliza para o efeito o predicado is que avalia o segundo argumento e unifica o resultado com o primeiro. Alguns exemplos (onde se utiliza a notação infixa para o predicado):
?- X is 3+2.
X = 5.
?- 3+2 is 2+3.
fail.
?- 5 is 3+2.
true.
?- 5 is X+2.
ERROR: is/2: Arguments are not sufficiently instantiated
Um aspecto importante na utilização do predicado is é a assimetria induzida: o segundo argumento deve ser sempre uma expressão completamente instanciada. Assim, se definirmos o predicado:
soma(X,Y,Z) :- X is Y + Z.
devemos considerar o segundo e o terceiro argumentos como "argumentos de entrada", que necessitam estar devidamente instanciados. Uma forma compacta de se exprimir esse facto (normalmente utilizada na documentação) é através da assinatura soma(-X,+Y,+Z) --- assim identifica-se o argumento Y e Z como de entrada e X como de saída.
Exercício:
Defina o predicado factorial(-R,+X) que suceda quando R for o factorial de X.
Uma forma alternativa de lidar com números naturais consiste em considerar termos zero, suc(zero), suc(suc(zero)), etc. (i.e. utilizar notação unária para os naturais). Defina o predicado nat2int que sucede quando o primeiro argumento é a representação unária do segundo.
No predicado definido na alínea anterior, verifique:
que argumentos tem de ser utilizados como entrada e como saída;
o que acontece quando solicita ao interpretador várias respostas.
Verifique, com o auxílio do mecanismo de help do SWI-Prolog (ou da documentação on-line, se preferir) qual a funcionalidade oferecida pelos operadores:
=:=, =\=, <, =<, ==, @<
Manipulação de listas
Um exemplo de um tipo estruturado muito utilizado em Prolog são as listas. A sintaxe pré-definida é [] que denota a lista vazia e [H|T] que denota a lista com cabeça H e cauda T.
Defina member/2 que verifica se um elemento pertence a uma lista.
Utilize o predicado member para determinar quais dos elementos da lista [3,5,4,6,5,7] são pares.
Defina um predicado que permita calcular o somatório de uma lista de inteiros.
O que alteraria, no predicado definido na alínea anterior, para calcular o somatório de uma lista de expressões inteiras?
Aula 1: Apresentação da linguagem PROLOG
Ao longo das aulas práticas de Lógica Computacional fazer uso da linguagem PROLOG. O interpretador adoptado será o SWI-Prolog que está disponível para para a generalidade das plataformas (MS-Windows, Linux, macOSX).
Conceitos Preliminares
Termos: o Prolog é uma linguagem simbólica que manipula termos que podem ser:
Variáveis - denotadas por identificadores começados por letras maiúsculas (e.g. X, Y, Xs, ...);
Constantes - átomos (identificadores começados por letras minúsculas) ou valores de tipos pré-definidos como inteiros, reais, strings, etc. (e.g. abc, xyz, 32, 3.1415)
Termos Compostos - termos da forma f(t1,...,tn) onde f é designado por functor (nome da função) e t1...tn são termos (e.g. xyz(X,abc), abc(abc(abc,abc)), +(4,2))
obs.: como iremos ver adiante, o Prolog permite a declaração de operadores infixos. Assim irá permitir escrever 4 + 2 como alternativa ao termo +(4,2) (o mesmo se aplica a outros operadores infixos que serão apresentados adiante).
Substituições e Unificação: o que caracteriza as variáveis é o facto de elas poderem vir a ser substituidas por outros termos. Considere-se o termo t(X,Y): se substituirmos X por abc(A,3) e Y por Z obtemos o termos t(abc(A,3),Z).
Uma operação fundamental no modelo de execução do Prolog é o que se designa por Unificação de dois termos. A ideia consiste em encontrar uma substituição que iguale (se possível) os termos dados. Vejamos alguns exemplos:
X = 4, Y = 3 é um unificador dos termos abc(3,X) e abc(Y,4);
X = 4, Y = 3 é um unificador dos termos abc(X,X) e abc(Y,4);
os termos abc(3,4) e abc(X,X) não dispõe de unificador.
Uma característica dos unificadores apresentados é que se tratam sempre dos unificadores mais gerais (qualquer outra substituição que unifique os termos pode ser expressa como um refinamento da substituição dada). Adiante iremos ter oportunidade de aprofundar estes aspectos mais teóricos... Para já interessa reter que o Prolog, quando unificar dois termos, determina sempre o unificador mais geral (i.e. a substituição mais simples que iguala os termos).
EXERCÍCIO: Determine o unificador mais geral para os seguintes pares de termos (se existir... naturalmente):
f(X,g(Y)) e g(X,f(Y))
f(X,g(Y)) e Z
f(X,g(y)) e f(g(y),X)
f(X) e X
f(X) e f(3+2)
f(3) e f(2+1)
f(3) e A(X)
Programas em Prolog
Executar um programa em Prolog consiste em interrogar o interpretador sobre a validade de um dado predicado lógico. A resposta mais simples será então true ou fail (se o predicado for válido ou não, respectivamente).
Objectivo (Goal):
Quando se invoca o SWI-Prolog, surge o prompt?- que assinala que o interpretador aguarda a introdução de um objectivo (ou query, ou goal).
Calvin:~ jba$ /opt/local/bin/swipl
Welcome to SWI-Prolog (Multi-threaded, 32 bits, Version 5.6.51)
Copyright (c) 1990-2008 University of Amsterdam.
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software,
and you are welcome to redistribute it under certain conditions.
Please visit http://www.swi-prolog.org for details.
For help, use ?- help(Topic). or ?- apropos(Word).
?-
Como referimos, o objectivo será um predicado lógico. Iremos ter oportunidade de definir novos predicados mas, para já, concentremo-nos na utilização do predicado pré-definido =/2 (o /2 significa que o predicado espera dois argumentos). Este predicado será válido precisamente quando os termos que forem passados como argumentos unificarem. Assim podemos introduzir:
?- =(3,3).
true.
?- 3=3.
true.
?- 3=2.
fail.
?- 3=X.
X = 3.
?- 3+2=X.
X = 3+2.
?- 3 + X = Y * 2.
fail.
?-
Os exemplos apresentados revelam-nos duas coisas: (1) podemos utilizar a notação infixa e, (2) quando no objectivo estão envolvidas veriáveis o Prolog retorna uma substituição dessas variáveis que verifiquem o predicado (ou falha, se não existir nenhuma substituição nessas condições) --- podemos então dizer que, intuitivamente, as variáveis dos objectivos estão quantificadas existencialmente.
EXERCÍCIO: Interrogue o interpretador de Prolog por forma a ele retornar os unificadores mais gerais atrás solicitados.
Factos (base de conhecimento I):
Referimos que executar um programa em Prolog consiste em interrogar o interpretador relativamente a um objectivo. Mas, em que é que consiste um programa Prolog?. Um programa em Prolog será a base de conhecimento que o interpretador utiliza para determinar a validade do objectivo pedido. Essa base de conhecimento será consituída por:
Factos: que estabelecem a validade imediata (de instâncias) de predicados;
Regras: que condicionam a validade de predicados à validade de sub-objectivos.
Comecemos pelos primeiros. Como exemplos de factos podemos ter:
Com base nestes factos, diriamos que pai(joaquim,manuel) é válido mas pai(joaquim,jose) já não o é (porque nada estabelece a sua validade). Para verificar isso com o Prolog, necessitamos de carregar a base de conhecimento no interpretador. Para tal devemos:
gravar um ficheiro com os factos apresentados (normalmente dá-se a extensão ".pl" aos ficheiros Prolog, e.g. "pai.pl");
carregar o ficheiro no interpretador por intermédio do predicado pré-definido consult (e.g. "consult(pai.pl)").
EXERCÍCIO: Verifique a validade de alguns objectivos com a base de conhecimento apresentada. O que acontece quando se inclui variáveis?
Por vezes, o interpretador retorna uma substituição de resultado sem voltar ao prompt inicial. Isso assinala que a solução apresentada é uma de várias possíveis, podendo o utilizador:
digitar . e retornar ao prompt inicial;
digitar ; para solicitar outra solução.
EXERCÍCIO:
introduza um predicado que permita determinar todos os filhos de "manuel".
o que aconteceria se incluisse na base de conhecimento o facto pai(X,carlos) ? Experimente... (verifique o impacto de o incluir no início e no fim da base de conhecimento).
O exercício anterior permite concluir que, nos factos, devemos realizar uma interpretação universal das variáveis.
Se as questões colocadas ao interpretador de Prolog são predicados lógicos, é natural perguntarmo-nos como construir predicados à custa de conectivas lógicas (como e, ou, etc.). O Prolog tem definido os operadores:
conjunção: denotado por uma vírgula (,)
disjunção: denotado por um ponto e vírgula (;)
(As restantes conectivas lógicas proposicionais serão introduzidas mais tarde.)
Regras (base de conhecimento II):
A expressividade do Prolog resulta do facto de permitir incluir, na base de conhecimento, regras que condicionam a validade de um predicado (colocado no lado esquerdo do operador :-, e designado por cabeça da regra) à validade de um conjunto de outros predicados (designados por corpo da regra). A título de exemplo, temos que a regra:
avo(X,Y) :- pai(X,Z), pai(Z,Y).
Quando acrescentada à base de conhecimento apresentada acima, permite que o Prolog responda afirmativamente ao predicado avo(francisco,manuel). No processo, o interpretador verificará os predicados pai(francisco,joao) e pai(joao,manuel).
Note que nas regras, as variáveis que ocorrem na cabeça da regra devem ser entendidas como quantificadas universalmente (como nos factos). Já as que só ocorrem no corpo da regra devem ser entendidas como quantificadas existencialmente (como nos objectivos).
Exercício: Extenda a base de conhecimento para exprimir outros graus de parentesco, como "irmão", "tio", etc.
Aula 10: Predicados de Segunda Ordem e outros predicados primitivos disponibilizados pelo Prolog
Predicados de segunda ordem
Existem meta-predicados que permitem coleccionar todas as soluções para um dado
objectivo de prova (ver User's Manual ou o help).
findall(?Template,:Goal,?Bag) : Bag é a lista de instâncias de Template encontradas nas provas de Goal. A ordem da lista corresponde à ordem em que são encontradas as respostas. Se não existirem instanciações para Template, Bag unifica com a lista vazia.
bagof(?Template,:Goal,?Bag) : Semelhante a findall, mas se Goal falhar, bagof falha.
setof(?Template,:Goal,?Set) : Semelhante a bagof, mas a lista é ordenada e sem repetições.
Exemplo:
| ?- findall(X, member(X,[1,2,3]), L).
L = [1,2,3]
yes
Relacionados com os apresentados, encontramos outros predicados de ordem superior, como o bem conhecido map (do haskell). No Prolog o predicado maplist implementa a funcionalidade análoga.
Exercícios:
Teste os predicados apresentados codificando exemplos apropriados.
Utilize o predicado findall para determinar todas as soluções para o problema das N rainhas com N=8.
Outras características do Prolog
Manipulação da base de conhecimento: O Prolog permite manipular dinamicamente a base de conhecimento (inserir ou remover factos ou regras). Para isso disponibiliza os predicados assert, retract, rectractall (e variantes...).
Input/Output: tal como qualquer linguagem com o mínimo de preocupações práticas, é possível realizar operações de Input/Output. Para o efeito dispõe-se dos predicados write, read (entre outros, e com muitas variantes...); open e close para maniputação de ficheiros, etc...
Exercícios:
Consulte a documentação relativa aos predicados referidos e teste cada um deles com exemplos apropriados.
Extenda o programa das N rainhas com um predicado runQueens que interrogue o utilizador sobre o número de rainhas a considerar e imprima no écran todas as soluções admissíveis.
Aula 9: Estratégia Gerar e Testar.
Estratégia Gerar e Testar
O mecanismo de backtracking do PROLOG torna possível codificar, de forma directa, a estratégia de gerar e testar para encontrar a solução de um determinado problema. Segundo esta estratégia, o problema é decomposto em duas fases:
Gera-se "soluções cadidatas" para o problema.
Verifica-se se a "solução candidata" satisfaz os requisitos do problema (e é, portanto, uma "solução efectiva").
Podemos assim identificar o padrão com a seguinte regra PROLOG:
resolve(X) :- gera(X), testa(X).
Note-se o papel preponderante do backtracking para encontrar uma dada solução para resolve(X): o predicado gera(X) instancia X com uma possível solução. No caso de testa(X) falhar (a solução proposta não satisfaz os requisitos impostos pelo problema), o mecanismo de backtracking permite que gera(X) instancie uma nova alternativa, até que se encontre a solução pretendida.
O predicado gera acaba normalmente por se revelar o ponto crítico na aplicação desta estratégia: por um lado, pretende-se que ele cubra todas as possíveis soluções para o problema (caso contrário, podemos nunca gerar a solução requerida). Por outro, e por questões de eficiência, vamos pretender que ele produza o mínimo de soluções erradas (para minimizar o espaço de busca) -- na prática, este esforço de minimização traduz-se por eliminar candidatos notoriamente errados e por encontrar codificações apropriadas para as possíveis soluções.
Vejamos um exemplo concreto: pretende-se encontrar um divisor para um dado número N (diferente de 1 e N).
fromToL(L,U,[]) :- U < L, !.
fromToL(L,U,[L|X]) :- L1 is L+1, fromToL(L1,U,X).
gera(N,X) :- fromToL(2,N-1,L), member(X,L).
testa(N,X) :- N mod X =:= 0.
divisor(N,X) :- gera(N,X), testa(N,X).
Mas o programa apresentado pode ser consideravelmente optimizado se observarmos que nos é suficiente encontrar um divisor entre 2 e sqrt(N) (se X>sqrt(N) é um divisor de N, então também será N/X<sqrt(N)). Dessa forma teríamos:
divisor2(N,X) :- fromtoL(2,sqrt(N),L), member(X,L), N mod X =:= 0.
Verifique ambos os programas para um número primo elevado (e.g. 209953, 331777, 472393, ...)
Utilize a estratégia generate & test para determinar a raiz de um natural, definida da seguinte forma: um número natural X é a raiz de N quando X2<=N e (X+1)2>N
Problema das N rainhas.
Um exemplo clássico de programação em PROLOG consiste em escrever um predicado que permita resolver o problema das n rainhas. Esse problema consiste em dispor n rainas num tabuleiro de damas com dimensão n*n, sem que qualquer rainha se encontre ameaçada por outra. Como um exemplo de uma solução temos (num tabuleiro 4*4):
Q
Q
Q
Q
Note que cada linha e cada coluna deve conter uma, e só uma, rainha (porquê?).
Dito isto, verificamos que uma forma expedita de representar as soluções para este problema consiste em utilizar uma lista que informe qual a coluna em que é colocada a rainha de cada uma das linhas (a solução do exemplo seria [3,1,4,2], querendo dizer que a rainha da primeira linha aparece na terceira coluna, a da segunda linha na primeira coluna, etc.) -- desta forma, aparece uma rainha em cada linha "por construção". A restrição de aparecer uma única rainha por cada coluna é traduzida por deverem aparecer na lista todos os números de 1 a 4, ou seja, a lista deve ser uma permutação de [1,2,3,4]. Temos assim resolvido o sub-problema de gerar soluções candidatas: são simplesmente permutações da lista [1..N].
Na fase de teste, falta unicamente verificar que nenhuma rainha está no alcance da diagonal de uma outra. Para isso notamos que:
Duas rainhas estão numa diagonal / sse a soma da linha e coluna da posição de cada uma delas for igual;
Duas rainhas estão numa diagonal \ sse a diferença da linha e coluna da posição de cada uma delas for igual.
Com base no que foi referido, codifique um predicado nrainhas(+N,?X) que determine uma solução para o problema das N-rainhas.
Aula 8: Implementação do algoritmo Davis-Putnam em Prolog.
Pretende-se definir um programa que permita verificar se uma dada fórmula é uma contradição pelo método de Davis Putnam. Para o efeito, sugere-se que considere o seguinte predicado matCNF que converte uma Forma Normal Conjuntiva (FNC) na respectiva forma matricial (como uma lista de listas):
% -----------------------------------------------------------------
% matCNF(+FNC,?MAT)
%
% FNC é uma forma normal conjuntiva e MAT é a sua representação sob a forma
% de matriz (lista de listas de literais).
% obs: os literais são da forma "atom" ou "-atom".
matCNF((A /\ B),M) :- !, matCNF(A,MA), matCNF(B,MB), append(MA,MB,M).
matCNF((A \/ B),C) :- !, matCNF(A,[CA]), matCNF(B,[CB]), union2(CA,CB,C).
matCNF(~Lit, [[-Lit]]) :- !.
matCNF(Lit, [[Lit]]).
union2([],L,[L]).
union2([X|L1],L2,L3) :- member2(X,L2), !, union2(L1,L2,L3).
union2([X|_],L2,[]) :- (-Xn=X;-X=Xn), member2(Xn,L2), !.
union2([X|L1],L2,L3) :- union2(L1,[X|L2],L3).
member2(X,[Y|_]) :- X==Y, !.
member2(X,[_|T]) :- member2(X,T).
Exercícios:
Defina o predicado de split/3 que determine o particionamento de uma FNC.
Defina o predicado davisPutnam/1 que verifique se uma fórmula proposicional é inconsistente.
Aula 7: Lógica Proposicional em Prolog.
Cálculo de Sequentes.
Pretende-se definir um predicado em Prolog que implemente as regras do cálculo de sequentes LC. Para tal deverá considerar que os sequentes são constituídos por pares de listas, sendo portanto o predicado pretendido da forma lc(+Gamma,+Delta) (Gamma e Delta são listas de fórmulas e o predicado verificará se o sequente Gamma |- Delta é válido ou não).
Formas Normais.
Defina os predicados:
nnf(+Form, -NNF) que determine a forma normal negativa de uma fórmula.
cnf(+NNF, -CNF) que determina a forma normal conjuntiva (FNC) de uma fórmula dada na FNN.
Aula 6: Manipulação de fórmulas de lógica proposicional em Prolog.
Definição de Operadores em Prolog.
O Prolog permite definir operadores prefixos, sufixos ou infixos. Para tal devemos utilizar o predicado pré-definido op(Prec,Type,Name). O argumento Name é o nome do operador definido; Prec é um número entre 0 e 1200 que determinará a sua precedência e Type determina o seu tipo e associatividade. Por exemplo, o operador de soma binário + está definido como op(700, yfx, +). A precedência 700 irá determinar que tenha menos precedência do que a multiplicação (definida com precedência 500 - note que um número menor indica maior precedência do operador), e o tipo yfx caracteriza o operador como infixo e associativo à esquerda. Outras possibilidades para o tipo dos operadores são: xfy, xfx para operadores infixos associativos à direita e sem associatividade; fx, fy para operadores prefixos e xf, yf para operadores sufixos.
Alguns dos operadores pré-definidos do Prolog são:
Faça um pequeno predicado que lhe permita confirmar a maior precedência do operador * face ao operador +.
Manipulação de fórmulas de lógica proposicional em Prolog.
A definição de operadores permite que a sintaxe do Prolog se aproxime do domínio onde se está a trabalhar. Considere que se pretendem representar fórmulas da Lógica Proposicional em Prolog. Em vez de considerar termos como or(not(p), and( and(p, r), not(q))), podemos utilizar operadores que nos permitam aproximar a sua representação da utilizada habitualmente. Assim definimos:
que denotam os operadores de implicação, disjunção, conjunção e negação. Assim, a fórmula apresentada atrás pode ser escrita como (~p \/ p /\ r /\ ~q) (note o papel da precedência e associatividade).
Exercícios:
Defina o predicado props(+Form,-Props) que calcule o conjunto de símbolos de proposições utilizados na fórmula dada.
Defina o predicado val(+Form,+Mod) que verifique se a fórmula é válida no modelo passado como argumento.
Como poderia reformular a definição do predicado val por forma a que não seja necessário instanciar o modelo (ou seja, construir o predicado valM(+Form, ?Mod).
Aula 5: Utilização de cut e negação por falha.
O predicado pré-definido cut (!) permite eliminar ramos nas árvores de derivação de predicados Prolog. Operacionalmente, o cut pode ser caracterizado da seguinte forma: Durante o processo de prova, a 1a passagem pelo cut é sempre verdadeira (com sucesso). Se por backtracking se voltar ao cut, então o cut faz falhar o predicado que está na cabeça da regra.
A utilização do cut está normalmente associada a questões de eficiência: os ramos da árvore que são eliminados acabariam eventualmente por falhar, e assim poupamos trabalho ao motor de inferência do Prolog. Esta utilização do cut é considerada benigna (green cut), porque não se afecta o significado dos predicados. Tomemos como exemplo um predicado que verifique se o terceiro argumento é o mínimo dos dois primeiros. Podería ser definido como:
minimo(X,Y,Y) :- X >= Y.
minimo(X,Y,X) :- X < Y.
Mas podemos facilmente observar que, uma vez verificado que X>=Y, não faz sentido tentar verificar que X<Y. Assim sendo, faz sentido colocar um cut no final da primeira cláusula:
minimo(X,Y,Y) :- X >= Y, !.
minimo(X,Y,X) :- X < Y.
Estaria correcto eliminar também o predicado X<Y na segunda cláusula? Justifique com exemplos apropriados.
É importante referir que certas utilizações do cut alteram propositadamente o comportamento do programa (tipicamente para impedir que a execução do programa entre em ciclo). Essas utilizações são normalmente consideradas "mais perigosas" (red cuts) porque obrigam a que o programador detenha uma ideia muito precisa sobre o processo de construção da derivação por parte do Prolog.
Mostre, avaliando um objectivo apropriado, que o programa está incorrecto.
Como o poderá corrigir?
Negação por falha.
Por vezes pretende-se garantir que um dado predicado não é válido. A utilização do cut (em conjunção com o predicado pré-definido fail que falha sempre) permite codificar uma forma restrita de negação: a "negação por falha". Considere o seguinte predicado:
neg(X) :- X, !, fail.
neg(X).
Note que neg(X) falha sempre que o Prolog consiga construir uma derivação para X. Por outro lado, sucede se falhar na construção dessa derivação (entra na segunda cláusula, que é trivialmente satisfeita). Obs.: o predicado pré-definido do Prolog \+ corresponde ao predicado neg apresentado.
Verifique o resultado de neg em predicados já definidos.
Construa a árvore de procura de soluções para a questão takeout(X,[1,2,3],Y).
Utilize o predicado takeout para definir um predicado que determine se uma lista é permutação de uma outra.
Tipos Algébricos
A utilização de termos permite a manipulação em Prolog de valores de tipos algébricos (que em Haskell seriam declarados com data). Um primeiro exemplo disso já foi ilustrado na última aula quando se manipularam naturais (zero, suc(zero), etc.). Para sistematizar, vejamos agora como manipular um outro tipo algébrico bem conhecido: as árvores binárias. Uma escolha óbvia para representar os seus valores será considerar o átomo vazia para representar a árvore vazia e termos da forma nodo(X,E,D) para representar nodos intermédios (com valor X, sub-árvore esquerda E e sub-árvore direita D). Temos então como exemplos de termos: vazia, nodo(4, vazia, vazia), etc.
Note no entanto que em Prolog não existe a noção de tipo (e.g. não podemos, à priori, condicionar um dado argumento de um predicado a ser uma árvore binária --- a única alternativa será definir-se um predicado que suceda para termos que tenham a estrutura prescrita...)
Defina um predicado arvBin/1 que verifique se o termo dado é uma árvore binária (e.g. deve falhar para termos como vazia(nodo,vazia(nodo))).
Defina um predicado que verifique se uma lista é uma travessia in-order de uma árvore.
Defina predicados que determinem:
uma árvore é uma Árvore Binária de Procura
uma lista está ordenada.
Aula 3: Árvores de derivação do Prolog.
Considere-se a definição do predicado member/2
member(X,[X|_]).
member(X,[_|T]) :- member(X,T).
Este predicado foi definido na última aula com o objectivo de verificar se um elemento está contido numa lista. De facto, podemos utiliza-lo como:
Mas podemos também utiliza-lo com variáveis não instanciadas com o objectivo de determinar quais os elementos de uma lista:
?- member(X,[1,2,3]).
X = 1 ;
X = 2 ;
X = 3 ;
fail.
Ou até para determinar soluções a questões mais complicadas, como (mais um exemplo da última aula):
?- member(X,[3,5,4,6,5,7]), X mod 2 =:= 0.
X = 4 ;
X = 6 ;
fail.
O objectivo desta aula é o de se perceber como é que o Prolog consegue chegar às soluções apresentadas (substituições de variáveis que validam o objectivo).
Inferência do Prolog
Um objectivo em Prolog consiste numa lista de predicados. O resultado da "execução" desse objectivo num interpretador consiste numa substituição que verifique esses predicados. O processo construção da substituição é normalmente designado por inferência, e pode ser justificado construindo uma árvore como se descreve:
Na raiz da árvore, coloca-se a lista de predicados. O Prolog irá processar cada predicado dessa lista por ordem.
Para cada predicado, o Prolog irá procurar encontrar na base de conhecimento uma instância dum facto ou duma regra cuja cabeça unifique com esse predicado. Esta procura processa-se também pela ordem pela qual as definições ocorrem na base de conhecimento.
Quando é encontrada uma regra nas condições referidas, cria-se um descendente na árvore contendo a lista já afectada pela substituição resultante da unificação (relembre que o resultada na unificação é uma substituição das variáveis) e onde o predicado em análise é substituído pelo lado direito da regra (ou simplesmente desaparece, no caso dos factos). É habitual anotarmos os arcos da árvore com as substituições resultantes das unificações.
Quando existe mais do que uma possibilidade para a referida unificação (e.g. várias regras são aplicáveis), traduz-se por uma ramificação da árvore de inferência.
Operacionalmente, o Prolog trata esta ramificação pelo mecanismo de backtracking (travessia depth-first da árvore).
Quando a lista de predicados fica vazia, cria-se uma folha na árvore denotada como true --- representa um resultado apresentado ao utilizador (a substituição calculada ao longo do caminho).
Quando não existe qualquer regra na base de conhecimento que unifique com o primeiro predicado da lista, cria-se uma folha denotada por fail .
A árvore de derivação para o objectivo "member(X,[1,2]), X mod 2 ==0" será:
Exercícios:
Considere a seguinte definição do predicado factorial:
fact(1,0).
fact(R,X) :- X2 is X-1, fact(R2,X2), R is X*R2.
Apresente a árvore de inferência para o objectivo fact(R,2).
Comente os resultados obtidos. Explique, em particular, que problemas aponta à solução apresentada.
Como pode ultrapassar os problemas detectados.
Considere o seguinte predicado:
nat2int(zero,0).
nat2int(suc(X),N) :- nat2int(X,N2), N is N2+1.
Apresente a árvore de inferência para o objectivo nat2int(suc(suc(zero)),X).
Apresente a árvore de inferência para o objectivo nat2int(X,2).
Comente os resultados obtidos.
Consegue propor alguma forma de ultrapassar os problemas detectados?
Tracing e Debug
Uma forma expedita de detectar problemas em programas Prolog consiste em utilizar o mecanismo de tracing. Esse mecanismo permite "monitorizar" determinados predicados durante o processo de inferência. Considere-se novamente o objectivo considerado atrás que faz uso do predicado member/2:
?- trace(member).
% member/2: [call, redo, exit, fail]
true.
[debug] ?- member(X,[1,2]), X mod 2 =:= 0.
T Call: (8) member(_G318, [1, 2])
T Exit: (8) member(1, [1, 2])
T Redo: (8) member(_G318, [1, 2])
T Call: (9) member(_G318, [2])
T Exit: (9) member(2, [2])
T Exit: (8) member(2, [1, 2])
X = 2 ;
T Redo: (9) member(_G318, [2])
T Call: (10) member(_G318, [])
T Fail: (10) member(_G318, [])
fail.
Note que o Prolog sinalizada diferentes eventos relativos ao predicado observado:
Call: o predicado em "resolução";
Exit: o predicado foi resolvido com sucesso (pode por isso ser removido da lista de objectivos);
Redo: nova visita ao predicado (por backtracking);
Fail: predicado falha definitivamente (já não existem mais alternativas para o backtracking).
Exercício:
Interprete o resultado do trace apresentado na árvore de inferência apresentada acima.
Realize análises de traces para as restantes árvores construídas nesta aula...
Aula 2: Operações aritméticas e Manipulação de listas.
Operações aritméticas
Já vimos que o Prolog aceita termos que representem expressões matemáticas, como 3+4*2. Mas quando manipulamos esses termos estamos normalmente interessados em avaliar essas expressões (i.e. calcular o seu resultado). O Prolog disponibiliza para o efeito o predicado is que avalia o segundo argumento e unifica o resultado com o primeiro. Alguns exemplos (onde se utiliza a notação infixa para o predicado):
?- X is 3+2.
X = 5.
?- 3+2 is 2+3.
fail.
?- 5 is 3+2.
true.
?- 5 is X+2.
ERROR: is/2: Arguments are not sufficiently instantiated
Um aspecto importante na utilização do predicado is é a assimetria induzida: o segundo argumento deve ser sempre uma expressão completamente instanciada. Assim, se definirmos o predicado:
soma(X,Y,Z) :- X is Y + Z.
devemos considerar o segundo e o terceiro argumentos como "argumentos de entrada", que necessitam estar devidamente instanciados. Uma forma compacta de se exprimir esse facto (normalmente utilizada na documentação) é através da assinatura soma(-X,+Y,+Z) --- assim identifica-se o argumento Y e Z como de entrada e X como de saída.
Exercício:
Defina o predicado factorial(-R,+X) que suceda quando R for o factorial de X.
Uma forma alternativa de lidar com números naturais consiste em considerar termos zero, suc(zero), suc(suc(zero)), etc. (i.e. utilizar notação unária para os naturais). Defina o predicado nat2int que sucede quando o primeiro argumento é a representação unária do segundo.
No predicado definido na alínea anterior, verifique:
que argumentos tem de ser utilizados como entrada e como saída;
o que acontece quando solicita ao interpretador várias respostas.
Verifique, com o auxílio do mecanismo de help do SWI-Prolog (ou da documentação on-line, se preferir) qual a funcionalidade oferecida pelos operadores:
=:=, =\=, <, =<, ==, @<
Manipulação de listas
Um exemplo de um tipo estruturado muito utilizado em Prolog são as listas. A sintaxe pré-definida é [] que denota a lista vazia e [H|T] que denota a lista com cabeça H e cauda T.
Defina member/2 que verifica se um elemento pertence a uma lista.
Utilize o predicado member para determinar quais dos elementos da lista [3,5,4,6,5,7] são pares.
Defina um predicado que permita calcular o somatório de uma lista de inteiros.
O que alteraria, no predicado definido na alínea anterior, para calcular o somatório de uma lista de expressões inteiras?
Defina o predicado concat/3 que verifique quando uma lista é a concatenação de outras duas. Verifique o resultado quando o invoca com diferentes listas instanciadas.
Aula 1: Apresentação da linguagem PROLOG
Ao longo das aulas práticas de Lógica Computacional fazer uso da linguagem PROLOG. O interpretador adoptado será o SWI-Prolog que está disponível para para a generalidade das plataformas (MS-Windows, Linux, macOSX).
Conceitos Preliminares
Termos: o Prolog é uma linguagem simbólica que manipula termos que podem ser:
Variáveis - denotadas por identificadores começados por letras maiúsculas (e.g. X, Y, Xs, ...);
Constantes - átomos (identificadores começados por letras minúsculas) ou valores de tipos pré-definidos como inteiros, reais, strings, etc. (e.g. abc, xyz, 32, 3.1415)
Termos Compostos - termos da forma f(t1,...,tn) onde f é designado por functor (nome da função) e t1...tn são termos (e.g. xyz(X,abc), abc(abc(abc,abc)), +(4,2))
obs.: como iremos ver adiante, o Prolog permite a declaração de operadores infixos. Assim irá permitir escrever 4 + 2 como alternativa ao termo +(4,2) (o mesmo se aplica a outros operadores infixos que serão apresentados adiante).
Substituições e Unificação: o que caracteriza as variáveis é o facto de elas poderem vir a ser substituidas por outros termos. Considere-se o termo t(X,Y): se substituirmos X por abc(A,3) e Y por Z obtemos o termos t(abc(A,3),Z).
Uma operação fundamental no modelo de execução do Prolog é o que se designa por Unificação de dois termos. A ideia consiste em encontrar uma substituição que iguale (se possível) os termos dados. Vejamos alguns exemplos:
X = 4, Y = 3 é um unificador dos termos abc(3,X) e abc(Y,4);
X = 4, Y = 3 é um unificador dos termos abc(X,X) e abc(Y,4);
os termos abc(3,4) e abc(X,X) não dispõe de unificador.
Uma característica dos unificadores apresentados é que se tratam sempre dos unificadores mais gerais (qualquer outra substituição que unifique os termos pode ser expressa como um refinamento da substituição dada). Adiante iremos ter oportunidade de aprofundar estes aspectos mais teóricos... Para já interessa reter que o Prolog, quando unificar dois termos, determina sempre o unificador mais geral (i.e. a substituição mais simples que iguala os termos).
EXERCÍCIO: Determine o unificador mais geral para os seguintes pares de termos (se existir... naturalmente):
f(X,g(Y)) e g(X,f(Y))
f(X,g(Y)) e Z
f(X,g(y)) e f(g(y),X)
f(X) e X
f(X) e f(3+2)
f(3) e f(2+1)
f(3) e A(X)
Programas em Prolog
Executar um programa em Prolog consiste em interrogar o interpretador sobre a validade de um dado predicado lógico. A resposta mais simples será então true ou fail (se o predicado for válido ou não, respectivamente).
Objectivo (Goal):
Quando se invoca o SWI-Prolog, surge o prompt?- que assinala que o interpretador aguarda a introdução de um objectivo (ou query, ou goal).
Calvin:~ jba$ /opt/local/bin/swipl
Welcome to SWI-Prolog (Multi-threaded, 32 bits, Version 5.6.51)
Copyright (c) 1990-2008 University of Amsterdam.
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software,
and you are welcome to redistribute it under certain conditions.
Please visit http://www.swi-prolog.org for details.
For help, use ?- help(Topic). or ?- apropos(Word).
?-
Como referimos, o objectivo será um predicado lógico. Iremos ter oportunidade de definir novos predicados mas, para já, concentremo-nos na utilização do predicado pré-definido =/2 (o /2 significa que o predicado espera dois argumentos). Este predicado será válido precisamente quando os termos que forem passados como argumentos unificarem. Assim podemos introduzir:
?- =(3,3).
true.
?- 3=3.
true.
?- 3=2.
fail.
?- 3=X.
X = 3.
?- 3+2=X.
X = 3+2.
?- 3 + X = Y * 2.
fail.
?-
Os exemplos apresentados revelam-nos duas coisas: (1) podemos utilizar a notação infixa e, (2) quando no objectivo estão envolvidas veriáveis o Prolog retorna uma substituição dessas variáveis que verifiquem o predicado (ou falha, se não existir nenhuma substituição nessas condições) --- podemos então dizer que, intuitivamente, as variáveis dos objectivos estão quantificadas existencialmente.
EXERCÍCIO: Interrogue o interpretador de Prolog por forma a ele retornar os unificadores mais gerais atrás solicitados.
Factos (base de conhecimento I):
Referimos que executar um programa em Prolog consiste em interrogar o interpretador relativamente a um objectivo. Mas, em que é que consiste um programa Prolog?. Um programa em Prolog será a base de conhecimento que o interpretador utiliza para determinar a validade do objectivo pedido. Essa base de conhecimento será consituída por:
Factos: que estabelecem a validade imediata (de instâncias) de predicados;
Regras: que condicionam a validade de predicados à validade de sub-objectivos.
Comecemos pelos primeiros. Como exemplos de factos podemos ter:
Com base nestes factos, diriamos que pai(joaquim,manuel) é válido mas pai(joaquim,jose) já não o é (porque nada estabelece a sua validade). Para verificar isso com o Prolog, necessitamos de carregar a base de conhecimento no interpretador. Para tal devemos:
gravar um ficheiro com os factos apresentados (normalmente dá-se a extensão ".pl" aos ficheiros Prolog, e.g. "pai.pl");
carregar o ficheiro no interpretador por intermédio do predicado pré-definido consult (e.g. "consult(pai.pl)").
EXERCÍCIO: Verifique a validade de alguns objectivos com a base de conhecimento apresentada. O que acontece quando se inclui variáveis?
Por vezes, o interpretador retorna uma substituição de resultado sem voltar ao prompt inicial. Isso assinala que a solução apresentada é uma de várias possíveis, podendo o utilizador:
digitar . e retornar ao prompt inicial;
digitar ; para solicitar outra solução.
EXERCÍCIO:
introduza um predicado que permita determinar todos os filhos de "manuel".
o que aconteceria se incluisse na base de conhecimento o facto pai(X,carlos) ? Experimente... (verifique o impacto de o incluir no início e no fim da base de conhecimento).
O exercício anterior permite concluir que, nos factos, devemos realizar uma interpretação universal das variáveis.
Se as questões colocadas ao interpretador de Prolog são predicados lógicos, é natural perguntarmo-nos como construir predicados à custa de conectivas lógicas (como e, ou, etc.). O Prolog tem definido os operadores:
conjunção: denotado por uma vírgula (,)
disjunção: denotado por um ponto e vírgula (;)
(As restantes conectivas lógicas proposicionais serão introduzidas mais tarde.)
Regras (base de conhecimento II):
A expressividade do Prolog resulta do facto de permitir incluir, na base de conhecimento, regras que condicionam a validade de um predicado (colocado no lado esquerdo do operador :-, e designado por cabeça da regra) à validade de um conjunto de outros predicados (designados por corpo da regra). A título de exemplo, temos que a regra:
avo(X,Y) :- pai(X,Z), pai(Z,Y).
Quando acrescentada à base de conhecimento apresentada acima, permite que o Prolog responda afirmativamente ao predicado avo(francisco,manuel). No processo, o interpretador verificará os predicados pai(francisco,joao) e pai(joao,manuel).
Note que nas regras, as variáveis que ocorrem na cabeça da regra devem ser entendidas como quantificadas universalmente (como nos factos). Já as que só ocorrem no corpo da regra devem ser entendidas como quantificadas existencialmente (como nos objectivos).
Exercício: Estenda a base de conhecimento para exprimir outros graus de parentesco, como "irmão", "tio", etc.
Esta página apresenta algumas ideias para projectos práticos da disciplina de Lógica Computacional. Os alunos interessados em realizar um projecto devem contactar o docente para definir a atribuição respectiva.
Utilização de SMT Provers na verificação de software
O objectivo deste projecto é o de explorar um SMT Prover na verificação de software. Um SMT Prover é uma ferramenta que combina um verificador automático de fórmulas proposicionais com estratégias específicas para lidar com problemas de decisão em teorias específicas (como aritmética linear, manipulação de arrays, etc.). Essas teorias são particularmente orientadas para cobrir as obrigações de prova resultantes da verificação de programas.
Com este projecto pretende-se validar esse desígnio verificando as obrigações de prova resultantes de programas concretos com um SMT Prover. Como gerador de obrigações de prova sugere-se a utilização de WHY (http://why.lri.fr/index.en.html) e como SMT prover o YICES (http://yices.csl.sri.com/).
Codificação de ORBDDs em Haskell
A codificação de Binary Decision Diagrams (BDDs) pressupõe um controlo apertado sobre a gestão de memória e nos algoritmos utilizados na sua construção. Esse facto torna a sua codificação em Haskell um desafio interessante, obrigando à utilização de Monads para permitir aspectos imperativos na sua programação.
Este projecto pretende estudar a implementação de BDDs em Haskell. Tanto pode incidir sobre a codificação "de raiz" dessas estruturas como pode adoptar uma implementação pré-existente a analisar a sua implementação e o respectivo desempenho (e.g. comparando-a com uma biblioteca análoga desenvolvida em C).
Um dos algoritmos mais utilizados na verificação de fórmulas proposicionais é o Davis-Putnam(-Logemann-Loveland). Este projecto propõe-se estudar a implementação desse algoritmo em Haskell. Tal como no caso do projecto anterior, o âmbito deste projecto tanto pode incidir sobre a codificação de raiz do algoritmo, como no estudo de uma implementação existente.
O objectivo deste projecto é o de explorar o demonstrador de teoremas COQ para realizar provas simples. Sugere-se que os interessados realizem os exemplos do tutorial e de o surveyCoq in a Hurry.
Para aplicar os conceitos estudados, devem escolher um (ou mais) dos desafios apresentados. Note que o trabalho é individual e a escolha do desafio deve ser sempre combinada com o docente. Para a entrega devem apresentar um pacote com o conjunto das scripts desenvolvidas (quer dos exemplos realizados, quer do desafio escolhido), "abundantemente" comentadas (preferencialmente fazendo uso da ferramenta coqdoc para produzir um documento contendo essas scripts). As sessões de apresentação irão consistir na execução e discussão das referidas scripts.
29/05: Cálculo de sequentes em Lógica de Primeira Ordem.
22/05: Formas Prenex e Skolenização.
15/05: Tolerância de ponto: enterro da gata.
08/05: BDDs: redução e construção bottom-up.
24/04: Algoritmo Davis-Putman: exercícios de aplicação.
17/04: Algoritmo de resoluçao de Robinson: exemplos de aplicação.
27/03: Formas clausais: Fórmulas Normais Conjuntivas e Fórmulas Normais Disjuntivas. Resulução proposicional.
20/03: Avaliação de fórmulas proposicionais por aplicação do método tableaux. Formas normais negativas.
13/03: Demonstrações simples envolvendo indução sobre estrutura das fórmulas e derivações em sistemas de dedução. Construção de derivações no sistema de cálculo de sequentes.
06/03: Exercícios sobre noções elementares da lógica proposicionais: validade de fórmulas; consequência semântica; derivações em Dedução Natural.
20/03: Continuação da manipulação de listas. Exploração do mecanismo de backtracking.
13/03: Utilização de termos, introdução à manipulação de Listas.
06/03: Apresentação da linguagem Prolog.
27/02: Inscrição nos turnos.
Docente: Olga Pacheco
Aulas Teórico-Práticas
17/03: Prova de que a relação de consequência semântica é uma relação de dedução.
Representação no cálculo de sequentes das regras da dedução natural.
07/03: Exercícios sobre noções elementares da lógica proposicional: validade de fórmulas; consequência semântica; derivações em Dedução Natural.
28/02: Inscrição nos turnos.
Aulas Práticas
14/03: Utlilização de termos estruturados. Representação dos naturais baseada nos construtores 0 e sucessor
(definição dos predicados: menor, maior ou igual, soma e multiplicação).
Manipulação de listas em Prolog (definição dos predicados: cabeça, cauda, ultimo elemento, elemento na posição n, e membro).
07/03: Apresentação da linguagem Prolog.
Representação em Prolog de informação sobre árvores geneológicas (definição dos predicados: mãe, pai, irmão, tio, avô, avó, avô paterno, avó paterna, bisavô, bisavó,...).
06/03: Revisões de Lógica Proposicional: sintaxe das fórmulas; noção de modelo e validade; tautologias e contradições; teorias; consequência semântica.
11/03: Relações de dedução. Sistema de Dedução Natural (formulação clássica e com sequentes).
13/03: Propriedades do sistema de Dedução Natural. Apresentação do Cálculo de Sequentes.
27/03 (15:00): Demonstração do teorema de Correcção e Completude do sistema de Dedução Natural.
27/03: Continuação das demonstrações de Correcção e Completude do sistema de Dedução Natural.
01/04: Esboço das demonstrações da Correcção e Completude do Cálculo de Sequentes e da propriedade de Eliminação do Corte. Apresentação do método de Tableaux.
03/04: Formal Normal Negativa (FNN) e Formais Clausais (Forma Normal Disjuntiva (FND) e Forma Normal Conjuntiva (FNC)).
08/04: Método de resolução proposicional. Apresentação do algoritmo de Robinson e ilustração da aplicação.
10/04: Algoritmo de Davis-Putnam.
15/04: BDDs: motivação e definição; redução de árvores de decisão binárias.
17/04: Construção bottom-up de BDDs.
22/04: TESTE INTERMÉDIO.
24/04: Lógica de Primeira Ordem: Sintaxe e Semântica.
29/04: Formas Normais: Prenex; Herbrand e Skolen.
06/05: Modelos de Herbrand.
08/05: Não houve aula (impossibilidade do docente).
13/05: Tolerância de Ponto: Enterro da Gata.
15/05: Tolerância de Ponto: Enterro da Gata.
20/05: Cálculo de Sequentes para Lógica de Primeira Ordem.
27/05: Resolução Proposicional em Lógica de Primeira Ordem.
29/05: Unificação.
03/06: Resolução de Primeira Ordem.
05/06: Analogia de Curry Howard: motivação; normalização das provas.
10/06: Sistemas de Anotação de Provas para Dedução Natural. Lambda-Calculus com tipos.
12/06: Esclarecimento de dúvidas. Correcção do primeiro teste.
TP1
Aulas Teórico-Práticas (3ª 10:00-11:00)
26/02: Não houve aula.
04/03: Não houve aula.
11/03: Exercícios sobre validade e consequência semântica.
01/04: Exercícios sobre relações de dedução. Construção de árvores em Dedução Natural.
08/04: Exercícios sobre construção de derivações no Cálculo de Sequentes.
15/04: Exercícios sobre Formas Clausais e Resolução Proposicional.
22/04: TESTE INTERMÉDIO.
29/04: Exercícios spbre método Davis Putnam .
06/05: Exercícios sobre validade em lógica de primeira ordem.
13/05: Tolerância de Ponto: Enterro da Gata.
20/05: Exercícios sobre formas normais (prenex, skolen e herbrand)
27/05: Exercícios sobre cálculo de sequentes para lógica de predicados.
TWiki's Education/LC webThe Education/LC web of TWiki. TWiki is a Web-Based Collaboration Platform for the Enterprise.http://wiki.di.uminho.pt/twiki/bin/view/Education/LCCopyright 2020 by contributing authors2020-10-30T14:39:17ZWebStatisticshttp://wiki.di.uminho.pt/twiki/bin/view/Education/LC/WebStatistics2020-10-30T14:39:17ZStatistics for Education/LC Web Month: Topic views: Topic saves: File uploads: Most popular topic views: Top contributors for topic save ... (last changed by TWikiGuest)TWikiGuestWebHomehttp://wiki.di.uminho.pt/twiki/bin/view/Education/LC/WebHome2010-02-18T13:06:08ZEsta disciplina tem por objectivo aprofundar a relação existente entre lógica formal e a computação. Esta relação pode assumir diferentes formas, dependendo da perspectiva ... (last changed by OlgaPacheco)OlgaPachecoMaterialApoiohttp://wiki.di.uminho.pt/twiki/bin/view/Education/LC/MaterialApoio2010-02-18T13:00:50ZSlides Lógica Proposicional I Cálculo de Sequentes (versão: 11/06/2008) Lógica Proposicional II Método Tableaux , Formas Clausais, Resolução (versão: 11 ... (last changed by OlgaPacheco)OlgaPachecoAvisos0809http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Avisos08092009-07-22T17:28:03Z22/07/2009: Disponíveis notas da época de recurso. 07/05/2009: Disponível enunciado do projecto prático. 06/03/2009: Já disponível o guião da primeira aula pr ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeida0809http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/08092009-07-22T17:27:12ZLógica Computacional (8504N2) em Matemática e Ciências de Computação 2º Ano 2º Semestre Ano lectivo 2008/2009 Equipa Docente José Carlos Bacelar ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaProgDetalhado0809http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/ProgDetalhado08092009-06-18T22:10:46ZPrograma detalhado do ano lectivo 2008/2009 Lógica Proposicional Sintaxe e Semântica Sistemas Dedutivos Dedução Natural ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaPrograma0809http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Programa08092009-06-18T22:10:01ZPrograma Resumido Componente Teórica Lógica Proposicional Sintaxe e Semântica Sistemas Dedutivos Métodos de Verificação Aspectos ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaPraticas0809http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Praticas08092009-05-29T23:07:19ZAulas Práticas #Aula10P Aula 10: Predicados de Segunda Ordem e outros predicados primitivos disponibilizados pelo Prolog Predicados de segunda ordem Existem meta ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaProjectos0809http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Projectos08092009-05-08T02:24:38ZProjecto O objectivo deste projecto é o de explorar o demonstrador de teoremas COQ para realizar provas simples. Sugere se que os interessados realizem os exemplos ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaTopicos0809http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Topicos08092009-02-12T17:21:40ZCalendário (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaCalendariohttp://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Calendario2009-02-12T17:16:45Z (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaSumarios0708http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Sumarios07082009-02-01T18:25:15ZSumários Aulas Teóricas (3ª 14:00 15:00; 5ª 16:00 17:00) 26/02: Não houve aula. 28/02: Não houve aula. 04/03: Aula de substituição em 27/03 , às 15:00. 06 ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaSumarios0809http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Sumarios08092009-02-01T18:23:00ZSumários Aulas Teóricas (3ª 14:00 15:00; 5ª 16:00 17:00) TP1 Aulas Teórico Práticas (2ª 16:00 17:00) Aulas Práticas (2ª 17:00 19:00) TP2 Aulas Teórico Pr ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeida0708http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/07082009-02-01T18:16:25ZLógica Computacional (8504N2) em Matemática e Ciências de Computação 2º Ano 2º Semestre Ano lectivo 2007/2008 Equipa Docente José Carlos Bacelar ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaWebPreferenceshttp://wiki.di.uminho.pt/twiki/bin/view/Education/LC/WebPreferences2009-02-01T18:15:29ZEducation/LC Web Preferences The following settings are web preferences of the Education/LC web. These preferences overwrite the site level preferences in ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaMFES0809http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/MFES08092008-12-05T23:17:24ZAnálise, Modelação e Teste de Software MFES Mestrado de Informática 13/11/2008 "Design by Contract and Java Modeling Language": apresentação do conceito e clausulas ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeida
Esta disciplina tem por objectivo aprofundar a relação existente entre lógica formal e a computação. Esta relação pode assumir diferentes formas, dependendo da perspectiva ...
22/07/2009: Disponíveis notas da época de recurso. 07/05/2009: Disponível enunciado do projecto prático. 06/03/2009: Já disponível o guião da primeira aula pr ...
Aulas Práticas #Aula10P Aula 10: Predicados de Segunda Ordem e outros predicados primitivos disponibilizados pelo Prolog Predicados de segunda ordem Existem meta ...
Projecto O objectivo deste projecto é o de explorar o demonstrador de teoremas COQ para realizar provas simples. Sugere se que os interessados realizem os exemplos ...
Education/LC Web Preferences The following settings are web preferences of the Education/LC web. These preferences overwrite the site level preferences in ...
Análise, Modelação e Teste de Software MFES Mestrado de Informática 13/11/2008 "Design by Contract and Java Modeling Language": apresentação do conceito e clausulas ...
24/09: Já estão disponíveis as notas da época de especial. 28/07: Já estão disponíveis as notas da época de recurso. 02/07: Já estão disponíveis as notas do 2 ...
Aulas Práticas #Aula9P Aula 9: Implementação do algoritmo Davis Putnam em Prolog. Pretende se definir um programa que permita verificar se uma dada fórmula é uma ...
Propostas de Projectos Práticos 2007/2008 Esta página apresenta algumas ideias para projectos práticos da disciplina de Lógica Computacional. Os alunos interessados ...
Elementos Lógicos da Programação II (702752) Licenciatura de Matemática e Ciências da Computação 2º Ano 2º Semestre Ano lectivo 2004/2005 Programa Programa ...
31/07 Já estão disponíveis as notas referentes à Época de Recurso. (aqui) 17/07 Já estão disponíveis as notas referentes à Época Normal. (aqui) 20/06 Foram disponibilizados ...
Sumários Docente: José Carlos Bacelar Aulas Teóricas 08/06: Esclarecimento de dúvidas. 05/06: Referência às propriedades básicas do Lambda calculus com tipos ...
Aulas Práticas #Aula8P Aula 8: Predicados de Segunda Ordem Existem meta predicados que permitem coleccionar todas as soluções para um dado objectivo de prova (ver ...
A resolução da ficha de avaliação prática 3 (enunciado da ficha está na página) é para ser entregue na aula prática de 2 de Junho . MariaJoaoFrade 25 May 2006 ...
Esta disciplina tem por objectivo aprofundar a relação existente entre lógica formal e a computação. Esta relação pode assumir diferentes formas, dependendo da perspectiva sobre a qual é analisada:
Uma primeira perspectiva consiste em eleger o processo de verificar a validade de fórmulas lógicas como problema computacional - por outras palavras, procuram-se construir programas que estabeleçam a validade de fórmulas lógicas. Tal como iremos ter oportunidade de estudar neste curso, este problema é difícil, mesmo para lógicas muito simples (e.g. lógica proposicional).
Uma segunda perspectiva consiste em adoptar a noção de dedução lógica como motor de cálculo de uma linguagem de programação. Uma destas linguagens é o Prolog, que será estudada neste curso.
Por último, iremos também abordar o que é habitualmente designado por Analogia de Curry-Howard: esta analogia permite-nos estabelecer um paralelo entre sistemas lógicos e linguagens de programação funcionais, constituindo assim uma fundamentação lógica para essas linguagens.
A resolução da ficha de avaliação prática 3 (enunciado da ficha está na página) é para ser entregue na aula prática de 2 de Junho . MariaJoaoFrade 25 May 2006 ...
31/07 Já estão disponíveis as notas referentes à Época de Recurso. (aqui) 17/07 Já estão disponíveis as notas referentes à Época Normal. (aqui) 20/06 Foram disponibilizados ...
24/09: Já estão disponíveis as notas da época de especial. 28/07: Já estão disponíveis as notas da época de recurso. 02/07: Já estão disponíveis as notas do 2 ...
22/07/2009: Disponíveis notas da época de recurso. 07/05/2009: Disponível enunciado do projecto prático. 06/03/2009: Já disponível o guião da primeira aula pr ...
Elementos Lógicos da Programação II (702752) Licenciatura de Matemática e Ciências da Computação 2º Ano 2º Semestre Ano lectivo 2004/2005 Programa Programa ...
Análise, Modelação e Teste de Software MFES Mestrado de Informática 13/11/2008 "Design by Contract and Java Modeling Language": apresentação do conceito e clausulas ...
Aulas Práticas #Aula8P Aula 8: Predicados de Segunda Ordem Existem meta predicados que permitem coleccionar todas as soluções para um dado objectivo de prova (ver ...
Aulas Práticas #Aula9P Aula 9: Implementação do algoritmo Davis Putnam em Prolog. Pretende se definir um programa que permita verificar se uma dada fórmula é uma ...
Aulas Práticas #Aula10P Aula 10: Predicados de Segunda Ordem e outros predicados primitivos disponibilizados pelo Prolog Predicados de segunda ordem Existem meta ...
Propostas de Projectos Práticos 2007/2008 Esta página apresenta algumas ideias para projectos práticos da disciplina de Lógica Computacional. Os alunos interessados ...
Projecto O objectivo deste projecto é o de explorar o demonstrador de teoremas COQ para realizar provas simples. Sugere se que os interessados realizem os exemplos ...
Sumários Docente: José Carlos Bacelar Aulas Teóricas 08/06: Esclarecimento de dúvidas. 05/06: Referência às propriedades básicas do Lambda calculus com tipos ...
Esta disciplina tem por objectivo aprofundar a relação existente entre lógica formal e a computação. Esta relação pode assumir diferentes formas, dependendo da perspectiva ...
Education/LC Web Preferences The following settings are web preferences of the Education/LC web. These preferences overwrite the site level preferences in ...
This is a subscription service to be automatically notified by e-mail when topics change in this Education/LC web. This is a convenient service, so you do not have to come back and check all the time if something has changed. To subscribe, please add a bullet with your WikiName in alphabetical order to this list:
Each TWiki web has an automatic e-mail notification service that sends you an e-mail with links to all of the topics modified since the last alert.
Users subscribe to email notifications using their WikiName or an alternative email address, and can specify the webs/topics they wish to track using one of these bullet list formats:
three spaces * [ webname . ] wikiName - SMTP mail address three spaces * [ webName . ] wikiName three spaces * SMTP mail address three spaces * SMTP mail address : topics three spaces * [ webname . ] wikiName : topics
In the above examples, topics is a space-separated list of topic names. The user may further customize the specific content they will receive using the following formats:
Specify topics without a Web. prefix
Topics must exist in this web.
Topics may be specified using * wildcards
Each topic may optionally be preceded by a '+' or '-' sign. The '+' sign means "subscribe to this topic" (the same as not putting anything). The '-' sign means "unsubscribe" or "don't send notifications regarding this topic". This allows users to elect to filter out certain topics (and their children, to an arbitrary depth). Topic filters ('-') take precedence over topic includes ('+').
Each topic may optionally be followed by an integer in parentheses, indicating the depth of the tree of children below that topic. Changes in all these children will be detected and reported along with changes to the topic itself. Note This uses the TWiki "Topic parent" feature.
Each topic may optionally be immediately followed by an exclamation mark ! or a question mark ? with no intervening spaces, indicating that the topic (and children if there is a tree depth specifier as well) should be mailed out as complete topics instead of change summaries. ! causes the topic to be mailed every time even if there have been no changes, ? will mail the topic only if there have been changes to it. This only makes sense for subscriptions.
For example:
Subscribe Daisy to all changes to topics in this web.
* daisy.cutter@flowers.com
Subscribe Daisy to all changes in all webs that start with Web.
* daisy.cutter@flowers.com: Web*
Subscribe Daisy to changes to topics starting with Petal, and their immediate children, WeedKillers and children to a depth of 3, and all topics that match start with Pretty and end with Flowers e.g. PrettyPinkFlowers
Subscribe Daisy to the full content of NewsLetter whenever it has changed
* daisy@flowers.com: TWiki.NewsLetter?
Subscribe buttercup to NewsLetter and its immediate children, even if it hasn't changed.
* buttercup@flowers.com: TWiki.NewsLetter! (1)
Subscribe GardenGroup (which includes Petunia) to all changed topics under AllnewsLetters to a depth of 3. Then unsubscribe Petunia from the ManureNewsLetter, which she would normally get as a member of GardenGroup? :
A user may be listed many times in the WebNotify topic. Where a user has several lines in WebNotify that all match the same topic, they will only be notified about changes that topic once (though they will still receive individual mails for news topics).
If a TWiki group is listed for notification, the group will be recursively expanded to the e-mail addresses of all members.
Tip: List names in alphabetical order to make it easier to find the names.
Note for System Administrators: Notification is supported by an add-on to the TWiki kernel called the MailerContrib. See the MailerContrib topic for details of how to set up this service.
Note: If you prefer a news feed, point your reader to WebRss (for RSS 1.0 feeds) or WebAtom (for ATOM 1.0 feeds). Learn more at WebRssBase and WebAtomBase, respectively.
These settings override the defaults for this web only. See full list of defaults with explanation. Many of the settings below are commented out. Remove the # sign to enable a local customisation.
Web-specific background color: (Pick a lighter one of the StandardColors).
Set WEBBGCOLOR = #D0D0D0
Note: This setting is automatically configured when you create a web
Image, URL and alternate tooltip text of web's logo. Note: Don't add your own local logos to the TWikiLogos topic; create your own logos topic instead.
List this web in the SiteMap. If you want the web listed, then set SITEMAPLIST to on, do not set NOSEARCHALL, and add the "what" and "use to..." description for the site map. Use links that include the name of the web, i.e. Education/LC.Topic links. Note: Unlike other variables, the setting of SITEMAPLIST is not inherited from parent webs. It has to be set in every web that is to be listed in the SiteMap
Set SITEMAPLIST = on
Set SITEMAPWHAT =
Set SITEMAPUSETO = Licenciatura em Ciências da Computação - 2º ano
Note: Above settings are automatically configured when you create a web
Exclude web from a web="all" search: (Set to on for hidden webs).
#Set NOSEARCHALL = on
Note: This setting is automatically configured when you create a web
Prevent automatic linking of WikiWords and acronyms (if set to on); link WikiWords (if empty); can be overwritten by web preferences:
#Set NOAUTOLINK =
Note: You can still use the [[...][...]] syntax to link topics if you disabled WikiWord linking. The <noautolink> ... </noautolink> syntax can be used to prevents links within a block of text.
Default template for new topics for this web:
WebTopicEditTemplate? : Default template for new topics in this web. (Site-level is used if topic does not exist)
Comma separated list of forms that can be attached to topics in this web. See TWikiForms for more information.
Set WEBFORMS =
Users or groups who are not / are allowed to view / change / rename topics in the Education/LC web: (See TWikiAccessControl). Remove the # to enable any of these settings. Remember that an empty setting is a valid setting; setting DENYWEBVIEW to nothing means that anyone can view the web.
Preferences are used as TWikiVariables by enclosing the name in percent signs. Example:
When you write variable %WEBBGCOLOR% , it gets expanded to #D0D0D0
The sequential order of the preference settings is significant. Define preferences that use other preferences first, i.e. set WEBCOPYRIGHT before WIKIWEBMASTER since %WEBCOPYRIGHT% uses the %WIKIWEBMASTER% variable.
You can introduce your own preferences variables and use them in your topics and templates.
TWiki search results for \.*
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC
The Education/LC web of TWiki. TWiki is a Web-Based Collaboration Platform for the Enterprise.en-usCopyright 2020 by contributing authorsTWiki Administrator [webmaster@di.uminho.pt]The contributing authors of TWikiTWikiDIUM.Education/LC
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC
/twiki/pub/Main/LocalLogos/um_eengP.jpgWebHome
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/WebHome
Esta disciplina tem por objectivo aprofundar a relação existente entre lógica formal e a computação. Esta relação pode assumir diferentes formas, dependendo da perspectiva ... (last changed by OlgaPacheco)2010-02-18T13:06:08ZOlgaPachecoMaterialApoio
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/MaterialApoio
Slides Lógica Proposicional I Cálculo de Sequentes (versão: 11/06/2008) Lógica Proposicional II Método Tableaux , Formas Clausais, Resolução (versão: 11 ... (last changed by OlgaPacheco)2010-02-18T13:00:50ZOlgaPachecoAvisos0809
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Avisos0809
22/07/2009: Disponíveis notas da época de recurso. 07/05/2009: Disponível enunciado do projecto prático. 06/03/2009: Já disponível o guião da primeira aula pr ... (last changed by JoseBacelarAlmeida)2009-07-22T17:28:03ZJoseBacelarAlmeida0809
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/0809
Lógica Computacional (8504N2) em Matemática e Ciências de Computação 2º Ano 2º Semestre Ano lectivo 2008/2009 Equipa Docente José Carlos Bacelar ... (last changed by JoseBacelarAlmeida)2009-07-22T17:27:12ZJoseBacelarAlmeidaProgDetalhado0809
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/ProgDetalhado0809
Programa detalhado do ano lectivo 2008/2009 Lógica Proposicional Sintaxe e Semântica Sistemas Dedutivos Dedução Natural ... (last changed by JoseBacelarAlmeida)2009-06-18T22:10:46ZJoseBacelarAlmeidaPrograma0809
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Programa0809
Programa Resumido Componente Teórica Lógica Proposicional Sintaxe e Semântica Sistemas Dedutivos Métodos de Verificação Aspectos ... (last changed by JoseBacelarAlmeida)2009-06-18T22:10:01ZJoseBacelarAlmeidaPraticas0809
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Praticas0809
Aulas Práticas #Aula10P Aula 10: Predicados de Segunda Ordem e outros predicados primitivos disponibilizados pelo Prolog Predicados de segunda ordem Existem meta ... (last changed by JoseBacelarAlmeida)2009-05-29T23:07:19ZJoseBacelarAlmeidaProjectos0809
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Projectos0809
Projecto O objectivo deste projecto é o de explorar o demonstrador de teoremas COQ para realizar provas simples. Sugere se que os interessados realizem os exemplos ... (last changed by JoseBacelarAlmeida)2009-05-08T02:24:38ZJoseBacelarAlmeidaTopicos0809
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Topicos0809
Calendário (last changed by JoseBacelarAlmeida)2009-02-12T17:21:40ZJoseBacelarAlmeidaCalendario
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Calendario
(last changed by JoseBacelarAlmeida)2009-02-12T17:16:45ZJoseBacelarAlmeidaSumarios0708
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Sumarios0708
Sumários Aulas Teóricas (3ª 14:00 15:00; 5ª 16:00 17:00) 26/02: Não houve aula. 28/02: Não houve aula. 04/03: Aula de substituição em 27/03 , às 15:00. 06 ... (last changed by JoseBacelarAlmeida)2009-02-01T18:25:15ZJoseBacelarAlmeidaSumarios0809
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Sumarios0809
Sumários Aulas Teóricas (3ª 14:00 15:00; 5ª 16:00 17:00) TP1 Aulas Teórico Práticas (2ª 16:00 17:00) Aulas Práticas (2ª 17:00 19:00) TP2 Aulas Teórico Pr ... (last changed by JoseBacelarAlmeida)2009-02-01T18:23:00ZJoseBacelarAlmeida0708
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/0708
Lógica Computacional (8504N2) em Matemática e Ciências de Computação 2º Ano 2º Semestre Ano lectivo 2007/2008 Equipa Docente José Carlos Bacelar ... (last changed by JoseBacelarAlmeida)2009-02-01T18:16:25ZJoseBacelarAlmeidaWebPreferences
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/WebPreferences
Education/LC Web Preferences The following settings are web preferences of the Education/LC web. These preferences overwrite the site level preferences in ... (last changed by JoseBacelarAlmeida)2009-02-01T18:15:29ZJoseBacelarAlmeidaMFES0809
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/MFES0809
Análise, Modelação e Teste de Software MFES Mestrado de Informática 13/11/2008 "Design by Contract and Java Modeling Language": apresentação do conceito e clausulas ... (last changed by JoseBacelarAlmeida)2008-12-05T23:17:24ZJoseBacelarAlmeidaAvisos0708
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Avisos0708
24/09: Já estão disponíveis as notas da época de especial. 28/07: Já estão disponíveis as notas da época de recurso. 02/07: Já estão disponíveis as notas do 2 ... (last changed by JoseBacelarAlmeida)2008-09-27T11:17:47ZJoseBacelarAlmeida
A avaliação da disciplina é realizada por exame final, sendo que a realização de fichas práticas ao longo do semestre permite a dispensa de parte desse exame (30%).
Temos então duas modalidades de avaliação:
Modalidade A: exame final com peso 70% e avaliação prática com peso 30% (ambas com nota mínima de 9 valores)
Modalidade B: exame final com peso 100%.
As melhorias de nota serão sempre realizadas na modalidade B.
Classificações finais superiores a 16 devem ainda contar com a realização de um pequeno projecto prático, cuja avaliação será incorporada na nota final com um peso de 20%.
Durante o período lectivo far-se-ão dois testes: um sensivelmente a meio do semestre e outro no final. Ambos os testes incluem uma componente teórica e outra prática (Prolog). O peso relativo de cada uma dessas componentes será aproximadamente 70 e 30%.
Opcionalmente, os alunos podem ainda realizar um pequeno projecto prático, cuja avaliação será incorporada na nota final com um peso de 20%. Nas notas finais superiores a 16 valores esta componente será sempre considerada (querendo dizer que a nota é majorada a 16 valores se não se realizar o dito projecto).
A avaliação da disciplina consiste nas seguintes componentes:
Realização de uma prova individual escrita com nota mínima de 8 valores (90%)
Participação nas aulas (teórico-)práticas (10%)
Opcionalmente, os alunos podem ainda realizar um pequeno projecto prático, cuja avaliação será incorporada na nota final com um peso de 20%. Nas notas finais superiores a 16 valores esta componente será sempre considerada (querendo dizer que a nota é majorada a 16 valores se não se realizar o dito projecto).
Sumários
Os sumários da disciplina estão disponíveis no calendário.
Aulas Práticas
Os guiões das aulas práticas estão disponíveis aqui.
Proof Theory and Automated Deduction. Jean Goubault-Larrecq & Ian Mackie , Kluwer Academic Publishers, 1997.
First Order Logic and Automated Theorem Proving. Melvin Fitting, Graduate Texts in Computer Science. Springer-Verlag, 1996.
Critérios de Avaliação
A avaliação tem uma componente teórica e uma componente prática, ambas
obrigatórias. A nota final será calculada com base na seguinte
fórmula:
Nota Final = NT * 0.7 + NP * 0.3
sendo
NT a nota teórica (nota mínima de 9 valores), obtida através da realização de uma prova individual escrita;
NP a nota prática (nota mínima de 9 valores), resultante da avaliação de um trabalho prático (realizado em grupos de 3 alunos) e da avaliação contínua realizada ao longo das aulas laboratoriais e que terá por base a resolução de fichas de trabalho;
Quem desejar realizar um projecto prático no âmbito desta disciplina deve contactar um dos docentes. O objectivo desse contacto é o de obter informação/apontadores adicionais sobre os vários projectos e decidir o projecto concreto a ser realizado.
Algumas ideias para projectos práticos:
Animador de uma pequena linguagem funcional com tipos.
Codificação da máquina abstracta de Krivine em C .
Estudo sobre o impacto da operação de substituição na avaliação de lambda-termos .
Inferência/verificação de tipos numa linguagem point-free .
"Design by Contract and Java Modeling Language": apresentação do conceito e clausulas básicas do JML (requires, ensures, invariant).
Universo de ferramentas para JML. Características do ESC/Java2 e da verificação de asserções em tempo de execução (jmlc/jmlrac).
Teórico-prática: exercício de utilização do plugin Eclipse do ESC/Java2 (análise estática simples).
20/11/2008
"JML - beyond the basics": especificação de casos multiplos e de comportamento excepcional; invariantes de ciclo; frame-confitions; dificuldades com aliasing de referências.
Teórico-prática: exercício de modelação em JML.
27/11/2008
"Abstract modeling in JML": herança de especificações; datagroups e abstracção; campos "ghost" e "model"; tipos abstractos para modelação.
Teórica-prática: acompanhamento do projecto JML.
04/12/2008
"Unit Testing and JmlUnit": objectivos e características dos testes unitários; utilização do JUnit; integração com verificação de asserções JML e ferramenta JML-Unit.
Existem meta-predicados que permitem coleccionar todas as soluções para um dado
objectivo de prova (ver User's Manual ou o help).
findall(?Template,:Goal,?Bag) : Bag é a lista de instâncias de Template encontradas nas provas de Goal. A ordem da lista corresponde à ordem em que são encontradas as respostas. Se não existirem instanciações para Template, Bag unifica com a lista vazia.
bagof(?Template,:Goal,?Bag) : Semelhante a findall, mas se Goal falhar, bagof falha.
setof(?Template,:Goal,?Set) : Semelhante a bagof, mas a lista é ordenada e sem repetições.
Exemplo:
| ?- findall(X, member(X,[1,2,3]), L).
L = [1,2,3]
yes
Utilize o predicado findall para determinar todas as soluções para o problema das N rainhas com N=8.
Aula 7: Estratégia Gerar e Testar.
Estratégia Gerar e Testar
O mecanismo de backtracking do PROLOG torna possível codificar, de forma directa, a estratégia de gerar e testar para encontrar a solução de um determinado problema. Segundo esta estratégia, o problema é decomposto em duas fases:
Gera-se "soluções cadidatas" para o problema.
Verifica-se se a "solução candidata" satisfaz os requisitos do problema (e é, portanto, uma "solução efectiva").
Podemos assim identificar o padrão com a seguinte regra PROLOG:
resolve(X) :- gera(X), testa(X).
Note-se o papel preponderante do backtracking para encontrar uma dada solução para resolve(X): o predicado gera(X) instancia X com uma possível solução. No caso de testa(X) falhar (a solução proposta não satisfaz os requisitos impostos pelo problema), o mecanismo de backtracking permite que gera(X) instancie uma nova alternativa, até que se encontre a solução pretendida.
O predicado gera acaba normalmente por se revelar o ponto crítico na aplicação desta estratégia: por um lado, pretende-se que ele cubra todas as possíveis soluções para o problema (caso contrário, podemos nunca gerar a solução requerida). Por outro, e por questões de eficiência, vamos pretender que ele produza o mínimo de soluções erradas (para minimizar o espaço de busca) -- na prática, este esforço de minimização traduz-se por eliminar candidatos notoriamente errados e por encontrar codificações apropriadas para as possíveis soluções.
Vejamos um exemplo concreto: pretende-se encontrar um divisor para um dado número N (diferente de 1 e N).
fromToL(L,U,[]) :- U < L, !.
fromToL(L,U,[L|X]) :- L1 is L+1, fromToL(L1,U,X).
gera(N,X) :- fromToL(2,N-1,L), member(X,L).
testa(N,X) :- N mod X =:= 0.
divisor(N,X) :- gera(N,X), testa(N,X).
Mas o programa apresentado pode ser consideravelmente optimizado se observarmos que nos é suficiente encontrar um divisor entre 2 e sqrt(N) (se X>sqrt(N) é um divisor de N, então também será N/X<sqrt(N)). Dessa forma teríamos:
divisor2(N,X) :- fromtoL(2,sqrt(N),L), member(X,L), N mod X =:= 0.
Verifique ambos os programas para um número primo elevado (e.g. 209953, 331777, 472393, ...)
Utilize a estratégia generate & test para determinar a raiz de um natural, definida da seguinte forma: um número natural X é a raiz de N quando X2<=N e (X+1)2>N
Problema das N rainhas.
Um exemplo clássico de programação em PROLOG consiste em escrever um predicado que permita resolver o problema das n rainhas. Esse problema consiste em dispor n rainas num tabuleiro de damas com dimensão n*n, sem que qualquer rainha se encontre ameaçada por outra. Como um exemplo de uma solução temos (num tabuleiro 4*4):
Q
Q
Q
Q
Note que cada linha e cada coluna deve conter uma, e só uma, rainha (porquê?).
Dito isto, verificamos que uma forma expedita de representar as soluções para este problema consiste em utilizar uma lista que informe qual a coluna em que é colocada a rainha de cada uma das linhas (a solução do exemplo seria [3,1,4,2], querendo dizer que a rainha da primeira linha aparece na terceira coluna, a da segunda linha na primeira coluna, etc.) -- desta forma, aparece uma rainha em cada linha "por construção". A restrição de aparecer uma única rainha por cada coluna é traduzida por deverem aparecer na lista todos os números de 1 a 4, ou seja, a lista deve ser uma permutação de [1,2,3,4]. Temos assim resolvido o sub-problema de gerar soluções candidatas: são simplesmente permutações da lista [1..N].
Na fase de teste, falta unicamente verificar que nenhuma rainha está no alcance da diagonal de uma outra. Para isso notamos que:
Duas rainhas estão numa diagonal / sse a soma da linha e coluna da posição de cada uma delas for igual;
Duas rainhas estão numa diagonal \ sse a diferença da linha e coluna da posição de cada uma delas for igual.
Com base no que foi referido, codifique um predicado nrainhas(+N,?X) que determine uma solução para o problema das N-rainhas.
Aula 6: Manipulação de fórmulas lógicas proposicionais em Prolog.
Definição de Operadores em Prolog.
O Prolog permite definir operadores prefixos, sufixos ou infixos. Para tal devemos utilizar o predicado pré-definido op(_Prec_,=_Type_,=_Name_=)=. O argumento Name é o nome do operador definido; Prec é um número entre 0 e 1200 que determinará a sua precedência e Type determina o seu tipo e associatividade. Por exemplo, o operador de soma binário + está definido como op(700, yfx, +). A precedência 700 irá determinar que tenha menos precedência do que a multiplicação (definida com precedência 500 - note que um número menor indica maior precedência do operador), e o tipo yfx caracteriza o operador como infixo e associativo à esquerda. Outras possibilidades para o tipo dos operadores são: xfy, xfx para operadores infixos associativos à direita e sem associatividade; fx, fy para operadores prefixos e xf, yf para operadores sufixos.
Alguns dos operadores pré-definidos do Prolog são:
Faça um pequeno predicado que lhe permita confirmar a maior precedência do operador * face ao operador +.
Manipulação de fórmulas lógicas proposicionais em Prolog.
A definição de operadores permite que a sintaxe do Prolog se aproxime do domínio onde se está a trabalhar. Considere que se pretendem representar fórmulas da Lógica Proposicional em Prolog. Em vez de considerar termos como or(not(p), and( and(p, r), not(q))), podemos utilizar operadores que nos permitam aproximar a sua representação da utilizada habitualmente. Assim definimos:
Estamos a utilizar os operadores de conjunção e disjunção do Prolog (se preferir, pode definir os operadores /\ e \/). Assim, a fórmula apresentada atrás pode ser escrita como (~p ; p , r, ~q) (note o papel da precedência e associatividade).
Defina um predicado que, dado uma fórmula proposicional, determine a Forma Normal Negativa (FNN).
Pretende-se definir um programa que permita verificar se uma dada fórmula é uma contradição pelo método de Davis Putnam. Para o efeito, considere os seguintes predicatos que convertem uma FNN na respectiva Forma Normal Conjuntiva (FNC), e que colocam esta última na sua forma matricial (como uma lista de listas) :
% -----------------------------------------------------------------
% fnc(+NNF,?FNC)
%
% NNF é uma forma normal negatiiva e FNC a respectiva forma normal conjuntiva
cnf(((A,B);C), (F1,F2)) :- !, cnf((A;C),F1), cnf((B;C),F2).
cnf((A;(B,C)), (F1,F2)) :- !, cnf((A;B),F1), cnf((A;C),F2).
cnf((A;B), F) :- !, cnf(A, A1), cnf(B, B1),
(/*IF*/ (A1=(C,D); B1=(C,D)) ->
/*THEN*/ cnf((A1;B1), F) ;
/*ELSE*/ F=(A1;B1) ).
cnf((A,B), (A1,B1)) :- !, cnf(A, A1), cnf(B, B1).
cnf(Lit, Lit).
% -----------------------------------------------------------------
% matCNF(+FNC,?MAT)
%
% FNC é uma forma normal conjuntiva e MAT é a sua representação sob a forma
% de matriz (lista de listas de literais).
matCNF((A,B),M) :- !, matCNF(A,MA), matCNF(B,MB), append(MA,MB,M).
matCNF((A;B),C) :- !, matCNF(A,[CA]), matCNF(B,[CB]), union2(CA,CB,C).
matCNF(~Lit, [[TWiki.-Lit][-Lit]]) :- !.
matCNF(Lit, [[TWiki.Lit][Lit]]).
union2([],L,[L]).
union2([X|L1],L2,L3) :- member2(X,L2), !, union2(L1,L2,L3).
union2([X|_],L2,[]) :- (-Xn=X;-X=Xn), member2(Xn,L2), !.
union2([X|L1],L2,L3) :- union2(L1,[X|L2],L3).
member2(X,[Y|_]) :- X==Y, !.
member2(X,[_|T]) :- member2(X,T).
Aula 5: Utilização de cut e negação por falha.
O predicado pré-definido cut (!) permite eliminar ramos nas árvores de derivação de predicados Prolog. Operacionalmente, o cut pode ser caracterizado da seguinte forma: _"Durante o processo de prova, a 1a passagem pelo cut é sempre
verdadeira (com sucesso). Se por backtracking se voltar ao cut,
então o cut faz falhar o predicado que está na cabeça da regra."_
A utilização do cut está normalmente associada a questões de eficiência: os ramos da árvore que são eliminados acabariam eventualmente por falhar, e assim poupamos trabalho ao motor de inferência do Prolog. Esta utilização do cut é considerada benigna, porque não se afecta o significado dos predicados. Tomemos como exemplo um predicado que verifique se o terceiro argumento é o mínimo dos dois primeiros. Podería ser definido como:
minimo(X,Y,Y) :- X >= Y.
minimo(X,Y,X) :- X < Y.
Mas podemos facilmente observar que, uma vez verificado que X>=Y, não faz sentido tentar verificar que X<Y. Assim sendo, faz sentido colocar um cut no final da primeira cláusula:
minimo(X,Y,Y) :- X >= Y, !.
minimo(X,Y,X) :- X < Y.
Estaria correcto eliminar também o predicado X<Y na segunda cláusula? Justifique com exemplos apropriados.
É importante referir que certas utilizações do cut alteram propositadamente o comportamento do programa (tipicamente para impedir que a execução do programa entre em ciclo). Essas utilizações são normalmente consideradas "mais perigosas" porque obriga a que o programador detenha uma ideia muito precisa sobre o processo de construção da derivação por parte do Prolog.
Relembre as seguintes alternativas para calcular o multiplicação de naturais:
a(zero, Y, Y).
a(suc(X), Y, suc(Z)) :- a(X,Y,Z).
m1(zero, _, zero).
m1(suc(X), Y, Z) :- a(Y, W, Z), m1(X,Y,W).
m2(zero, _, zero).
m2(suc(X), Y, Z) :- m2(X,Y,W), a(Y, W, Z).
Seria possível impedir a computação infinita de m2 por intermédio da introdução de cuts?
A introdução de cuts também faria sentido para m1? Onde? Justifique.
Considere o seguinte programa que pretende inserir o primeiro argumento (um número) na lista ordenada passada no segundo argumento.
Mostre, avaliando um objectivo apropriado, que o programa está incorrecto.
Como o poderá corrigir?
Negação por falha.
Por vezes pretende-se garantir que um dado predicado não é válido. A utilização do cut (em conjunção com o predicado pré-definido fail que falha sempre) permite codificar uma forma restrita de negação: a "negação por falha". Considere o seguinte predicado:
neg(X) :- X, !, fail.
neg(X).
Note que neg(X) falha sempre que o Prolog consiga construir uma derivação para X. Por outro lado, sucede se falhar na construção dessa derivação (entra na segunda cláusula, que é trivialmente satisfeita). Obs.: o predicado pré-definido do Prolog \+ corresponde ao predicado neg apresentado.
Verifique o resultado de neg em predicados já definidos.
Como explica a resposta às questões estudante_solteiro(paulo) e estudante_solteiro(X)
Aula 4: Árvores de Prova. Tipos algébricos
Árvores de Prova em Prolog
Operacionalmente, o Prolog segue uma estratégia top down, depth-first para encontrar soluções das questões colocadas. O processo de Unificação permite concretizar as questões colocadas definindo as condições em que a questão inicial é satisfeita (a substituição obtida). Quando o motor de inferência se depara com uma situação de "falha", retrocede na árvore de prova por forma a tentar novas alternativas.
Relembre o predicado member que verifica se um elemento pertence a uma lista. Construa a árvore de procura de soluções para a questão member(X,[1,2,3]).
Considere agora o predicado takeout/3 referido na última aula. Construa a árvore de procura de soluções para a questão takeout(X,[1,2,3],Y).
Tipos algébricos em Prolog
A utilização de termos permite a manipulação em Prolog de valores de tipos algébricos (que em Haskell seriam declarados com data). Por exemplo, árvores binárias podem ser representadas por termos como vazia, nodo(vazia, vazia), etc.
Defina um predicado que verifique se uma lista é uma travessia in-order de uma árvore.
Defina predicados que determinem:
uma árvore é uma Árvore Binária de Procura
uma lista está ordenada.
Note no entanto que em Prolog não existe a noção de tipo. De facto nada nos impede de considerar termos como vazia(nodo,vazia(nodo)).
Aula 3: Continuação da manipulação de listas
Defina last/2 que verifique se o último elemento de uma lista é um dado.
Defina append/3 que concatene duas listas.
Utilize o predicado append para definir os predicados prefixo e sufixo que verificam se uma lista é prefixo ou sufixo doutra.
Defina split/4 que separe os elementos de uma lista nos menores e maiores que um dado valor.
Utilize o predicado takeout para definir um predicado que determine se uma lista é permutação de uma outra.
Aula 2: Utilização de termos, introdução à manipulação de Listas.
Termos Estruturados
Para além dos tipos primitivos, o Prolog admite termos estruturados da forma f(t1,t2,...,tn), onde f é o functor do termo e t1,...tn são sub-termos.
Uma aplicação típica de termos estruturados é para organizar a informação contida num programa. Por exemplo, podemos armazenar datas com termos da forma "data(25,abril,2007)". O seguinte predicado extrai o dia duma data armazenada dessa forma:
diaData(D,data(D,_,_)).
Defina o predicado valData/1 que verifique se uma data é correcta.
Nada nos impede de considerarmos termos arbitrariamente complicados. Em particular, podemos considerar termos de natureza recursiva como a representação dos naturais com os construtores zero e suc (i.e. zero, suc(zero), suc(suc(zero)), etc.).
Defina o predicado nat/1 que verifique se um termo é um natural na representação referida.
Defina soma/3 que verifique se o terceiro argumento é a soma dos dois primeiros.
Mostre como usar o predicado soma/3 para calcular a subtração de dois naturais.
Defina predicados int2nat/2 e nat2int/2 que convertam naturais em inteiros e vice-versa.
Introdução às Listas em Prolog
Um exemplo de um tipo estruturado que está pré-definido no Prolog são as listas. A sintaxe mais prática é [] que denota a lista vazia e [H|T] que denota a lista com cabeça H e cauda T.
Defina member/2 que verifica se um elemento pertence a uma lista.
Utilize o predicado member para determinar quais dos elementos da lista [3,5,4,6,5,7] são pares.
Aula 9: Implementação do algoritmo Davis-Putnam em Prolog.
Pretende-se definir um programa que permita verificar se uma dada fórmula é uma contradição pelo método de Davis Putnam. Para o efeito, considere os seguintes predicatos que convertem uma FNN na respectiva Forma Normal Conjuntiva (FNC), e que colocam esta última na sua forma matricial (como uma lista de listas) :
% -----------------------------------------------------------------
% fnc(+NNF,?FNC)
%
% NNF é uma forma normal negatiiva e FNC a respectiva forma normal conjuntiva
cnf(((A /\ B) \/ C), (F1 /\ F2)) :- !, cnf((A \/ C),F1), cnf((B \/ C),F2).
cnf((A \/ (B /\ C)), (F1,F2)) :- !, cnf((A \/ B),F1), cnf((A \/ C),F2).
cnf((A \/ B), F) :- !, cnf(A, A1), cnf(B, B1),
(/*IF*/ (A1=(C /\ D); B1=(C /\ D)) ->
/*THEN*/ cnf((A1 \/ B1), F) ;
/*ELSE*/ F=(A1 \/ B1) ).
cnf((A /\ B), (A1 /\ B1)) :- !, cnf(A, A1), cnf(B, B1).
cnf(Lit, Lit).
% -----------------------------------------------------------------
% matCNF(+FNC,?MAT)
%
% FNC é uma forma normal conjuntiva e MAT é a sua representação sob a forma
% de matriz (lista de listas de literais).
matCNF((A /\ B),M) :- !, matCNF(A,MA), matCNF(B,MB), append(MA,MB,M).
matCNF((A \/ B),C) :- !, matCNF(A,[CA]), matCNF(B,[CB]), union2(CA,CB,C).
matCNF(~Lit, [[TWiki.-Lit][-Lit]]) :- !.
matCNF(Lit, [[TWiki.Lit][Lit]]).
union2([],L,[L]).
union2([X|L1],L2,L3) :- member2(X,L2), !, union2(L1,L2,L3).
union2([X|_],L2,[]) :- (-Xn=X;-X=Xn), member2(Xn,L2), !.
union2([X|L1],L2,L3) :- union2(L1,[X|L2],L3).
member2(X,[Y|_]) :- X==Y, !.
member2(X,[_|T]) :- member2(X,T).
Exercícios:
Defina um predicado que determine a forma normal disjuntiva.
Defina o predicado de split/3 que determine o particionamento de uma FN.
Defina o predicado davisPutnam/1 que verifique se uma fórmula proposicional é inconsistente.
Aula 8: Manipulação de fórmulas de lógica proposicional em Prolog.
Definição de Operadores em Prolog.
O Prolog permite definir operadores prefixos, sufixos ou infixos. Para tal devemos utilizar o predicado pré-definido op(Prec,Type,Name). O argumento Name é o nome do operador definido; Prec é um número entre 0 e 1200 que determinará a sua precedência e Type determina o seu tipo e associatividade. Por exemplo, o operador de soma binário + está definido como op(700, yfx, +). A precedência 700 irá determinar que tenha menos precedência do que a multiplicação (definida com precedência 500 - note que um número menor indica maior precedência do operador), e o tipo yfx caracteriza o operador como infixo e associativo à esquerda. Outras possibilidades para o tipo dos operadores são: xfy, xfx para operadores infixos associativos à direita e sem associatividade; fx, fy para operadores prefixos e xf, yf para operadores sufixos.
Alguns dos operadores pré-definidos do Prolog são:
Faça um pequeno predicado que lhe permita confirmar a maior precedência do operador * face ao operador +.
Manipulação de fórmulas de lógica proposicional em Prolog.
A definição de operadores permite que a sintaxe do Prolog se aproxime do domínio onde se está a trabalhar. Considere que se pretendem representar fórmulas da Lógica Proposicional em Prolog. Em vez de considerar termos como or(not(p), and( and(p, r), not(q))), podemos utilizar operadores que nos permitam aproximar a sua representação da utilizada habitualmente. Assim definimos:
que denotam os operadores de implicação, disjunção, conjunção e negação. Assim, a fórmula apresentada atrás pode ser escrita como (~p \/ p /\ r /\ ~q) (note o papel da precedência e associatividade).
Exercícios:
Defina o predicado props(+Form,-Props) que calcule o conjunto de símbolos de proposições utilizados na fórmula dada.
Defina o predicado val(+Form,+Mod) que verifique se a fórmula é válida no modelo passado como argumento.
Como poderia reformular a definição do predicado val por forma a que não seja necessário instanciar o modelo (ou seja, construir o predicado valM(+Form, ?Mod).
Defina o predicado nnf(+Form, -NNF) que determine a forma normal negativa de uma fórmula.
Aula 7: Predicados de Segunda Ordem e outros predicados primitivos disponibilizados pelo Prolog
Predicados de segunda ordem
Existem meta-predicados que permitem coleccionar todas as soluções para um dado
objectivo de prova (ver User's Manual ou o help).
findall(?Template,:Goal,?Bag) : Bag é a lista de instâncias de Template encontradas nas provas de Goal. A ordem da lista corresponde à ordem em que são encontradas as respostas. Se não existirem instanciações para Template, Bag unifica com a lista vazia.
bagof(?Template,:Goal,?Bag) : Semelhante a findall, mas se Goal falhar, bagof falha.
setof(?Template,:Goal,?Set) : Semelhante a bagof, mas a lista é ordenada e sem repetições.
Exemplo:
| ?- findall(X, member(X,[1,2,3]), L).
L = [1,2,3]
yes
Relacionados com os apresentados, encontramos outros predicados de ordem superior, como o bem conhecido map (do haskell). No Prolog o predicado maplist implementa a funcionalidade análoga.
Exercícios:
Teste os predicados apresentados codificando exemplos apropriados.
Utilize o predicado findall para determinar todas as soluções para o problema das N rainhas com N=8.
Outras características do Prolog
Manipulação da base de conhecimento: O Prolog permite manipular dinamicamente a base de conhecimento (inserir ou remover factos ou regras). Para isso disponibiliza os predicados assert, retract, rectractall (e variantes...).
Input/Output: tal como qualquer linguagem com o mínimo de preocupações práticas, é possível realizar operações de Input/Output. Para o efeito dispõe-se dos predicados write, read (entre outros, e com muitas variantes...); open e close para maniputação de ficheiros, etc...
Exercícios:
Consulte a documentação relativa aos predicados referidos e teste cada um deles com exemplos apropriados.
Extenda o programa das N rainhas com um predicado runQueens que interrogue o utilizador sobre o número de rainhas a considerar e imprima no écran todas as soluções admissíveis.
Aula 6: Estratégia Gerar e Testar.
Estratégia Gerar e Testar
O mecanismo de backtracking do PROLOG torna possível codificar, de forma directa, a estratégia de gerar e testar para encontrar a solução de um determinado problema. Segundo esta estratégia, o problema é decomposto em duas fases:
Gera-se "soluções cadidatas" para o problema.
Verifica-se se a "solução candidata" satisfaz os requisitos do problema (e é, portanto, uma "solução efectiva").
Podemos assim identificar o padrão com a seguinte regra PROLOG:
resolve(X) :- gera(X), testa(X).
Note-se o papel preponderante do backtracking para encontrar uma dada solução para resolve(X): o predicado gera(X) instancia X com uma possível solução. No caso de testa(X) falhar (a solução proposta não satisfaz os requisitos impostos pelo problema), o mecanismo de backtracking permite que gera(X) instancie uma nova alternativa, até que se encontre a solução pretendida.
O predicado gera acaba normalmente por se revelar o ponto crítico na aplicação desta estratégia: por um lado, pretende-se que ele cubra todas as possíveis soluções para o problema (caso contrário, podemos nunca gerar a solução requerida). Por outro, e por questões de eficiência, vamos pretender que ele produza o mínimo de soluções erradas (para minimizar o espaço de busca) -- na prática, este esforço de minimização traduz-se por eliminar candidatos notoriamente errados e por encontrar codificações apropriadas para as possíveis soluções.
Vejamos um exemplo concreto: pretende-se encontrar um divisor para um dado número N (diferente de 1 e N).
fromToL(L,U,[]) :- U < L, !.
fromToL(L,U,[L|X]) :- L1 is L+1, fromToL(L1,U,X).
gera(N,X) :- fromToL(2,N-1,L), member(X,L).
testa(N,X) :- N mod X =:= 0.
divisor(N,X) :- gera(N,X), testa(N,X).
Mas o programa apresentado pode ser consideravelmente optimizado se observarmos que nos é suficiente encontrar um divisor entre 2 e sqrt(N) (se X>sqrt(N) é um divisor de N, então também será N/X<sqrt(N)). Dessa forma teríamos:
divisor2(N,X) :- fromtoL(2,sqrt(N),L), member(X,L), N mod X =:= 0.
Verifique ambos os programas para um número primo elevado (e.g. 209953, 331777, 472393, ...)
Utilize a estratégia generate & test para determinar a raiz de um natural, definida da seguinte forma: um número natural X é a raiz de N quando X2<=N e (X+1)2>N
Problema das N rainhas.
Um exemplo clássico de programação em PROLOG consiste em escrever um predicado que permita resolver o problema das n rainhas. Esse problema consiste em dispor n rainas num tabuleiro de damas com dimensão n*n, sem que qualquer rainha se encontre ameaçada por outra. Como um exemplo de uma solução temos (num tabuleiro 4*4):
Q
Q
Q
Q
Note que cada linha e cada coluna deve conter uma, e só uma, rainha (porquê?).
Dito isto, verificamos que uma forma expedita de representar as soluções para este problema consiste em utilizar uma lista que informe qual a coluna em que é colocada a rainha de cada uma das linhas (a solução do exemplo seria [3,1,4,2], querendo dizer que a rainha da primeira linha aparece na terceira coluna, a da segunda linha na primeira coluna, etc.) -- desta forma, aparece uma rainha em cada linha "por construção". A restrição de aparecer uma única rainha por cada coluna é traduzida por deverem aparecer na lista todos os números de 1 a 4, ou seja, a lista deve ser uma permutação de [1,2,3,4]. Temos assim resolvido o sub-problema de gerar soluções candidatas: são simplesmente permutações da lista [1..N].
Na fase de teste, falta unicamente verificar que nenhuma rainha está no alcance da diagonal de uma outra. Para isso notamos que:
Duas rainhas estão numa diagonal / sse a soma da linha e coluna da posição de cada uma delas for igual;
Duas rainhas estão numa diagonal \ sse a diferença da linha e coluna da posição de cada uma delas for igual.
Com base no que foi referido, codifique um predicado nrainhas(+N,?X) que determine uma solução para o problema das N-rainhas.
Aula 5: Utilização de cut e negação por falha.
O predicado pré-definido cut (!) permite eliminar ramos nas árvores de derivação de predicados Prolog. Operacionalmente, o cut pode ser caracterizado da seguinte forma: _Durante o processo de prova, a 1a passagem pelo cut é sempre
verdadeira (com sucesso). Se por backtracking se voltar ao cut,
então o cut faz falhar o predicado que está na cabeça da regra._
A utilização do cut está normalmente associada a questões de eficiência: os ramos da árvore que são eliminados acabariam eventualmente por falhar, e assim poupamos trabalho ao motor de inferência do Prolog. Esta utilização do cut é considerada benigna (green cut), porque não se afecta o significado dos predicados. Tomemos como exemplo um predicado que verifique se o terceiro argumento é o mínimo dos dois primeiros. Podería ser definido como:
minimo(X,Y,Y) :- X >= Y.
minimo(X,Y,X) :- X < Y.
Mas podemos facilmente observar que, uma vez verificado que X>=Y, não faz sentido tentar verificar que X<Y. Assim sendo, faz sentido colocar um cut no final da primeira cláusula:
minimo(X,Y,Y) :- X >= Y, !.
minimo(X,Y,X) :- X < Y.
Estaria correcto eliminar também o predicado X<Y na segunda cláusula? Justifique com exemplos apropriados.
É importante referir que certas utilizações do cut alteram propositadamente o comportamento do programa (tipicamente para impedir que a execução do programa entre em ciclo). Essas utilizações são normalmente consideradas "mais perigosas" (red cuts) porque obrigam a que o programador detenha uma ideia muito precisa sobre o processo de construção da derivação por parte do Prolog.
Mostre, avaliando um objectivo apropriado, que o programa está incorrecto.
Como o poderá corrigir?
Negação por falha.
Por vezes pretende-se garantir que um dado predicado não é válido. A utilização do cut (em conjunção com o predicado pré-definido fail que falha sempre) permite codificar uma forma restrita de negação: a "negação por falha". Considere o seguinte predicado:
neg(X) :- X, !, fail.
neg(X).
Note que neg(X) falha sempre que o Prolog consiga construir uma derivação para X. Por outro lado, sucede se falhar na construção dessa derivação (entra na segunda cláusula, que é trivialmente satisfeita). Obs.: o predicado pré-definido do Prolog \+ corresponde ao predicado neg apresentado.
Verifique o resultado de neg em predicados já definidos.
Construa a árvore de procura de soluções para a questão takeout(X,[1,2,3],Y).
Utilize o predicado takeout para definir um predicado que determine se uma lista é permutação de uma outra.
Tipos Algébricos
A utilização de termos permite a manipulação em Prolog de valores de tipos algébricos (que em Haskell seriam declarados com data). Um primeiro exemplo disso já foi ilustrado na última aula quando se manipularam naturais (zero, suc(zero), etc.). Para sistematizar, vejamos agora como manipular um outro tipo algébrico bem conhecido: as árvores binárias. Uma escolha óbvia para representar os seus valores será considerar o átomo vazia para representar a árvore vazia e termos da forma nodo(X,E,D) para representar nodos intermédios (com valor X, sub-árvore esquerda E e sub-árvore direita D). Temos então como exemplos de termos: vazia, nodo(4, vazia, vazia), etc.
Note no entanto que em Prolog não existe a noção de tipo (e.g. não podemos, à priori, condicionar um dado argumento de um predicado a ser uma árvore binária --- a única alternativa será definir-se um predicado que suceda para termos que tenham a estrutura prescrita...)
Defina um predicado arvBin/1 que verifique se o termo dado é uma árvore binária (e.g. deve falhar para termos como vazia(nodo,vazia(nodo))).
Defina um predicado que verifique se uma lista é uma travessia in-order de uma árvore.
Defina predicados que determinem:
uma árvore é uma Árvore Binária de Procura
uma lista está ordenada.
Aula 3: Árvores de derivação do Prolog.
Considere-se a definição do predicado member/2
member(X,[X|_]).
member(X,[_|T]) :- member(X,T).
Este predicado foi definido na última aula com o objectivo de verificar se um elemento está contido numa lista. De facto, podemos utiliza-lo como:
Mas podemos também utiliza-lo com variáveis não instanciadas com o objectivo de determinar quais os elementos de uma lista:
?- member(X,[1,2,3]).
X = 1 ;
X = 2 ;
X = 3 ;
fail.
Ou até para determinar soluções a questões mais complicadas, como (mais um exemplo da última aula):
?- member(X,[3,5,4,6,5,7]), X mod 2 =:= 0.
X = 4 ;
X = 6 ;
fail.
O objectivo desta aula é o de se perceber como é que o Prolog consegue chegar às soluções apresentadas (substituições de variáveis que validam o objectivo).
Inferência do Prolog
Um objectivo em Prolog consiste numa lista de predicados. O resultado da "execução" desse objectivo num interpretador consiste numa substituição que verifique esses predicados. O processo construção da substituição é normalmente designado por inferência, e pode ser justificado construindo uma árvore como se descreve:
Na raiz da árvore, coloca-se a lista de predicados. O Prolog irá processar cada predicado dessa lista por ordem.
Para cada predicado, o Prolog irá procurar encontrar na base de conhecimento uma instância dum facto ou duma regra cuja cabeça unifique com esse predicado. Esta procura processa-se também pela ordem pela qual as definições ocorrem na base de conhecimento.
Quando é encontrada uma regra nas condições referidas, cria-se um descendente na árvore contendo a lista já afectada pela substituição resultante da unificação (relembre que o resultada na unificação é uma substituição das variáveis) e onde o predicado em análise é substituído pelo lado direito da regra (ou simplesmente desaparece, no caso dos factos). É habitual anotarmos os arcos da árvore com as substituições resultantes das unificações.
Quando existe mais do que uma possibilidade para a referida unificação (e.g. várias regras são aplicáveis), traduz-se por uma ramificação da árvore de inferência.
Operacionalmente, o Prolog trata esta ramificação pelo mecanismo de backtracking (travessia depth-first da árvore).
Quando a lista de predicados fica vazia, cria-se uma folha na árvore denotada como true --- representa um resultado apresentado ao utilizador (a substituição calculada ao longo do caminho).
Quando não existe qualquer regra na base de conhecimento que unifique com o primeiro predicado da lista, cria-se uma folha denotada por fail .
A árvore de derivação para o objectivo "member(X,[1,2]), X mod 2 ==0" será:
Exercícios:
Considere a seguinte definição do predicado factorial:
fact(1,0).
fact(R,X) :- X2 is X-1, fact(R2,X2), R is X*R2.
Apresente a árvore de inferência para o objectivo fact(R,2).
Comente os resultados obtidos. Explique, em particular, que problemas aponta à solução apresentada.
Como pode ultrapassar os problemas detectados.
Considere o seguinte predicado:
nat2int(zero,0).
nat2int(suc(X),N) :- nat2int(X,N2), N is N2+1.
Apresente a árvore de inferência para o objectivo nat2int(suc(suc(zero)),X).
Apresente a árvore de inferência para o objectivo nat2int(X,2).
Comente os resultados obtidos.
Consegue propor alguma forma de ultrapassar os problemas detectados?
Tracing e Debug
Uma forma expedita de detectar problemas em programas Prolog consiste em utilizar o mecanismo de tracing. Esse mecanismo permite "monitorizar" determinados predicados durante o processo de inferência. Considere-se novamente o objectivo considerado atrás que faz uso do predicado member/2:
?- trace(member).
% member/2: [call, redo, exit, fail]
true.
[debug] ?- member(X,[1,2]), X mod 2 =:= 0.
T Call: (8) member(_G318, [1, 2])
T Exit: (8) member(1, [1, 2])
T Redo: (8) member(_G318, [1, 2])
T Call: (9) member(_G318, [2])
T Exit: (9) member(2, [2])
T Exit: (8) member(2, [1, 2])
X = 2 ;
T Redo: (9) member(_G318, [2])
T Call: (10) member(_G318, [])
T Fail: (10) member(_G318, [])
fail.
Note que o Prolog sinalizada diferentes eventos relativos ao predicado observado:
Call: o predicado em "resolução";
Exit: o predicado foi resolvido com sucesso (pode por isso ser removido da lista de objectivos);
Redo: nova visita ao predicado (por backtracking);
Fail: predicado falha definitivamente (já não existem mais alternativas para o backtracking).
Exercício:
Interprete o resultado do trace apresentado na árvore de inferência apresentada acima.
Realize análises de traces para as restantes árvores construídas nesta aula...
Aula 2: Operações aritméticas e Manipulação de listas.
Operações aritméticas
Já vimos que o Prolog aceita termos que representem expressões matemáticas, como 3+4*2. Mas quando manipulamos esses termos estamos normalmente interessados em avaliar essas expressões (i.e. calcular o seu resultado). O Prolog disponibiliza para o efeito o predicado is que avalia o segundo argumento e unifica o resultado com o primeiro. Alguns exemplos (onde se utiliza a notação infixa para o predicado):
?- X is 3+2.
X = 5.
?- 3+2 is 2+3.
fail.
?- 5 is 3+2.
true.
?- 5 is X+2.
ERROR: is/2: Arguments are not sufficiently instantiated
Um aspecto importante na utilização do predicado is é a assimetria induzida: o segundo argumento deve ser sempre uma expressão completamente instanciada. Assim, se definirmos o predicado:
soma(X,Y,Z) :- X is Y + Z.
devemos considerar o segundo e o terceiro argumentos como "argumentos de entrada", que necessitam estar devidamente instanciados. Uma forma compacta de se exprimir esse facto (normalmente utilizada na documentação) é através da assinatura soma(-X,+Y,+Z) --- assim identifica-se o argumento Y e Z como de entrada e X como de saída.
Exercício:
Defina o predicado factorial(-R,+X) que suceda quando R for o factorial de X.
Uma forma alternativa de lidar com números naturais consiste em considerar termos zero, suc(zero), suc(suc(zero)), etc. (i.e. utilizar notação unária para os naturais). Defina o predicado nat2int que sucede quando o primeiro argumento é a representação unária do segundo.
No predicado definido na alínea anterior, verifique:
que argumentos tem de ser utilizados como entrada e como saída;
o que acontece quando solicita ao interpretador várias respostas.
Verifique, com o auxílio do mecanismo de help do SWI-Prolog (ou da documentação on-line, se preferir) qual a funcionalidade oferecida pelos operadores:
=:=, =\=, <, =<, ==, @<
Manipulação de listas
Um exemplo de um tipo estruturado muito utilizado em Prolog são as listas. A sintaxe pré-definida é [] que denota a lista vazia e [H|T] que denota a lista com cabeça H e cauda T.
Defina member/2 que verifica se um elemento pertence a uma lista.
Utilize o predicado member para determinar quais dos elementos da lista [3,5,4,6,5,7] são pares.
Defina um predicado que permita calcular o somatório de uma lista de inteiros.
O que alteraria, no predicado definido na alínea anterior, para calcular o somatório de uma lista de expressões inteiras?
Aula 1: Apresentação da linguagem PROLOG
Ao longo das aulas práticas de Lógica Computacional fazer uso da linguagem PROLOG. O interpretador adoptado será o SWI-Prolog que está disponível para para a generalidade das plataformas (MS-Windows, Linux, macOSX).
Conceitos Preliminares
Termos: o Prolog é uma linguagem simbólica que manipula termos que podem ser:
Variáveis - denotadas por identificadores começados por letras maiúsculas (e.g. X, Y, Xs, ...);
Constantes - átomos (identificadores começados por letras minúsculas) ou valores de tipos pré-definidos como inteiros, reais, strings, etc. (e.g. abc, xyz, 32, 3.1415)
Termos Compostos - termos da forma f(t1,...,tn) onde f é designado por functor (nome da função) e t1...tn são termos (e.g. xyz(X,abc), abc(abc(abc,abc)), +(4,2))
obs.: como iremos ver adiante, o Prolog permite a declaração de operadores infixos. Assim irá permitir escrever 4 + 2 como alternativa ao termo +(4,2) (o mesmo se aplica a outros operadores infixos que serão apresentados adiante).
Substituições e Unificação: o que caracteriza as variáveis é o facto de elas poderem vir a ser substituidas por outros termos. Considere-se o termo t(X,Y): se substituirmos X por abc(A,3) e Y por Z obtemos o termos t(abc(A,3),Z).
Uma operação fundamental no modelo de execução do Prolog é o que se designa por Unificação de dois termos. A ideia consiste em encontrar uma substituição que iguale (se possível) os termos dados. Vejamos alguns exemplos:
X = 4, Y = 3 é um unificador dos termos abc(3,X) e abc(Y,4);
X = 4, Y = 3 é um unificador dos termos abc(X,X) e abc(Y,4);
os termos abc(3,4) e abc(X,X) não dispõe de unificador.
Uma característica dos unificadores apresentados é que se tratam sempre dos unificadores mais gerais (qualquer outra substituição que unifique os termos pode ser expressa como um refinamento da substituição dada). Adiante iremos ter oportunidade de aprofundar estes aspectos mais teóricos... Para já interessa reter que o Prolog, quando unificar dois termos, determina sempre o unificador mais geral (i.e. a substituição mais simples que iguala os termos).
EXERCÍCIO: Determine o unificador mais geral para os seguintes pares de termos (se existir... naturalmente):
f(X,g(Y)) e g(X,f(Y))
f(X,g(Y)) e Z
f(X,g(y)) e f(g(y),X)
f(X) e X
f(X) e f(3+2)
f(3) e f(2+1)
f(3) e A(X)
Programas em Prolog
Executar um programa em Prolog consiste em interrogar o interpretador sobre a validade de um dado predicado lógico. A resposta mais simples será então true ou fail (se o predicado for válido ou não, respectivamente).
Objectivo (Goal):
Quando se invoca o SWI-Prolog, surge o prompt?- que assinala que o interpretador aguarda a introdução de um objectivo (ou query, ou goal).
Calvin:~ jba$ /opt/local/bin/swipl
Welcome to SWI-Prolog (Multi-threaded, 32 bits, Version 5.6.51)
Copyright (c) 1990-2008 University of Amsterdam.
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software,
and you are welcome to redistribute it under certain conditions.
Please visit http://www.swi-prolog.org for details.
For help, use ?- help(Topic). or ?- apropos(Word).
?-
Como referimos, o objectivo será um predicado lógico. Iremos ter oportunidade de definir novos predicados mas, para já, concentremo-nos na utilização do predicado pré-definido =/2 (o /2 significa que o predicado espera dois argumentos). Este predicado será válido precisamente quando os termos que forem passados como argumentos unificarem. Assim podemos introduzir:
?- =(3,3).
true.
?- 3=3.
true.
?- 3=2.
fail.
?- 3=X.
X = 3.
?- 3+2=X.
X = 3+2.
?- 3 + X = Y * 2.
fail.
?-
Os exemplos apresentados revelam-nos duas coisas: (1) podemos utilizar a notação infixa e, (2) quando no objectivo estão envolvidas veriáveis o Prolog retorna uma substituição dessas variáveis que verifiquem o predicado (ou falha, se não existir nenhuma substituição nessas condições) --- podemos então dizer que, intuitivamente, as variáveis dos objectivos estão quantificadas existencialmente.
EXERCÍCIO: Interrogue o interpretador de Prolog por forma a ele retornar os unificadores mais gerais atrás solicitados.
Factos (base de conhecimento I):
Referimos que executar um programa em Prolog consiste em interrogar o interpretador relativamente a um objectivo. Mas, em que é que consiste um programa Prolog?. Um programa em Prolog será a base de conhecimento que o interpretador utiliza para determinar a validade do objectivo pedido. Essa base de conhecimento será consituída por:
Factos: que estabelecem a validade imediata (de instâncias) de predicados;
Regras: que condicionam a validade de predicados à validade de sub-objectivos.
Comecemos pelos primeiros. Como exemplos de factos podemos ter:
Com base nestes factos, diriamos que pai(joaquim,manuel) é válido mas pai(joaquim,jose) já não o é (porque nada estabelece a sua validade). Para verificar isso com o Prolog, necessitamos de carregar a base de conhecimento no interpretador. Para tal devemos:
gravar um ficheiro com os factos apresentados (normalmente dá-se a extensão ".pl" aos ficheiros Prolog, e.g. "pai.pl");
carregar o ficheiro no interpretador por intermédio do predicado pré-definido consult (e.g. "consult(pai.pl)").
EXERCÍCIO: Verifique a validade de alguns objectivos com a base de conhecimento apresentada. O que acontece quando se inclui variáveis?
Por vezes, o interpretador retorna uma substituição de resultado sem voltar ao prompt inicial. Isso assinala que a solução apresentada é uma de várias possíveis, podendo o utilizador:
digitar . e retornar ao prompt inicial;
digitar ; para solicitar outra solução.
EXERCÍCIO:
introduza um predicado que permita determinar todos os filhos de "manuel".
o que aconteceria se incluisse na base de conhecimento o facto pai(X,carlos) ? Experimente... (verifique o impacto de o incluir no início e no fim da base de conhecimento).
O exercício anterior permite concluir que, nos factos, devemos realizar uma interpretação universal das variáveis.
Se as questões colocadas ao interpretador de Prolog são predicados lógicos, é natural perguntarmo-nos como construir predicados à custa de conectivas lógicas (como e, ou, etc.). O Prolog tem definido os operadores:
conjunção: denotado por uma vírgula (,)
disjunção: denotado por um ponto e vírgula (;)
(As restantes conectivas lógicas proposicionais serão introduzidas mais tarde.)
Regras (base de conhecimento II):
A expressividade do Prolog resulta do facto de permitir incluir, na base de conhecimento, regras que condicionam a validade de um predicado (colocado no lado esquerdo do operador :-, e designado por cabeça da regra) à validade de um conjunto de outros predicados (designados por corpo da regra). A título de exemplo, temos que a regra:
avo(X,Y) :- pai(X,Z), pai(Z,Y).
Quando acrescentada à base de conhecimento apresentada acima, permite que o Prolog responda afirmativamente ao predicado avo(francisco,manuel). No processo, o interpretador verificará os predicados pai(francisco,joao) e pai(joao,manuel).
Note que nas regras, as variáveis que ocorrem na cabeça da regra devem ser entendidas como quantificadas universalmente (como nos factos). Já as que só ocorrem no corpo da regra devem ser entendidas como quantificadas existencialmente (como nos objectivos).
Exercício: Extenda a base de conhecimento para exprimir outros graus de parentesco, como "irmão", "tio", etc.
Aula 10: Predicados de Segunda Ordem e outros predicados primitivos disponibilizados pelo Prolog
Predicados de segunda ordem
Existem meta-predicados que permitem coleccionar todas as soluções para um dado
objectivo de prova (ver User's Manual ou o help).
findall(?Template,:Goal,?Bag) : Bag é a lista de instâncias de Template encontradas nas provas de Goal. A ordem da lista corresponde à ordem em que são encontradas as respostas. Se não existirem instanciações para Template, Bag unifica com a lista vazia.
bagof(?Template,:Goal,?Bag) : Semelhante a findall, mas se Goal falhar, bagof falha.
setof(?Template,:Goal,?Set) : Semelhante a bagof, mas a lista é ordenada e sem repetições.
Exemplo:
| ?- findall(X, member(X,[1,2,3]), L).
L = [1,2,3]
yes
Relacionados com os apresentados, encontramos outros predicados de ordem superior, como o bem conhecido map (do haskell). No Prolog o predicado maplist implementa a funcionalidade análoga.
Exercícios:
Teste os predicados apresentados codificando exemplos apropriados.
Utilize o predicado findall para determinar todas as soluções para o problema das N rainhas com N=8.
Outras características do Prolog
Manipulação da base de conhecimento: O Prolog permite manipular dinamicamente a base de conhecimento (inserir ou remover factos ou regras). Para isso disponibiliza os predicados assert, retract, rectractall (e variantes...).
Input/Output: tal como qualquer linguagem com o mínimo de preocupações práticas, é possível realizar operações de Input/Output. Para o efeito dispõe-se dos predicados write, read (entre outros, e com muitas variantes...); open e close para maniputação de ficheiros, etc...
Exercícios:
Consulte a documentação relativa aos predicados referidos e teste cada um deles com exemplos apropriados.
Extenda o programa das N rainhas com um predicado runQueens que interrogue o utilizador sobre o número de rainhas a considerar e imprima no écran todas as soluções admissíveis.
Aula 9: Estratégia Gerar e Testar.
Estratégia Gerar e Testar
O mecanismo de backtracking do PROLOG torna possível codificar, de forma directa, a estratégia de gerar e testar para encontrar a solução de um determinado problema. Segundo esta estratégia, o problema é decomposto em duas fases:
Gera-se "soluções cadidatas" para o problema.
Verifica-se se a "solução candidata" satisfaz os requisitos do problema (e é, portanto, uma "solução efectiva").
Podemos assim identificar o padrão com a seguinte regra PROLOG:
resolve(X) :- gera(X), testa(X).
Note-se o papel preponderante do backtracking para encontrar uma dada solução para resolve(X): o predicado gera(X) instancia X com uma possível solução. No caso de testa(X) falhar (a solução proposta não satisfaz os requisitos impostos pelo problema), o mecanismo de backtracking permite que gera(X) instancie uma nova alternativa, até que se encontre a solução pretendida.
O predicado gera acaba normalmente por se revelar o ponto crítico na aplicação desta estratégia: por um lado, pretende-se que ele cubra todas as possíveis soluções para o problema (caso contrário, podemos nunca gerar a solução requerida). Por outro, e por questões de eficiência, vamos pretender que ele produza o mínimo de soluções erradas (para minimizar o espaço de busca) -- na prática, este esforço de minimização traduz-se por eliminar candidatos notoriamente errados e por encontrar codificações apropriadas para as possíveis soluções.
Vejamos um exemplo concreto: pretende-se encontrar um divisor para um dado número N (diferente de 1 e N).
fromToL(L,U,[]) :- U < L, !.
fromToL(L,U,[L|X]) :- L1 is L+1, fromToL(L1,U,X).
gera(N,X) :- fromToL(2,N-1,L), member(X,L).
testa(N,X) :- N mod X =:= 0.
divisor(N,X) :- gera(N,X), testa(N,X).
Mas o programa apresentado pode ser consideravelmente optimizado se observarmos que nos é suficiente encontrar um divisor entre 2 e sqrt(N) (se X>sqrt(N) é um divisor de N, então também será N/X<sqrt(N)). Dessa forma teríamos:
divisor2(N,X) :- fromtoL(2,sqrt(N),L), member(X,L), N mod X =:= 0.
Verifique ambos os programas para um número primo elevado (e.g. 209953, 331777, 472393, ...)
Utilize a estratégia generate & test para determinar a raiz de um natural, definida da seguinte forma: um número natural X é a raiz de N quando X2<=N e (X+1)2>N
Problema das N rainhas.
Um exemplo clássico de programação em PROLOG consiste em escrever um predicado que permita resolver o problema das n rainhas. Esse problema consiste em dispor n rainas num tabuleiro de damas com dimensão n*n, sem que qualquer rainha se encontre ameaçada por outra. Como um exemplo de uma solução temos (num tabuleiro 4*4):
Q
Q
Q
Q
Note que cada linha e cada coluna deve conter uma, e só uma, rainha (porquê?).
Dito isto, verificamos que uma forma expedita de representar as soluções para este problema consiste em utilizar uma lista que informe qual a coluna em que é colocada a rainha de cada uma das linhas (a solução do exemplo seria [3,1,4,2], querendo dizer que a rainha da primeira linha aparece na terceira coluna, a da segunda linha na primeira coluna, etc.) -- desta forma, aparece uma rainha em cada linha "por construção". A restrição de aparecer uma única rainha por cada coluna é traduzida por deverem aparecer na lista todos os números de 1 a 4, ou seja, a lista deve ser uma permutação de [1,2,3,4]. Temos assim resolvido o sub-problema de gerar soluções candidatas: são simplesmente permutações da lista [1..N].
Na fase de teste, falta unicamente verificar que nenhuma rainha está no alcance da diagonal de uma outra. Para isso notamos que:
Duas rainhas estão numa diagonal / sse a soma da linha e coluna da posição de cada uma delas for igual;
Duas rainhas estão numa diagonal \ sse a diferença da linha e coluna da posição de cada uma delas for igual.
Com base no que foi referido, codifique um predicado nrainhas(+N,?X) que determine uma solução para o problema das N-rainhas.
Aula 8: Implementação do algoritmo Davis-Putnam em Prolog.
Pretende-se definir um programa que permita verificar se uma dada fórmula é uma contradição pelo método de Davis Putnam. Para o efeito, sugere-se que considere o seguinte predicado matCNF que converte uma Forma Normal Conjuntiva (FNC) na respectiva forma matricial (como uma lista de listas):
% -----------------------------------------------------------------
% matCNF(+FNC,?MAT)
%
% FNC é uma forma normal conjuntiva e MAT é a sua representação sob a forma
% de matriz (lista de listas de literais).
% obs: os literais são da forma "atom" ou "-atom".
matCNF((A /\ B),M) :- !, matCNF(A,MA), matCNF(B,MB), append(MA,MB,M).
matCNF((A \/ B),C) :- !, matCNF(A,[CA]), matCNF(B,[CB]), union2(CA,CB,C).
matCNF(~Lit, [[TWiki.-Lit][-Lit]]) :- !.
matCNF(Lit, [[TWiki.Lit][Lit]]).
union2([],L,[L]).
union2([X|L1],L2,L3) :- member2(X,L2), !, union2(L1,L2,L3).
union2([X|_],L2,[]) :- (-Xn=X;-X=Xn), member2(Xn,L2), !.
union2([X|L1],L2,L3) :- union2(L1,[X|L2],L3).
member2(X,[Y|_]) :- X==Y, !.
member2(X,[_|T]) :- member2(X,T).
Exercícios:
Defina o predicado de split/3 que determine o particionamento de uma FNC.
Defina o predicado davisPutnam/1 que verifique se uma fórmula proposicional é inconsistente.
Aula 7: Lógica Proposicional em Prolog.
Cálculo de Sequentes.
Pretende-se definir um predicado em Prolog que implemente as regras do cálculo de sequentes LC. Para tal deverá considerar que os sequentes são constituídos por pares de listas, sendo portanto o predicado pretendido da forma lc(+Gamma,+Delta) (Gamma e Delta são listas de fórmulas e o predicado verificará se o sequente Gamma |- Delta é válido ou não).
Formas Normais.
Defina os predicados:
nnf(+Form, -NNF) que determine a forma normal negativa de uma fórmula.
cnf(+NNF, -CNF) que determina a forma normal conjuntiva (FNC) de uma fórmula dada na FNN.
Aula 6: Manipulação de fórmulas de lógica proposicional em Prolog.
Definição de Operadores em Prolog.
O Prolog permite definir operadores prefixos, sufixos ou infixos. Para tal devemos utilizar o predicado pré-definido op(Prec,Type,Name). O argumento Name é o nome do operador definido; Prec é um número entre 0 e 1200 que determinará a sua precedência e Type determina o seu tipo e associatividade. Por exemplo, o operador de soma binário + está definido como op(700, yfx, +). A precedência 700 irá determinar que tenha menos precedência do que a multiplicação (definida com precedência 500 - note que um número menor indica maior precedência do operador), e o tipo yfx caracteriza o operador como infixo e associativo à esquerda. Outras possibilidades para o tipo dos operadores são: xfy, xfx para operadores infixos associativos à direita e sem associatividade; fx, fy para operadores prefixos e xf, yf para operadores sufixos.
Alguns dos operadores pré-definidos do Prolog são:
Faça um pequeno predicado que lhe permita confirmar a maior precedência do operador * face ao operador +.
Manipulação de fórmulas de lógica proposicional em Prolog.
A definição de operadores permite que a sintaxe do Prolog se aproxime do domínio onde se está a trabalhar. Considere que se pretendem representar fórmulas da Lógica Proposicional em Prolog. Em vez de considerar termos como or(not(p), and( and(p, r), not(q))), podemos utilizar operadores que nos permitam aproximar a sua representação da utilizada habitualmente. Assim definimos:
que denotam os operadores de implicação, disjunção, conjunção e negação. Assim, a fórmula apresentada atrás pode ser escrita como (~p \/ p /\ r /\ ~q) (note o papel da precedência e associatividade).
Exercícios:
Defina o predicado props(+Form,-Props) que calcule o conjunto de símbolos de proposições utilizados na fórmula dada.
Defina o predicado val(+Form,+Mod) que verifique se a fórmula é válida no modelo passado como argumento.
Como poderia reformular a definição do predicado val por forma a que não seja necessário instanciar o modelo (ou seja, construir o predicado valM(+Form, ?Mod).
Aula 5: Utilização de cut e negação por falha.
O predicado pré-definido cut (!) permite eliminar ramos nas árvores de derivação de predicados Prolog. Operacionalmente, o cut pode ser caracterizado da seguinte forma: Durante o processo de prova, a 1a passagem pelo cut é sempre verdadeira (com sucesso). Se por backtracking se voltar ao cut, então o cut faz falhar o predicado que está na cabeça da regra.
A utilização do cut está normalmente associada a questões de eficiência: os ramos da árvore que são eliminados acabariam eventualmente por falhar, e assim poupamos trabalho ao motor de inferência do Prolog. Esta utilização do cut é considerada benigna (green cut), porque não se afecta o significado dos predicados. Tomemos como exemplo um predicado que verifique se o terceiro argumento é o mínimo dos dois primeiros. Podería ser definido como:
minimo(X,Y,Y) :- X >= Y.
minimo(X,Y,X) :- X < Y.
Mas podemos facilmente observar que, uma vez verificado que X>=Y, não faz sentido tentar verificar que X<Y. Assim sendo, faz sentido colocar um cut no final da primeira cláusula:
minimo(X,Y,Y) :- X >= Y, !.
minimo(X,Y,X) :- X < Y.
Estaria correcto eliminar também o predicado X<Y na segunda cláusula? Justifique com exemplos apropriados.
É importante referir que certas utilizações do cut alteram propositadamente o comportamento do programa (tipicamente para impedir que a execução do programa entre em ciclo). Essas utilizações são normalmente consideradas "mais perigosas" (red cuts) porque obrigam a que o programador detenha uma ideia muito precisa sobre o processo de construção da derivação por parte do Prolog.
Mostre, avaliando um objectivo apropriado, que o programa está incorrecto.
Como o poderá corrigir?
Negação por falha.
Por vezes pretende-se garantir que um dado predicado não é válido. A utilização do cut (em conjunção com o predicado pré-definido fail que falha sempre) permite codificar uma forma restrita de negação: a "negação por falha". Considere o seguinte predicado:
neg(X) :- X, !, fail.
neg(X).
Note que neg(X) falha sempre que o Prolog consiga construir uma derivação para X. Por outro lado, sucede se falhar na construção dessa derivação (entra na segunda cláusula, que é trivialmente satisfeita). Obs.: o predicado pré-definido do Prolog \+ corresponde ao predicado neg apresentado.
Verifique o resultado de neg em predicados já definidos.
Construa a árvore de procura de soluções para a questão takeout(X,[1,2,3],Y).
Utilize o predicado takeout para definir um predicado que determine se uma lista é permutação de uma outra.
Tipos Algébricos
A utilização de termos permite a manipulação em Prolog de valores de tipos algébricos (que em Haskell seriam declarados com data). Um primeiro exemplo disso já foi ilustrado na última aula quando se manipularam naturais (zero, suc(zero), etc.). Para sistematizar, vejamos agora como manipular um outro tipo algébrico bem conhecido: as árvores binárias. Uma escolha óbvia para representar os seus valores será considerar o átomo vazia para representar a árvore vazia e termos da forma nodo(X,E,D) para representar nodos intermédios (com valor X, sub-árvore esquerda E e sub-árvore direita D). Temos então como exemplos de termos: vazia, nodo(4, vazia, vazia), etc.
Note no entanto que em Prolog não existe a noção de tipo (e.g. não podemos, à priori, condicionar um dado argumento de um predicado a ser uma árvore binária --- a única alternativa será definir-se um predicado que suceda para termos que tenham a estrutura prescrita...)
Defina um predicado arvBin/1 que verifique se o termo dado é uma árvore binária (e.g. deve falhar para termos como vazia(nodo,vazia(nodo))).
Defina um predicado que verifique se uma lista é uma travessia in-order de uma árvore.
Defina predicados que determinem:
uma árvore é uma Árvore Binária de Procura
uma lista está ordenada.
Aula 3: Árvores de derivação do Prolog.
Considere-se a definição do predicado member/2
member(X,[X|_]).
member(X,[_|T]) :- member(X,T).
Este predicado foi definido na última aula com o objectivo de verificar se um elemento está contido numa lista. De facto, podemos utiliza-lo como:
Mas podemos também utiliza-lo com variáveis não instanciadas com o objectivo de determinar quais os elementos de uma lista:
?- member(X,[1,2,3]).
X = 1 ;
X = 2 ;
X = 3 ;
fail.
Ou até para determinar soluções a questões mais complicadas, como (mais um exemplo da última aula):
?- member(X,[3,5,4,6,5,7]), X mod 2 =:= 0.
X = 4 ;
X = 6 ;
fail.
O objectivo desta aula é o de se perceber como é que o Prolog consegue chegar às soluções apresentadas (substituições de variáveis que validam o objectivo).
Inferência do Prolog
Um objectivo em Prolog consiste numa lista de predicados. O resultado da "execução" desse objectivo num interpretador consiste numa substituição que verifique esses predicados. O processo construção da substituição é normalmente designado por inferência, e pode ser justificado construindo uma árvore como se descreve:
Na raiz da árvore, coloca-se a lista de predicados. O Prolog irá processar cada predicado dessa lista por ordem.
Para cada predicado, o Prolog irá procurar encontrar na base de conhecimento uma instância dum facto ou duma regra cuja cabeça unifique com esse predicado. Esta procura processa-se também pela ordem pela qual as definições ocorrem na base de conhecimento.
Quando é encontrada uma regra nas condições referidas, cria-se um descendente na árvore contendo a lista já afectada pela substituição resultante da unificação (relembre que o resultada na unificação é uma substituição das variáveis) e onde o predicado em análise é substituído pelo lado direito da regra (ou simplesmente desaparece, no caso dos factos). É habitual anotarmos os arcos da árvore com as substituições resultantes das unificações.
Quando existe mais do que uma possibilidade para a referida unificação (e.g. várias regras são aplicáveis), traduz-se por uma ramificação da árvore de inferência.
Operacionalmente, o Prolog trata esta ramificação pelo mecanismo de backtracking (travessia depth-first da árvore).
Quando a lista de predicados fica vazia, cria-se uma folha na árvore denotada como true --- representa um resultado apresentado ao utilizador (a substituição calculada ao longo do caminho).
Quando não existe qualquer regra na base de conhecimento que unifique com o primeiro predicado da lista, cria-se uma folha denotada por fail .
A árvore de derivação para o objectivo "member(X,[1,2]), X mod 2 ==0" será:
Exercícios:
Considere a seguinte definição do predicado factorial:
fact(1,0).
fact(R,X) :- X2 is X-1, fact(R2,X2), R is X*R2.
Apresente a árvore de inferência para o objectivo fact(R,2).
Comente os resultados obtidos. Explique, em particular, que problemas aponta à solução apresentada.
Como pode ultrapassar os problemas detectados.
Considere o seguinte predicado:
nat2int(zero,0).
nat2int(suc(X),N) :- nat2int(X,N2), N is N2+1.
Apresente a árvore de inferência para o objectivo nat2int(suc(suc(zero)),X).
Apresente a árvore de inferência para o objectivo nat2int(X,2).
Comente os resultados obtidos.
Consegue propor alguma forma de ultrapassar os problemas detectados?
Tracing e Debug
Uma forma expedita de detectar problemas em programas Prolog consiste em utilizar o mecanismo de tracing. Esse mecanismo permite "monitorizar" determinados predicados durante o processo de inferência. Considere-se novamente o objectivo considerado atrás que faz uso do predicado member/2:
?- trace(member).
% member/2: [call, redo, exit, fail]
true.
[debug] ?- member(X,[1,2]), X mod 2 =:= 0.
T Call: (8) member(_G318, [1, 2])
T Exit: (8) member(1, [1, 2])
T Redo: (8) member(_G318, [1, 2])
T Call: (9) member(_G318, [2])
T Exit: (9) member(2, [2])
T Exit: (8) member(2, [1, 2])
X = 2 ;
T Redo: (9) member(_G318, [2])
T Call: (10) member(_G318, [])
T Fail: (10) member(_G318, [])
fail.
Note que o Prolog sinalizada diferentes eventos relativos ao predicado observado:
Call: o predicado em "resolução";
Exit: o predicado foi resolvido com sucesso (pode por isso ser removido da lista de objectivos);
Redo: nova visita ao predicado (por backtracking);
Fail: predicado falha definitivamente (já não existem mais alternativas para o backtracking).
Exercício:
Interprete o resultado do trace apresentado na árvore de inferência apresentada acima.
Realize análises de traces para as restantes árvores construídas nesta aula...
Aula 2: Operações aritméticas e Manipulação de listas.
Operações aritméticas
Já vimos que o Prolog aceita termos que representem expressões matemáticas, como 3+4*2. Mas quando manipulamos esses termos estamos normalmente interessados em avaliar essas expressões (i.e. calcular o seu resultado). O Prolog disponibiliza para o efeito o predicado is que avalia o segundo argumento e unifica o resultado com o primeiro. Alguns exemplos (onde se utiliza a notação infixa para o predicado):
?- X is 3+2.
X = 5.
?- 3+2 is 2+3.
fail.
?- 5 is 3+2.
true.
?- 5 is X+2.
ERROR: is/2: Arguments are not sufficiently instantiated
Um aspecto importante na utilização do predicado is é a assimetria induzida: o segundo argumento deve ser sempre uma expressão completamente instanciada. Assim, se definirmos o predicado:
soma(X,Y,Z) :- X is Y + Z.
devemos considerar o segundo e o terceiro argumentos como "argumentos de entrada", que necessitam estar devidamente instanciados. Uma forma compacta de se exprimir esse facto (normalmente utilizada na documentação) é através da assinatura soma(-X,+Y,+Z) --- assim identifica-se o argumento Y e Z como de entrada e X como de saída.
Exercício:
Defina o predicado factorial(-R,+X) que suceda quando R for o factorial de X.
Uma forma alternativa de lidar com números naturais consiste em considerar termos zero, suc(zero), suc(suc(zero)), etc. (i.e. utilizar notação unária para os naturais). Defina o predicado nat2int que sucede quando o primeiro argumento é a representação unária do segundo.
No predicado definido na alínea anterior, verifique:
que argumentos tem de ser utilizados como entrada e como saída;
o que acontece quando solicita ao interpretador várias respostas.
Verifique, com o auxílio do mecanismo de help do SWI-Prolog (ou da documentação on-line, se preferir) qual a funcionalidade oferecida pelos operadores:
=:=, =\=, <, =<, ==, @<
Manipulação de listas
Um exemplo de um tipo estruturado muito utilizado em Prolog são as listas. A sintaxe pré-definida é [] que denota a lista vazia e [H|T] que denota a lista com cabeça H e cauda T.
Defina member/2 que verifica se um elemento pertence a uma lista.
Utilize o predicado member para determinar quais dos elementos da lista [3,5,4,6,5,7] são pares.
Defina um predicado que permita calcular o somatório de uma lista de inteiros.
O que alteraria, no predicado definido na alínea anterior, para calcular o somatório de uma lista de expressões inteiras?
Defina o predicado concat/3 que verifique quando uma lista é a concatenação de outras duas. Verifique o resultado quando o invoca com diferentes listas instanciadas.
Aula 1: Apresentação da linguagem PROLOG
Ao longo das aulas práticas de Lógica Computacional fazer uso da linguagem PROLOG. O interpretador adoptado será o SWI-Prolog que está disponível para para a generalidade das plataformas (MS-Windows, Linux, macOSX).
Conceitos Preliminares
Termos: o Prolog é uma linguagem simbólica que manipula termos que podem ser:
Variáveis - denotadas por identificadores começados por letras maiúsculas (e.g. X, Y, Xs, ...);
Constantes - átomos (identificadores começados por letras minúsculas) ou valores de tipos pré-definidos como inteiros, reais, strings, etc. (e.g. abc, xyz, 32, 3.1415)
Termos Compostos - termos da forma f(t1,...,tn) onde f é designado por functor (nome da função) e t1...tn são termos (e.g. xyz(X,abc), abc(abc(abc,abc)), +(4,2))
obs.: como iremos ver adiante, o Prolog permite a declaração de operadores infixos. Assim irá permitir escrever 4 + 2 como alternativa ao termo +(4,2) (o mesmo se aplica a outros operadores infixos que serão apresentados adiante).
Substituições e Unificação: o que caracteriza as variáveis é o facto de elas poderem vir a ser substituidas por outros termos. Considere-se o termo t(X,Y): se substituirmos X por abc(A,3) e Y por Z obtemos o termos t(abc(A,3),Z).
Uma operação fundamental no modelo de execução do Prolog é o que se designa por Unificação de dois termos. A ideia consiste em encontrar uma substituição que iguale (se possível) os termos dados. Vejamos alguns exemplos:
X = 4, Y = 3 é um unificador dos termos abc(3,X) e abc(Y,4);
X = 4, Y = 3 é um unificador dos termos abc(X,X) e abc(Y,4);
os termos abc(3,4) e abc(X,X) não dispõe de unificador.
Uma característica dos unificadores apresentados é que se tratam sempre dos unificadores mais gerais (qualquer outra substituição que unifique os termos pode ser expressa como um refinamento da substituição dada). Adiante iremos ter oportunidade de aprofundar estes aspectos mais teóricos... Para já interessa reter que o Prolog, quando unificar dois termos, determina sempre o unificador mais geral (i.e. a substituição mais simples que iguala os termos).
EXERCÍCIO: Determine o unificador mais geral para os seguintes pares de termos (se existir... naturalmente):
f(X,g(Y)) e g(X,f(Y))
f(X,g(Y)) e Z
f(X,g(y)) e f(g(y),X)
f(X) e X
f(X) e f(3+2)
f(3) e f(2+1)
f(3) e A(X)
Programas em Prolog
Executar um programa em Prolog consiste em interrogar o interpretador sobre a validade de um dado predicado lógico. A resposta mais simples será então true ou fail (se o predicado for válido ou não, respectivamente).
Objectivo (Goal):
Quando se invoca o SWI-Prolog, surge o prompt?- que assinala que o interpretador aguarda a introdução de um objectivo (ou query, ou goal).
Calvin:~ jba$ /opt/local/bin/swipl
Welcome to SWI-Prolog (Multi-threaded, 32 bits, Version 5.6.51)
Copyright (c) 1990-2008 University of Amsterdam.
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software,
and you are welcome to redistribute it under certain conditions.
Please visit http://www.swi-prolog.org for details.
For help, use ?- help(Topic). or ?- apropos(Word).
?-
Como referimos, o objectivo será um predicado lógico. Iremos ter oportunidade de definir novos predicados mas, para já, concentremo-nos na utilização do predicado pré-definido =/2 (o /2 significa que o predicado espera dois argumentos). Este predicado será válido precisamente quando os termos que forem passados como argumentos unificarem. Assim podemos introduzir:
?- =(3,3).
true.
?- 3=3.
true.
?- 3=2.
fail.
?- 3=X.
X = 3.
?- 3+2=X.
X = 3+2.
?- 3 + X = Y * 2.
fail.
?-
Os exemplos apresentados revelam-nos duas coisas: (1) podemos utilizar a notação infixa e, (2) quando no objectivo estão envolvidas veriáveis o Prolog retorna uma substituição dessas variáveis que verifiquem o predicado (ou falha, se não existir nenhuma substituição nessas condições) --- podemos então dizer que, intuitivamente, as variáveis dos objectivos estão quantificadas existencialmente.
EXERCÍCIO: Interrogue o interpretador de Prolog por forma a ele retornar os unificadores mais gerais atrás solicitados.
Factos (base de conhecimento I):
Referimos que executar um programa em Prolog consiste em interrogar o interpretador relativamente a um objectivo. Mas, em que é que consiste um programa Prolog?. Um programa em Prolog será a base de conhecimento que o interpretador utiliza para determinar a validade do objectivo pedido. Essa base de conhecimento será consituída por:
Factos: que estabelecem a validade imediata (de instâncias) de predicados;
Regras: que condicionam a validade de predicados à validade de sub-objectivos.
Comecemos pelos primeiros. Como exemplos de factos podemos ter:
Com base nestes factos, diriamos que pai(joaquim,manuel) é válido mas pai(joaquim,jose) já não o é (porque nada estabelece a sua validade). Para verificar isso com o Prolog, necessitamos de carregar a base de conhecimento no interpretador. Para tal devemos:
gravar um ficheiro com os factos apresentados (normalmente dá-se a extensão ".pl" aos ficheiros Prolog, e.g. "pai.pl");
carregar o ficheiro no interpretador por intermédio do predicado pré-definido consult (e.g. "consult(pai.pl)").
EXERCÍCIO: Verifique a validade de alguns objectivos com a base de conhecimento apresentada. O que acontece quando se inclui variáveis?
Por vezes, o interpretador retorna uma substituição de resultado sem voltar ao prompt inicial. Isso assinala que a solução apresentada é uma de várias possíveis, podendo o utilizador:
digitar . e retornar ao prompt inicial;
digitar ; para solicitar outra solução.
EXERCÍCIO:
introduza um predicado que permita determinar todos os filhos de "manuel".
o que aconteceria se incluisse na base de conhecimento o facto pai(X,carlos) ? Experimente... (verifique o impacto de o incluir no início e no fim da base de conhecimento).
O exercício anterior permite concluir que, nos factos, devemos realizar uma interpretação universal das variáveis.
Se as questões colocadas ao interpretador de Prolog são predicados lógicos, é natural perguntarmo-nos como construir predicados à custa de conectivas lógicas (como e, ou, etc.). O Prolog tem definido os operadores:
conjunção: denotado por uma vírgula (,)
disjunção: denotado por um ponto e vírgula (;)
(As restantes conectivas lógicas proposicionais serão introduzidas mais tarde.)
Regras (base de conhecimento II):
A expressividade do Prolog resulta do facto de permitir incluir, na base de conhecimento, regras que condicionam a validade de um predicado (colocado no lado esquerdo do operador :-, e designado por cabeça da regra) à validade de um conjunto de outros predicados (designados por corpo da regra). A título de exemplo, temos que a regra:
avo(X,Y) :- pai(X,Z), pai(Z,Y).
Quando acrescentada à base de conhecimento apresentada acima, permite que o Prolog responda afirmativamente ao predicado avo(francisco,manuel). No processo, o interpretador verificará os predicados pai(francisco,joao) e pai(joao,manuel).
Note que nas regras, as variáveis que ocorrem na cabeça da regra devem ser entendidas como quantificadas universalmente (como nos factos). Já as que só ocorrem no corpo da regra devem ser entendidas como quantificadas existencialmente (como nos objectivos).
Exercício: Estenda a base de conhecimento para exprimir outros graus de parentesco, como "irmão", "tio", etc.
Esta página apresenta algumas ideias para projectos práticos da disciplina de Lógica Computacional. Os alunos interessados em realizar um projecto devem contactar o docente para definir a atribuição respectiva.
Utilização de SMT Provers na verificação de software
O objectivo deste projecto é o de explorar um SMT Prover na verificação de software. Um SMT Prover é uma ferramenta que combina um verificador automático de fórmulas proposicionais com estratégias específicas para lidar com problemas de decisão em teorias específicas (como aritmética linear, manipulação de arrays, etc.). Essas teorias são particularmente orientadas para cobrir as obrigações de prova resultantes da verificação de programas.
Com este projecto pretende-se validar esse desígnio verificando as obrigações de prova resultantes de programas concretos com um SMT Prover. Como gerador de obrigações de prova sugere-se a utilização de WHY (http://why.lri.fr/index.en.html) e como SMT prover o YICES (http://yices.csl.sri.com/).
Codificação de ORBDDs em Haskell
A codificação de Binary Decision Diagrams (BDDs) pressupõe um controlo apertado sobre a gestão de memória e nos algoritmos utilizados na sua construção. Esse facto torna a sua codificação em Haskell um desafio interessante, obrigando à utilização de Monads para permitir aspectos imperativos na sua programação.
Este projecto pretende estudar a implementação de BDDs em Haskell. Tanto pode incidir sobre a codificação "de raiz" dessas estruturas como pode adoptar uma implementação pré-existente a analisar a sua implementação e o respectivo desempenho (e.g. comparando-a com uma biblioteca análoga desenvolvida em C).
Um dos algoritmos mais utilizados na verificação de fórmulas proposicionais é o Davis-Putnam(-Logemann-Loveland). Este projecto propõe-se estudar a implementação desse algoritmo em Haskell. Tal como no caso do projecto anterior, o âmbito deste projecto tanto pode incidir sobre a codificação de raiz do algoritmo, como no estudo de uma implementação existente.
O objectivo deste projecto é o de explorar o demonstrador de teoremas COQ para realizar provas simples. Sugere-se que os interessados realizem os exemplos do tutorial e de o surveyCoq in a Hurry.
Para aplicar os conceitos estudados, devem escolher um (ou mais) dos desafios apresentados. Note que o trabalho é individual e a escolha do desafio deve ser sempre combinada com o docente. Para a entrega devem apresentar um pacote com o conjunto das scripts desenvolvidas (quer dos exemplos realizados, quer do desafio escolhido), "abundantemente" comentadas (preferencialmente fazendo uso da ferramenta coqdoc para produzir um documento contendo essas scripts). As sessões de apresentação irão consistir na execução e discussão das referidas scripts.
29/05: Cálculo de sequentes em Lógica de Primeira Ordem.
22/05: Formas Prenex e Skolenização.
15/05: Tolerância de ponto: enterro da gata.
08/05: BDDs: redução e construção bottom-up.
24/04: Algoritmo Davis-Putman: exercícios de aplicação.
17/04: Algoritmo de resoluçao de Robinson: exemplos de aplicação.
27/03: Formas clausais: Fórmulas Normais Conjuntivas e Fórmulas Normais Disjuntivas. Resulução proposicional.
20/03: Avaliação de fórmulas proposicionais por aplicação do método tableaux. Formas normais negativas.
13/03: Demonstrações simples envolvendo indução sobre estrutura das fórmulas e derivações em sistemas de dedução. Construção de derivações no sistema de cálculo de sequentes.
06/03: Exercícios sobre noções elementares da lógica proposicionais: validade de fórmulas; consequência semântica; derivações em Dedução Natural.
20/03: Continuação da manipulação de listas. Exploração do mecanismo de backtracking.
13/03: Utilização de termos, introdução à manipulação de Listas.
06/03: Apresentação da linguagem Prolog.
27/02: Inscrição nos turnos.
Docente: Olga Pacheco
Aulas Teórico-Práticas
17/03: Prova de que a relação de consequência semântica é uma relação de dedução.
Representação no cálculo de sequentes das regras da dedução natural.
07/03: Exercícios sobre noções elementares da lógica proposicional: validade de fórmulas; consequência semântica; derivações em Dedução Natural.
28/02: Inscrição nos turnos.
Aulas Práticas
14/03: Utlilização de termos estruturados. Representação dos naturais baseada nos construtores 0 e sucessor
(definição dos predicados: menor, maior ou igual, soma e multiplicação).
Manipulação de listas em Prolog (definição dos predicados: cabeça, cauda, ultimo elemento, elemento na posição n, e membro).
07/03: Apresentação da linguagem Prolog.
Representação em Prolog de informação sobre árvores geneológicas (definição dos predicados: mãe, pai, irmão, tio, avô, avó, avô paterno, avó paterna, bisavô, bisavó,...).
06/03: Revisões de Lógica Proposicional: sintaxe das fórmulas; noção de modelo e validade; tautologias e contradições; teorias; consequência semântica.
11/03: Relações de dedução. Sistema de Dedução Natural (formulação clássica e com sequentes).
13/03: Propriedades do sistema de Dedução Natural. Apresentação do Cálculo de Sequentes.
27/03 (15:00): Demonstração do teorema de Correcção e Completude do sistema de Dedução Natural.
27/03: Continuação das demonstrações de Correcção e Completude do sistema de Dedução Natural.
01/04: Esboço das demonstrações da Correcção e Completude do Cálculo de Sequentes e da propriedade de Eliminação do Corte. Apresentação do método de Tableaux.
03/04: Formal Normal Negativa (FNN) e Formais Clausais (Forma Normal Disjuntiva (FND) e Forma Normal Conjuntiva (FNC)).
08/04: Método de resolução proposicional. Apresentação do algoritmo de Robinson e ilustração da aplicação.
10/04: Algoritmo de Davis-Putnam.
15/04: BDDs: motivação e definição; redução de árvores de decisão binárias.
17/04: Construção bottom-up de BDDs.
22/04: TESTE INTERMÉDIO.
24/04: Lógica de Primeira Ordem: Sintaxe e Semântica.
29/04: Formas Normais: Prenex; Herbrand e Skolen.
06/05: Modelos de Herbrand.
08/05: Não houve aula (impossibilidade do docente).
13/05: Tolerância de Ponto: Enterro da Gata.
15/05: Tolerância de Ponto: Enterro da Gata.
20/05: Cálculo de Sequentes para Lógica de Primeira Ordem.
27/05: Resolução Proposicional em Lógica de Primeira Ordem.
29/05: Unificação.
03/06: Resolução de Primeira Ordem.
05/06: Analogia de Curry Howard: motivação; normalização das provas.
10/06: Sistemas de Anotação de Provas para Dedução Natural. Lambda-Calculus com tipos.
12/06: Esclarecimento de dúvidas. Correcção do primeiro teste.
TP1
Aulas Teórico-Práticas (3ª 10:00-11:00)
26/02: Não houve aula.
04/03: Não houve aula.
11/03: Exercícios sobre validade e consequência semântica.
01/04: Exercícios sobre relações de dedução. Construção de árvores em Dedução Natural.
08/04: Exercícios sobre construção de derivações no Cálculo de Sequentes.
15/04: Exercícios sobre Formas Clausais e Resolução Proposicional.
22/04: TESTE INTERMÉDIO.
29/04: Exercícios spbre método Davis Putnam .
06/05: Exercícios sobre validade em lógica de primeira ordem.
13/05: Tolerância de Ponto: Enterro da Gata.
20/05: Exercícios sobre formas normais (prenex, skolen e herbrand)
27/05: Exercícios sobre cálculo de sequentes para lógica de predicados.
TWiki's Education/LC webThe Education/LC web of TWiki. TWiki is a Web-Based Collaboration Platform for the Enterprise.http://wiki.di.uminho.pt/twiki/bin/view/Education/LCCopyright 2020 by contributing authors2020-10-30T14:39:17ZWebStatisticshttp://wiki.di.uminho.pt/twiki/bin/view/Education/LC/WebStatistics2020-10-30T14:39:17ZStatistics for Education/LC Web Month: Topic views: Topic saves: File uploads: Most popular topic views: Top contributors for topic save ... (last changed by TWikiGuest)TWikiGuestWebHomehttp://wiki.di.uminho.pt/twiki/bin/view/Education/LC/WebHome2010-02-18T13:06:08ZEsta disciplina tem por objectivo aprofundar a relação existente entre lógica formal e a computação. Esta relação pode assumir diferentes formas, dependendo da perspectiva ... (last changed by OlgaPacheco)OlgaPachecoMaterialApoiohttp://wiki.di.uminho.pt/twiki/bin/view/Education/LC/MaterialApoio2010-02-18T13:00:50ZSlides Lógica Proposicional I Cálculo de Sequentes (versão: 11/06/2008) Lógica Proposicional II Método Tableaux , Formas Clausais, Resolução (versão: 11 ... (last changed by OlgaPacheco)OlgaPachecoAvisos0809http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Avisos08092009-07-22T17:28:03Z22/07/2009: Disponíveis notas da época de recurso. 07/05/2009: Disponível enunciado do projecto prático. 06/03/2009: Já disponível o guião da primeira aula pr ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeida0809http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/08092009-07-22T17:27:12ZLógica Computacional (8504N2) em Matemática e Ciências de Computação 2º Ano 2º Semestre Ano lectivo 2008/2009 Equipa Docente José Carlos Bacelar ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaProgDetalhado0809http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/ProgDetalhado08092009-06-18T22:10:46ZPrograma detalhado do ano lectivo 2008/2009 Lógica Proposicional Sintaxe e Semântica Sistemas Dedutivos Dedução Natural ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaPrograma0809http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Programa08092009-06-18T22:10:01ZPrograma Resumido Componente Teórica Lógica Proposicional Sintaxe e Semântica Sistemas Dedutivos Métodos de Verificação Aspectos ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaPraticas0809http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Praticas08092009-05-29T23:07:19ZAulas Práticas #Aula10P Aula 10: Predicados de Segunda Ordem e outros predicados primitivos disponibilizados pelo Prolog Predicados de segunda ordem Existem meta ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaProjectos0809http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Projectos08092009-05-08T02:24:38ZProjecto O objectivo deste projecto é o de explorar o demonstrador de teoremas COQ para realizar provas simples. Sugere se que os interessados realizem os exemplos ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaTopicos0809http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Topicos08092009-02-12T17:21:40ZCalendário (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaCalendariohttp://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Calendario2009-02-12T17:16:45Z (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaSumarios0708http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Sumarios07082009-02-01T18:25:15ZSumários Aulas Teóricas (3ª 14:00 15:00; 5ª 16:00 17:00) 26/02: Não houve aula. 28/02: Não houve aula. 04/03: Aula de substituição em 27/03 , às 15:00. 06 ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaSumarios0809http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Sumarios08092009-02-01T18:23:00ZSumários Aulas Teóricas (3ª 14:00 15:00; 5ª 16:00 17:00) TP1 Aulas Teórico Práticas (2ª 16:00 17:00) Aulas Práticas (2ª 17:00 19:00) TP2 Aulas Teórico Pr ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeida0708http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/07082009-02-01T18:16:25ZLógica Computacional (8504N2) em Matemática e Ciências de Computação 2º Ano 2º Semestre Ano lectivo 2007/2008 Equipa Docente José Carlos Bacelar ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaWebPreferenceshttp://wiki.di.uminho.pt/twiki/bin/view/Education/LC/WebPreferences2009-02-01T18:15:29ZEducation/LC Web Preferences The following settings are web preferences of the Education/LC web. These preferences overwrite the site level preferences in ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaMFES0809http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/MFES08092008-12-05T23:17:24ZAnálise, Modelação e Teste de Software MFES Mestrado de Informática 13/11/2008 "Design by Contract and Java Modeling Language": apresentação do conceito e clausulas ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeida
Esta disciplina tem por objectivo aprofundar a relação existente entre lógica formal e a computação. Esta relação pode assumir diferentes formas, dependendo da perspectiva ...
22/07/2009: Disponíveis notas da época de recurso. 07/05/2009: Disponível enunciado do projecto prático. 06/03/2009: Já disponível o guião da primeira aula pr ...
Aulas Práticas #Aula10P Aula 10: Predicados de Segunda Ordem e outros predicados primitivos disponibilizados pelo Prolog Predicados de segunda ordem Existem meta ...
Projecto O objectivo deste projecto é o de explorar o demonstrador de teoremas COQ para realizar provas simples. Sugere se que os interessados realizem os exemplos ...
Education/LC Web Preferences The following settings are web preferences of the Education/LC web. These preferences overwrite the site level preferences in ...
Análise, Modelação e Teste de Software MFES Mestrado de Informática 13/11/2008 "Design by Contract and Java Modeling Language": apresentação do conceito e clausulas ...
24/09: Já estão disponíveis as notas da época de especial. 28/07: Já estão disponíveis as notas da época de recurso. 02/07: Já estão disponíveis as notas do 2 ...
Aulas Práticas #Aula9P Aula 9: Implementação do algoritmo Davis Putnam em Prolog. Pretende se definir um programa que permita verificar se uma dada fórmula é uma ...
Propostas de Projectos Práticos 2007/2008 Esta página apresenta algumas ideias para projectos práticos da disciplina de Lógica Computacional. Os alunos interessados ...
Elementos Lógicos da Programação II (702752) Licenciatura de Matemática e Ciências da Computação 2º Ano 2º Semestre Ano lectivo 2004/2005 Programa Programa ...
31/07 Já estão disponíveis as notas referentes à Época de Recurso. (aqui) 17/07 Já estão disponíveis as notas referentes à Época Normal. (aqui) 20/06 Foram disponibilizados ...
Sumários Docente: José Carlos Bacelar Aulas Teóricas 08/06: Esclarecimento de dúvidas. 05/06: Referência às propriedades básicas do Lambda calculus com tipos ...
Aulas Práticas #Aula8P Aula 8: Predicados de Segunda Ordem Existem meta predicados que permitem coleccionar todas as soluções para um dado objectivo de prova (ver ...
A resolução da ficha de avaliação prática 3 (enunciado da ficha está na página) é para ser entregue na aula prática de 2 de Junho . MariaJoaoFrade 25 May 2006 ...
Esta disciplina tem por objectivo aprofundar a relação existente entre lógica formal e a computação. Esta relação pode assumir diferentes formas, dependendo da perspectiva sobre a qual é analisada:
Uma primeira perspectiva consiste em eleger o processo de verificar a validade de fórmulas lógicas como problema computacional - por outras palavras, procuram-se construir programas que estabeleçam a validade de fórmulas lógicas. Tal como iremos ter oportunidade de estudar neste curso, este problema é difícil, mesmo para lógicas muito simples (e.g. lógica proposicional).
Uma segunda perspectiva consiste em adoptar a noção de dedução lógica como motor de cálculo de uma linguagem de programação. Uma destas linguagens é o Prolog, que será estudada neste curso.
Por último, iremos também abordar o que é habitualmente designado por Analogia de Curry-Howard: esta analogia permite-nos estabelecer um paralelo entre sistemas lógicos e linguagens de programação funcionais, constituindo assim uma fundamentação lógica para essas linguagens.
A resolução da ficha de avaliação prática 3 (enunciado da ficha está na página) é para ser entregue na aula prática de 2 de Junho . MariaJoaoFrade 25 May 2006 ...
31/07 Já estão disponíveis as notas referentes à Época de Recurso. (aqui) 17/07 Já estão disponíveis as notas referentes à Época Normal. (aqui) 20/06 Foram disponibilizados ...
24/09: Já estão disponíveis as notas da época de especial. 28/07: Já estão disponíveis as notas da época de recurso. 02/07: Já estão disponíveis as notas do 2 ...
22/07/2009: Disponíveis notas da época de recurso. 07/05/2009: Disponível enunciado do projecto prático. 06/03/2009: Já disponível o guião da primeira aula pr ...
Elementos Lógicos da Programação II (702752) Licenciatura de Matemática e Ciências da Computação 2º Ano 2º Semestre Ano lectivo 2004/2005 Programa Programa ...
Análise, Modelação e Teste de Software MFES Mestrado de Informática 13/11/2008 "Design by Contract and Java Modeling Language": apresentação do conceito e clausulas ...
Aulas Práticas #Aula8P Aula 8: Predicados de Segunda Ordem Existem meta predicados que permitem coleccionar todas as soluções para um dado objectivo de prova (ver ...
Aulas Práticas #Aula9P Aula 9: Implementação do algoritmo Davis Putnam em Prolog. Pretende se definir um programa que permita verificar se uma dada fórmula é uma ...
Aulas Práticas #Aula10P Aula 10: Predicados de Segunda Ordem e outros predicados primitivos disponibilizados pelo Prolog Predicados de segunda ordem Existem meta ...
Propostas de Projectos Práticos 2007/2008 Esta página apresenta algumas ideias para projectos práticos da disciplina de Lógica Computacional. Os alunos interessados ...
Projecto O objectivo deste projecto é o de explorar o demonstrador de teoremas COQ para realizar provas simples. Sugere se que os interessados realizem os exemplos ...
Sumários Docente: José Carlos Bacelar Aulas Teóricas 08/06: Esclarecimento de dúvidas. 05/06: Referência às propriedades básicas do Lambda calculus com tipos ...
Esta disciplina tem por objectivo aprofundar a relação existente entre lógica formal e a computação. Esta relação pode assumir diferentes formas, dependendo da perspectiva ...
Education/LC Web Preferences The following settings are web preferences of the Education/LC web. These preferences overwrite the site level preferences in ...
This is a subscription service to be automatically notified by e-mail when topics change in this Education/LC web. This is a convenient service, so you do not have to come back and check all the time if something has changed. To subscribe, please add a bullet with your WikiName in alphabetical order to this list:
Each TWiki web has an automatic e-mail notification service that sends you an e-mail with links to all of the topics modified since the last alert.
Users subscribe to email notifications using their WikiName or an alternative email address, and can specify the webs/topics they wish to track using one of these bullet list formats:
three spaces * [ webname . ] wikiName - SMTP mail address three spaces * [ webName . ] wikiName three spaces * SMTP mail address three spaces * SMTP mail address : topics three spaces * [ webname . ] wikiName : topics
In the above examples, topics is a space-separated list of topic names. The user may further customize the specific content they will receive using the following formats:
Specify topics without a Web. prefix
Topics must exist in this web.
Topics may be specified using * wildcards
Each topic may optionally be preceded by a '+' or '-' sign. The '+' sign means "subscribe to this topic" (the same as not putting anything). The '-' sign means "unsubscribe" or "don't send notifications regarding this topic". This allows users to elect to filter out certain topics (and their children, to an arbitrary depth). Topic filters ('-') take precedence over topic includes ('+').
Each topic may optionally be followed by an integer in parentheses, indicating the depth of the tree of children below that topic. Changes in all these children will be detected and reported along with changes to the topic itself. Note This uses the TWiki "Topic parent" feature.
Each topic may optionally be immediately followed by an exclamation mark ! or a question mark ? with no intervening spaces, indicating that the topic (and children if there is a tree depth specifier as well) should be mailed out as complete topics instead of change summaries. ! causes the topic to be mailed every time even if there have been no changes, ? will mail the topic only if there have been changes to it. This only makes sense for subscriptions.
For example:
Subscribe Daisy to all changes to topics in this web.
* daisy.cutter@flowers.com
Subscribe Daisy to all changes in all webs that start with Web.
* daisy.cutter@flowers.com: Web*
Subscribe Daisy to changes to topics starting with Petal, and their immediate children, WeedKillers and children to a depth of 3, and all topics that match start with Pretty and end with Flowers e.g. PrettyPinkFlowers
Subscribe Daisy to the full content of NewsLetter whenever it has changed
* daisy@flowers.com: TWiki.NewsLetter?
Subscribe buttercup to NewsLetter and its immediate children, even if it hasn't changed.
* buttercup@flowers.com: TWiki.NewsLetter! (1)
Subscribe GardenGroup (which includes Petunia) to all changed topics under AllnewsLetters to a depth of 3. Then unsubscribe Petunia from the ManureNewsLetter, which she would normally get as a member of GardenGroup? :
A user may be listed many times in the WebNotify topic. Where a user has several lines in WebNotify that all match the same topic, they will only be notified about changes that topic once (though they will still receive individual mails for news topics).
If a TWiki group is listed for notification, the group will be recursively expanded to the e-mail addresses of all members.
Tip: List names in alphabetical order to make it easier to find the names.
Note for System Administrators: Notification is supported by an add-on to the TWiki kernel called the MailerContrib. See the MailerContrib topic for details of how to set up this service.
Note: If you prefer a news feed, point your reader to WebRss (for RSS 1.0 feeds) or WebAtom (for ATOM 1.0 feeds). Learn more at WebRssBase and WebAtomBase, respectively.
These settings override the defaults for this web only. See full list of defaults with explanation. Many of the settings below are commented out. Remove the # sign to enable a local customisation.
Web-specific background color: (Pick a lighter one of the StandardColors).
Set WEBBGCOLOR = #D0D0D0
Note: This setting is automatically configured when you create a web
Image, URL and alternate tooltip text of web's logo. Note: Don't add your own local logos to the TWikiLogos topic; create your own logos topic instead.
List this web in the SiteMap. If you want the web listed, then set SITEMAPLIST to on, do not set NOSEARCHALL, and add the "what" and "use to..." description for the site map. Use links that include the name of the web, i.e. Education/LC.Topic links. Note: Unlike other variables, the setting of SITEMAPLIST is not inherited from parent webs. It has to be set in every web that is to be listed in the SiteMap
Set SITEMAPLIST = on
Set SITEMAPWHAT =
Set SITEMAPUSETO = Licenciatura em Ciências da Computação - 2º ano
Note: Above settings are automatically configured when you create a web
Exclude web from a web="all" search: (Set to on for hidden webs).
#Set NOSEARCHALL = on
Note: This setting is automatically configured when you create a web
Prevent automatic linking of WikiWords and acronyms (if set to on); link WikiWords (if empty); can be overwritten by web preferences:
#Set NOAUTOLINK =
Note: You can still use the [[...][...]] syntax to link topics if you disabled WikiWord linking. The <noautolink> ... </noautolink> syntax can be used to prevents links within a block of text.
Default template for new topics for this web:
WebTopicEditTemplate? : Default template for new topics in this web. (Site-level is used if topic does not exist)
Comma separated list of forms that can be attached to topics in this web. See TWikiForms for more information.
Set WEBFORMS =
Users or groups who are not / are allowed to view / change / rename topics in the Education/LC web: (See TWikiAccessControl). Remove the # to enable any of these settings. Remember that an empty setting is a valid setting; setting DENYWEBVIEW to nothing means that anyone can view the web.
Preferences are used as TWikiVariables by enclosing the name in percent signs. Example:
When you write variable %WEBBGCOLOR% , it gets expanded to #D0D0D0
The sequential order of the preference settings is significant. Define preferences that use other preferences first, i.e. set WEBCOPYRIGHT before WIKIWEBMASTER since %WEBCOPYRIGHT% uses the %WIKIWEBMASTER% variable.
You can introduce your own preferences variables and use them in your topics and templates.
TWiki search results for \.*
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC
The Education/LC web of TWiki. TWiki is a Web-Based Collaboration Platform for the Enterprise.en-usCopyright 2020 by contributing authorsTWiki Administrator [webmaster@di.uminho.pt]The contributing authors of TWikiTWikiDIUM.Education/LC
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC
/twiki/pub/Main/LocalLogos/um_eengP.jpgWebHome
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/WebHome
Esta disciplina tem por objectivo aprofundar a relação existente entre lógica formal e a computação. Esta relação pode assumir diferentes formas, dependendo da perspectiva ... (last changed by OlgaPacheco)2010-02-18T13:06:08ZOlgaPachecoMaterialApoio
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/MaterialApoio
Slides Lógica Proposicional I Cálculo de Sequentes (versão: 11/06/2008) Lógica Proposicional II Método Tableaux , Formas Clausais, Resolução (versão: 11 ... (last changed by OlgaPacheco)2010-02-18T13:00:50ZOlgaPachecoAvisos0809
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Avisos0809
22/07/2009: Disponíveis notas da época de recurso. 07/05/2009: Disponível enunciado do projecto prático. 06/03/2009: Já disponível o guião da primeira aula pr ... (last changed by JoseBacelarAlmeida)2009-07-22T17:28:03ZJoseBacelarAlmeida0809
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/0809
Lógica Computacional (8504N2) em Matemática e Ciências de Computação 2º Ano 2º Semestre Ano lectivo 2008/2009 Equipa Docente José Carlos Bacelar ... (last changed by JoseBacelarAlmeida)2009-07-22T17:27:12ZJoseBacelarAlmeidaProgDetalhado0809
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/ProgDetalhado0809
Programa detalhado do ano lectivo 2008/2009 Lógica Proposicional Sintaxe e Semântica Sistemas Dedutivos Dedução Natural ... (last changed by JoseBacelarAlmeida)2009-06-18T22:10:46ZJoseBacelarAlmeidaPrograma0809
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Programa0809
Programa Resumido Componente Teórica Lógica Proposicional Sintaxe e Semântica Sistemas Dedutivos Métodos de Verificação Aspectos ... (last changed by JoseBacelarAlmeida)2009-06-18T22:10:01ZJoseBacelarAlmeidaPraticas0809
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Praticas0809
Aulas Práticas #Aula10P Aula 10: Predicados de Segunda Ordem e outros predicados primitivos disponibilizados pelo Prolog Predicados de segunda ordem Existem meta ... (last changed by JoseBacelarAlmeida)2009-05-29T23:07:19ZJoseBacelarAlmeidaProjectos0809
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Projectos0809
Projecto O objectivo deste projecto é o de explorar o demonstrador de teoremas COQ para realizar provas simples. Sugere se que os interessados realizem os exemplos ... (last changed by JoseBacelarAlmeida)2009-05-08T02:24:38ZJoseBacelarAlmeidaTopicos0809
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Topicos0809
Calendário (last changed by JoseBacelarAlmeida)2009-02-12T17:21:40ZJoseBacelarAlmeidaCalendario
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Calendario
(last changed by JoseBacelarAlmeida)2009-02-12T17:16:45ZJoseBacelarAlmeidaSumarios0708
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Sumarios0708
Sumários Aulas Teóricas (3ª 14:00 15:00; 5ª 16:00 17:00) 26/02: Não houve aula. 28/02: Não houve aula. 04/03: Aula de substituição em 27/03 , às 15:00. 06 ... (last changed by JoseBacelarAlmeida)2009-02-01T18:25:15ZJoseBacelarAlmeidaSumarios0809
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Sumarios0809
Sumários Aulas Teóricas (3ª 14:00 15:00; 5ª 16:00 17:00) TP1 Aulas Teórico Práticas (2ª 16:00 17:00) Aulas Práticas (2ª 17:00 19:00) TP2 Aulas Teórico Pr ... (last changed by JoseBacelarAlmeida)2009-02-01T18:23:00ZJoseBacelarAlmeida0708
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/0708
Lógica Computacional (8504N2) em Matemática e Ciências de Computação 2º Ano 2º Semestre Ano lectivo 2007/2008 Equipa Docente José Carlos Bacelar ... (last changed by JoseBacelarAlmeida)2009-02-01T18:16:25ZJoseBacelarAlmeidaWebPreferences
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/WebPreferences
Education/LC Web Preferences The following settings are web preferences of the Education/LC web. These preferences overwrite the site level preferences in ... (last changed by JoseBacelarAlmeida)2009-02-01T18:15:29ZJoseBacelarAlmeidaMFES0809
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/MFES0809
Análise, Modelação e Teste de Software MFES Mestrado de Informática 13/11/2008 "Design by Contract and Java Modeling Language": apresentação do conceito e clausulas ... (last changed by JoseBacelarAlmeida)2008-12-05T23:17:24ZJoseBacelarAlmeidaAvisos0708
http://wiki.di.uminho.pt/twiki/bin/view/Education/LC/Avisos0708
24/09: Já estão disponíveis as notas da época de especial. 28/07: Já estão disponíveis as notas da época de recurso. 02/07: Já estão disponíveis as notas do 2 ... (last changed by JoseBacelarAlmeida)2008-09-27T11:17:47ZJoseBacelarAlmeida
Tip: List names in alphabetical order to make it easier to find the names.
Rename, move or delete this web: 
If you already know the name of the topic, enter the name of the topic into the 
List topics that start with the letter: 
Once you have created the topic, consider adding links in related topics to the new topic so that there are more ways people can discover it.
Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.