Alunos:Vinicius ArcanjoPedro Garagnani

Curso: Engenharia de Computação, 2009.02Professor: Adolfo NetoDisciplina: Lógica para Computação.

Tablôs

• - É um método de inferência baseado em refutação para lógica proposicional.

• Para provarmos que:• B1,...,Bn |- A1,...,An, • afirmaremos a veracidade de B1,..., Bn e a falsidade de

A1,...,An, na esperança de derivarmos uma contradição.• Se a contradição for obtida, teremos demonstrado o

sequente.• Caso contrário teremos obtido um contra-exemplo, ou seja,

teremos construído uma valoração que satisfaz todas as fórmulas Bi do antecedente e falsifica todas as formulas Aj do consequente.

As fórmulas dos tablôs analíticos podem ser de dois tipos: Fórmulas do tipo α e fórmulas do tipo β -As fórmulas do tipo α se decompõem em fórmulas α1 e α2 em um único ramo.-As fórmulas do tipo β se decompõem através da bifurcação gerando β1 e β2,ou seja, decompõem-se em dois ramos.- Se no sequente existir um átomo p, onde p é um átomo qualquer, por exemplo, ele não é formula nem do tipo α nem β, logo não gera expansão.

Regras Alpha : Regras Beta :

Observação: T = True, F = False

• Em cada ramo, uma fórmula só pode ser expandida uma vez. • Um ramo que não possui mais fórmulas para serem expandi-

das é chamado de ramo saturado. • Ramo aberto é um ramo que não possui um par de fórmulas

conjugadas.• Um ramo é dito fechado quando nele encontramos um par de

fórmulas conjugadas, por exemplo, T p e F p. (T = true, F = false)

• Quando fecha-se um ramo não é preciso expandi-lo mais.• Após realizar todas as expansões possíveis e existir um ramo

aberto e saturado, o sequente é dito refutável.• Um sequente é provado (ou deduzido) quando todos os

ramos foram fechados.

Para deduzir um sequente siga os seguintes passos:

• A prova de um sequente através dos Tablôs KE é muito semelhante ao método dos Tablôs Analíticos.

• Da mesma maneira, para se provar um sequente, é necessário refutar todas as premissas e afirmar a veracidade das hipóteses para tentar achar uma contradição.

• Se, em cada ramo, a contradição for obtida, o sequente foi provado.

• Recomenda-se aplicar primeiramente todas as regras alfa possíveis, depois todas as beta e por fim, se ainda restarem fórmulas a serem analisadas, utiliza-se a regra PB para ramificar o corpo do tablô.

Regras alpha: Regras beta:

Rega PB:

• Assim como os Tablôs Analíticos, os Tablôs KE utilizam-se de regras alpha e beta.

• Basicamente, as regras alpha são aquelas que utilizam-se de apenas uma fórmula para se obter um (ou mais) resultados.

• As regras beta, por sua vez, necessitam de duas fórmulas para gerar um resultado.

• A única regra que ramifica o Tablô é a regra PB.

• Se não for possível aplicar mais nenhuma regra alfa ou beta, seleciona-se uma fórmula composta qualquer, por exemplo F A v B, e cria-se dois ramos a partir de um átomo selecionado, como TA e FA.

• Com essas novas fórmulas é possível então voltar a aplicar regras no Tablô.

• Nota-se que será necessário finalizar cada novo ramo gerado para concluir a prova.

SILVA, Flávio S. C. da; FINGER, Marcelo; MELO, Ana C. V. de. Lógica para Computação. São Paulo: Thomson Learning, 2006.

KAESTNER, Celso. Slides sobre “Sistemas Dedutivos". 2008. Disponível em: <http://www.dainf.ct.utfpr.edu.br/~kaestner/Logica/SistemasDedutivos.ppt>. Acesso em: 28 nov. 2009.

NETO, Adolfo. Como provar KE. 2009. Disponível em: <http://www.dainf.ct.utfpr.edu.br/~adolfo/Disciplinas/LogicaParaComputacao/5.SistemasDedutivos/ComoProvarKE.pdf>. Acesso em: 28 nov. 2009.