Lógica de programação

Cap´ ıtulo 1

L´gica proposicional o 1.1

Introdu¸˜o ca A l´gica proposicional, ` qual este cap´ o a ıtulo ´ dedicado, pode ser vista como a parte da e l´gica que se ocupa do estudo do comportamento dos conectivos l´gicos e das regras o o que os manipulam. As f´rmulas s˜o constru´ o a ıdas apenas a partir de s´ ımbolos proposicionais e de conectivos l´gicos. Os s´ o ımbolos proposicionais representam proposi¸˜es co (at´micas) cuja estrutura interna ´, neste contexto, irrelevante. o e
´
E importante estudar em primeiro lugar a l´gica proposicional porque muitos o dos conceitos e t´cnicas envolvidos est˜o tamb´m presentes em l´gicas mais sofistie a e o cadas e, numa primeira abordagem, a sua compreens˜o torna-se mais f´cil quando ´ a a e apresentada neste contexto mais simples.
Neste cap´ ıtulo s˜o apresentados, em primeiro lugar, os aspectos sint´cticos e a a semˆnticos da l´gica proposicional. De seguida, apresenta-se um primeiro sistema a o dedutivo para a l´gica proposicional: o sistema de dedu¸˜o natural Np . Como exo ca emplo de outros sistemas dedutivos para a l´gica proposicional que podem tamb´m o e ser encontrados na literatura, apresentam-se depois, de um modo mais sucinto, os seguintes sistemas dedutivos: o sistema de sequentes Sp (e a sua variante Sp ), o sistema de tableaux Tp e o sistema de tipo Hilbert Hp .
O cap´ ıtulo est´ organizado como se segue. Na sec¸˜o 1.2 introduzem-se os aspeca ca tos sint´cticos e na sec¸˜o 1.3 os aspectos semˆnticos. Na sec¸˜o 1.4 apresenta-se o a ca a ca sistema de dedu¸˜o natural Np . Na sec¸˜o 1.5 apresenta-se o sistema de sequentes Sp ca ca ca (e a sua variante Sp ), sendo o sistema de Tp apresentado na sec¸˜o 1.6 e o sistema Hp
1

Sintaxe

na sec¸˜o 1.7. No final de algumas sec¸˜es s˜o propostos exerc´ ca co a ıcios sobre os assuntos nelas apresentados. Os assuntos expostos nas sec¸˜es com a indica¸˜o ( ) tˆm um co ca e car´cter mais