Revisão: Árvores de Análise, Substituição e Dedução Natural - Exercícios de Linguagem Formal

Revisao A rvores de Analise Substituicao Deducao Natural Exercıcios Linguagem Formal Termo Qualquer variavel e um termo Uma constante e um termo Um sımbolo funcional eum termo t x c ft1 tn Revisao A rvores de Analise Substituicao Deducao Natural Exercıcios Linguagem Formal For mulas Um predicado e uma formula Se φ e uma formula φ e uma formula Se φ e ψ sao formulas φψ φψ φ ψ euma formula Se φ euma formula xφ e xφtambem sao formulas φ Pt1 tn φ φφ φφ φ φ xφ xφ Revisao A rvores de Analise Substituicao Deducao Natural Exercıcios A rvores de Analise x e x formam nos e possuem apenas um filho Predicados Pt1 t2 tn tem P como noe P tem n filhos Revisao A rvores de Analise Substituicao Deducao Natural Exercıcios A rvores de Analise Construa as seguintes ar vores de analise xPx Qx Sx y xPx Qx Px Qy Revisao A rvores de Analise Substituicao Deducao Natural Exercıcios A rvores de Analise Variaveis livres Variaveis presas Revisao A rvores de Analise Substituicao Deducao Natural Exercıcios Substituicao Dada uma variavel x um termo t e uma formula φ definimos φtx para a formula obtida de φ substituindose cada ocorreˆncia livre da variavel x em φ Revisao A rvores de Analise Substituicao Deducao Natural Exercıcios Substituicao Exemplos φfx yx sendo φ xPx Qx Sx y Revisao A rvores de Analise Substituicao Deducao Natural Exercıcios Substituicao Exemplos φfx yx sendo φ xPx Qx Sx y φfx yx sendo φ xPx Qx Px Qy Revisao A rvores de Analise Substituicao Deducao Natural Exercıcios Substituicao termo livre termo preso Revisao A rvores de Analise Substituicao Deducao Natural Exercıcios Substituicao termo livre termo preso Definicao Dados um termo t uma variavel x e uma formula φ dizemos t e livre para x em φ se nenhuma folha livre de x ocorre no escopo de y y para qualquer variavel y ocorrendo em t Revisao A rvores de Analise Substituicao Deducao Natural Exercıcios Exercıcio Seja φ a formula xPy z yQyx Py z Construa a arvore de analise de φ Identifique todas as variaveis livres e presas Existe alguma variavel em φ que ocorre livre e presa Qual Considere os termos w fx e gy z compute φwx φfxx e φgy zx Quais dos termos w fx e gy z sao livres para x em φ Revisao A rvores de Analise Substituicao Deducao Natural Exercıcios Deducao Natural Logica de Predicados Revisao A rvores de Analise Substituicao Deducao Natural Exercıcios Regras para o Quantificador Universal Eliminacao do Quantificador Universal m xφx p φx0x e m se φeverdade para todos os x φ everdade para um x0 especıfico Revisao A rvores de Analise Substituicao Deducao Natural Exercıcios Regras para o Quantificador Universal Exemplo 1 Pt xPx Qx Qt Revisao A rvores de Analise Substituicao Deducao Natural Exercıcios Regras para o Quantificador Universal Introducao do Quantificador Universal x0 φx0 m n n1 xφxx0 i mn se φ everdade para um x0 arbitrario φ everdade para todo x Revisao A rvores de Analise Substituicao Deducao Natural Exercıcios Regras para o Quantificador Universal Exemplo 2 xPx Qx x Px x Qx Revisao A rvores de Analise Substituicao Deducao Natural Exercıcios Regras para o Quantificador Existencial Introducao do Quantificador Existencial m φx0 p xφxx0 i m se φ e verdade para um x entao existe um x em que φ e verdade Revisao A rvores de Analise Substituicao Deducao Natural Exercıcios Regras para o Quantificador Existencial Exemplo 3 xPx xPx Revisao A rvores de Analise Substituicao Deducao Natural Exercıcios Regras para o Quantificador Existencial Eliminacao do Quantificador Existencial xφx x0 φx0x hipotese χ m n p p 1 χ e m np se φeverdade para pelo menos um valor de x e se a partir da suposicao que φeverdade para um x0 generico pudermos demonstrar χ Entao χ e verdade Revisao A rvores de Analise Substituicao Deducao Natural Exercıcios Regras para o Quantificador Existencial Exemplo 4 xPx Qx xPx xQx Revisao A rvores de Analise Substituicao Deducao Natural Exercıcios Exercıcios 1 xQx Rx xPx Qx xPx Rx 2 xPx xyPx Qy y Qy 3 xPx xPx 4 xPx xPx