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
15/07/2014
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
15/07/2014
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 xV então x  T();
2.
Se cC então c  T();
3.
Se fFj e se t1,...tj  T() então f(t1,...tj ) T().
4
Prof. Celso A A Kaestner
15/07/2014
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 xV então x() e x()  Fbf().
5
Prof. Celso A A Kaestner
15/07/2014
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
15/07/2014
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
15/07/2014
Lógica para Computação (IF61B)
Lógica Predicativa

Exemplos:
8
Prof. Celso A A Kaestner
15/07/2014
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
15/07/2014
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 fFj 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
15/07/2014
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 fFj , t1,..., tj são termos e t=f(t1,..., tj) então
tA() []= vA() (fj)(t1A()[],..., tjA()[]).
11
Prof. Celso A A Kaestner
15/07/2014
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
15/07/2014
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
15/07/2014
Lógica para Computação (IF61B)
Lógica Predicativa

Exemplos
14
Prof. Celso A A Kaestner
15/07/2014
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
15/07/2014
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)),
yVLIVRES () 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
15/07/2014
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, zVLIVRES () 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
15/07/2014
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
15/07/2014
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
15/07/2014
Lógica para Computação (IF61B)
Lógica Predicativa

Método da Dedução Natural...
20
Prof. Celso A A Kaestner
15/07/2014
Download

Lógica Predicativa - DAINF