Teorema de herbrand
481 palavras
2 páginas
INF2217 – Lógica e EspecificaçãoNotação Clausal e Teorema de Herbrand
Marco A. Casanova
6/8/2008
(c) MAC / KKB - PUC-Rio
1
Referências
• [CGF] Seções 3.2, 3.3, 3.4 e 3.6 • [BL] Seções 4.2 e 4.3
6/8/2008
(c) MAC / KKB - PUC-Rio
2
Representação Clausal de Fórmulas
• Algoritmo de Representação Clausal:
6/8/2008
(c) MAC / KKB - PUC-Rio
3
Representação Clausal de Fórmulas
• Algoritmo de Representação Clausal:
6/8/2008
(c) MAC / KKB - PUC-Rio
4
Representação Clausal de Fórmulas
• Algoritmo de Representação Clausal:
6/8/2008
(c) MAC / KKB - PUC-Rio
5
Representação Clausal de Fórmulas
• Algoritmo de Representação Clausal:
6/8/2008
(c) MAC / KKB - PUC-Rio
6
Representação Clausal de Fórmulas
• Algoritmo de Representação Clausal:
6/8/2008
(c) MAC / KKB - PUC-Rio
7
Representação Clausal de Fórmulas
• Algoritmo de Representação Clausal:
6/8/2008
(c) MAC / KKB - PUC-Rio
8
Representação Clausal de Fórmulas
• Algoritmo de Representação Clausal:
6/8/2008
(c) MAC / KKB - PUC-Rio
9
Representação Clausal de Fórmulas
• Algoritmo de Representação Clausal:
6/8/2008
(c) MAC / KKB - PUC-Rio
10
Representação Clausal de Fórmulas
6/8/2008
(c) MAC / KKB - PUC-Rio
11
Representação Clausal de Fórmulas
• Exemplo:
6/8/2008
(c) MAC / KKB - PUC-Rio
12
Representação Clausal de Fórmulas
• Exemplo (cont.):
6/8/2008
(c) MAC / KKB - PUC-Rio
13
Representação Clausal de Fórmulas
• Exemplo (cont.):
6/8/2008
(c) MAC / KKB - PUC-Rio
14
Representação Clausal de Fórmulas
• Exemplo (cont.):
6/8/2008
(c) MAC / KKB - PUC-Rio
15
Representação Clausal de Fórmulas
• Exemplo (cont.):
6/8/2008
(c) MAC / KKB - PUC-Rio
16
Teorema de Herbrand
6/8/2008
(c) MAC / KKB - PUC-Rio
17
Teorema de Herbrand
6/8/2008
(c) MAC / KKB - PUC-Rio
18
Teorema de Herbrand
6/8/2008
(c) MAC / KKB -