Lógica para Computação Prof. Celso Antônio Alves Kaestner, Dr. Eng. celsokaestner (at) utfpr (dot) edu (dot) br Lógica para Computação (IF61B) Lógica Predicativa A Lógica Predicativa (ou lógica de 1ª ordem) é uma extensão da lógica proposicional que aumenta sua expressividade, permitindo que se façam afirmações sobre propriedades – ou predicados – inerentes a conjuntos de elementos individuais; Tipicamente as fórmulas envolvem os quantificadores “para todo” () e “existe” (); Uma fórmula típica é: x(homem(x)→mortal(x)). Obs.: para representar o mesmo em Lógica Proposicional seria necessário utilizar uma fórmula para cada indivíduo, por exemplo: (homem_joão → mortal_joão), (homem_josé → mortal_josé), etc. 2 Prof. Celso A A Kaestner 05/11/2015 Lógica para Computação (IF61B) Lógica Predicativa A linguagem (sintaxe) da Lógica Predicativa LPRED é mais complexa que a da Lógica Proposicional; Para a definição de LPRED necessita-se de: 1. Um conjunto de predicados: Ri = { ri1, ri2,... rin,...} onde o sobrescrito i indica a aridade do predicado (o seu nº de argumentos); 2. Um conjunto de constantes: C = {c1,c2, ...}; 3. Um conjunto de funções: Fi = { fi1, fi2,... fin,...} onde o sobrescrito i também indica a aridade da função; 4. Um conjunto de variáveis: V = {x1,x2, ...}. 3 Prof. Celso A A Kaestner 05/11/2015 Lógica para Computação (IF61B) Lógica Predicativa A assinatura de LPRED é a uma tupla do tipo = [R1,R2, ...RM,C,F1,F2,...FN] onde N e M são números naturais conhecidos. O conjunto dos termos de LPRED é T() definido recursivamente por: 1. Se xV então x T(); 2. Se cC então c T(); 3. Se fFj e se t1,...tj T() então f(t1,...tj ) T(). 4 Prof. Celso A A Kaestner 05/11/2015 Lógica para Computação (IF61B) Lógica Predicativa O conjunto das fórmulas (fbf) de LPRED é Fbf() definido recursivamente como sendo o menor conjunto que atenda ao seguinte: 1. Se t1,...tj T() e se rj Rj então rj(t1,...tj) Fbf(); 2. Se t1, t2 T() então t1= t2 Fbf(); Estas fbf são chamadas de fórmulas atômicas; 3. Se , Fbf() então , , , → Fbf(); 4. Se Fbf() e se xV então x() e x() Fbf(). 5 Prof. Celso A A Kaestner 05/11/2015 Lógica para Computação (IF61B) Lógica Predicativa O conjunto das variáveis livres VLIVRES () em uma fórmula é definido por: 1. Se = rj(t1,...tj) com rj Rj e os ti T() então todas as variáveis em pertencem a VLIVRES (); 2. Se = (t1=t2) com os ti T() então todas as variáveis em pertencem a VLIVRES (); 3. Se = então VLIVRES ()= VLIVRES (); 4. Se = , , ou → então VLIVRES ()= VLIVRES () VLIVRES (); 5. Se = x() ou x() então VLIVRES ()= VLIVRES () – {x}. Exemplo: Se = x (r(x) q(y) → z (s(z,y))) então VLIVRES () = { y }. 6 Prof. Celso A A Kaestner 05/11/2015 Lógica para Computação (IF61B) Lógica Predicativa Uma fórmula tal que VLIVRES () = (sem variáveis livres) é denominada uma sentença. Uma subfórmula de uma fórmula é uma subseqüência dos símbolos de que também pertence a Fbf(). Exemplo: se = x (r(x) q(y) → z (s(z,y))) então r(x) q(y) → z (s(z,y)) , r(x) q(y), z (s(z,y)), r(x) e q(y) são subfórmulas de . 7 Prof. Celso A A Kaestner 05/11/2015 Lógica para Computação (IF61B) Lógica Predicativa Exemplos: 8 Prof. Celso A A Kaestner 05/11/2015 Lógica para Computação (IF61B) Lógica Predicativa A semântica da Lógica Predicativa é definida sobre um par A()=[A, vA()] denominado sistema algébrico da assinatura , tal que: 1. A é um conjunto denominado domínio (ou portador) do sistema algébrico; 2. vA() é uma interpretação, que mapeia os elementos dos conjuntos em em relações sobre A (para os predicados), em funções sobre A (para as funções) e em elementos de A (para as constantes). 9 Prof. Celso A A Kaestner 05/11/2015 Lógica para Computação (IF61B) Lógica Predicativa Desta forma para uma interpretação vA() tem-se: 1. Se rj Rj então vA() (rj) Aj = A A ... A (j vezes); 2. Se fFj então existe uma função vA() (fj): Aj →A; 3. Se c C então vA() (c) A; 4. Para um conjunto de variáveis X V existe ainda uma função : X → A denominada interpretação das variáveis X em A . 10 Prof. Celso A A Kaestner 05/11/2015 Lógica para Computação (IF61B) Lógica Predicativa O valor de um termo t T () em um sistema algébrico A() e para uma interpretação de variáveis é definido indutivamente por: 1. Se t = x X então tA() [] = (x); 2. Se t = c C então tA() [] = vA() (c); 3. Se fFj , t1,..., tj são termos e t=f(t1,..., tj) então tA() []= vA() (fj)(t1A()[],..., tjA()[]). 11 Prof. Celso A A Kaestner 05/11/2015 Lógica para Computação (IF61B) Lógica Predicativa Finalmente é possível se definir quando uma fórmula é verdadeira para um sistema algébrico A() e uma interpretação de variáveis ; Denota-se por A() |= []; 1. Se = rj(t1,...tj) Fbf() então A() |= [] é equivalente a [t1A()[],..., tjA()[]] vA() (rj); 2. Se = (t1=t2) com t1, t2 T() então A() |= [] é equivalente a t1A()[] = t2A()[]; 3. Se = e Fbf() então A() |= [] se e somente se não for verdade que A() |= []; 12 Prof. Celso A A Kaestner 05/11/2015 Lógica para Computação (IF61B) Lógica Predicativa 4. Se = , com , Fbf() então A() |= [] se e somente se A() |= [] e A() |= []; 5. Se = , com , Fbf() então A() |= [] se e somente se A() |= [] ou A() |= []; 6. Se = →, com , Fbf() então A() |= [] se e somente se quando A() |= [] necessariamente também ocorre A() |= []; 7. Se = x() com Fbf() então A() |= [] se e somente se existir pelo menos uma interpretação de variáveis : X → A que, restrita às variáveis de , seja tal que A() |= []; 8. Se = x() com Fbf() então A() |= [] se e somente se para todas as interpretações de variáveis : X → A , quando restritas às variáveis de , sejam tais que A() |= []. 13 Prof. Celso A A Kaestner 05/11/2015 Lógica para Computação (IF61B) Lógica Predicativa Exemplos 14 Prof. Celso A A Kaestner 05/11/2015 Lógica para Computação (IF61B) Lógica Predicativa Uma teoria em LPRED é um conjunto de sentenças; Um sistema algébrico A() é um modelo para uma teoria se A() |= para toda ; Se tiver ao menos um modelo diz-se que é satisfazível; Se não tiver modelos é dita insatisfazível. 15 Prof. Celso A A Kaestner 05/11/2015 Lógica para Computação (IF61B) Lógica Predicativa Substituição de variáveis: • Seja uma fórmula, x VLIVRES () uma variável livre em e t T() um termo; • Neste caso a variável x pode ser substituída pelo termo t em , gerando uma nova fórmula [x:=t]; • Exemplo: se = x(r(x) →s(x,y)), yVLIVRES () e t=f(a,z) então [y:=f(a,z)] = x(r(x) →s(x,f(a,z))). 16 Prof. Celso A A Kaestner 05/11/2015 Lógica para Computação (IF61B) Lógica Predicativa • Intuitivamente uma substituição gera um “caso particular” de uma fórmula; • As substituições só podem ser feitas sobre as variáveis livres de , e de forma a não introduzir restrições na fórmula gerada que já não estivessem presentes na fórmula original; • Várias substituições podem ser feitas simultaneamente, desde que não introduzam restrições. • Exemplo: Se = x(r(x) →s(x,y) r(z)) y, zVLIVRES () e t1=f(a,w), t2=b então [y:=f(a,w), z:=b]=x(r(x)→s(x,f(a,z))r(b))) 17 Prof. Celso A A Kaestner 05/11/2015 Lógica para Computação (IF61B) Lógica Predicativa Sistemas Dedutivos em Lógica Predicativa: 1. Método axiomático: ver item 4.5 pg. 128; 2. Dedução natural: ver item 4.4 pg. 122, e também a ferramenta JAPE; 3. Método dos tableaux analíticos: ver item 5.6 pg. 147. 18 Prof. Celso A A Kaestner 05/11/2015 Lógica para Computação (IF61B) Lógica Predicativa Exemplo do método dos tableaux analíticos: 1. x(r(x) → s(x)) |- x r(x) → x s(x) 2. T x(r(x) → s(x)) de 1 3. F x r(x) → x s(x) de 1 4. T x r(x) de 3 5. F x s(x) de 3 6. F s(a) de 5 7. T r(a) de 4 8. T r(a) → s(a) de 2 9. F r(a) de 8 X (7,9) T s(a) X (6,9) 19 Prof. Celso A A Kaestner 05/11/2015 Lógica para Computação (IF61B) Lógica Predicativa Método da Dedução Natural... 20 Prof. Celso A A Kaestner 05/11/2015