45
Lógica Computacional DCC/FCUP 2019/20

Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

  • Upload
    others

  • View
    3

  • Download
    0

Embed Size (px)

Citation preview

Page 1: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Lógica Computacional

DCC/FCUP

2019/20

Page 2: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Funcionamento da disciplina

• Docentes:• Teóricas: Sandra Alves• Práticas: Sandra Alves, Sabine Broda e Nelma Moreira

• Página webhttp://www.dcc.fc.up.pt/~sandra/Home/LC1920.html(slides de aulas e folhas de exercícios, etc...)

• Avaliação:• Primeiro teste (PT) + Segundo teste (ST)

Final = PT ⇤ (0.5) + ST ⇤ (0.5)1

• Recurso cotado para 20 valores.• Data do primeiro teste: 13 de Novembro.• Data do segundo teste: a definir durante a época normal de

avaliação.

1PT , ST � 6 e Final � 9.5

Page 3: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Alguma Bibliografia

• “Logic in Computer Science”, Michael Huth , 1962.• “Language, proof, and logic” , Jon Barwise, 1999.• “Essentials of logic programming” , Christopher John Hogger,

1990.• “Rigorous software development” , José Bacelar Almeida et al.,

2011.• “Mathematical Logic for Computer Science” . Mordechai

Ben-Ari 2001.

Page 4: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Objectivos

Introdução à lógica matemática numa perspectiva computacional.

• noções básicas do raciocínio lógico e utilização correcta dossistemas dedutivos

• Relação entre semântica e sistemas dedutivos: integridade ecompletude (o que é válido é deduzível; o que é deduzível éválido)...

• Lógica proposicional e Lógica de primeira ordem• Axiomatizações• Breve introdução à Programação em Lógica (base da

linguagem de programação prolog).

Page 5: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Programa

1. Lógica proposicional• sintaxe; semântica (tautologias, satisfazibilidade, validade);

formas normais; sistema dedutivo de dedução natural, DN;Completude e integridade do sistema DN; outros sistemasdedutivos (Hilbert, tableaux, resolução); decidibilidade ealgoritmos de satisfazibilidade

2. Lógica de primeira ordem (de predicados)• linguagens; sintaxe; semântica (interpretações, modelos,

satisfazibilidade, validade); sistema dedutivo de deduçãonatural; completude e integridade do DN; teorias eaxiomatizações; indecidibilidade da lógica de primeira ordem;limite dos métodos formais (Teorema de Gödel)

3. Programação em lógica• resolução; fórmulas de Horn e programas definidos; unificação

de termos, resolução-SLD, completude e integridade.

Page 6: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Programa

1. Lógica proposicional• sintaxe; semântica (tautologias, satisfazibilidade, validade);

formas normais; sistema dedutivo de dedução natural, DN;Completude e integridade do sistema DN; outros sistemasdedutivos (Hilbert, tableaux, resolução); decidibilidade ealgoritmos de satisfazibilidade

2. Lógica de primeira ordem (de predicados)• linguagens; sintaxe; semântica (interpretações, modelos,

satisfazibilidade, validade); sistema dedutivo de deduçãonatural; completude e integridade do DN; teorias eaxiomatizações; indecidibilidade da lógica de primeira ordem;limite dos métodos formais (Teorema de Gödel)

3. Programação em lógica• resolução; fórmulas de Horn e programas definidos; unificação

de termos, resolução-SLD, completude e integridade.

Page 7: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Programa

1. Lógica proposicional• sintaxe; semântica (tautologias, satisfazibilidade, validade);

formas normais; sistema dedutivo de dedução natural, DN;Completude e integridade do sistema DN; outros sistemasdedutivos (Hilbert, tableaux, resolução); decidibilidade ealgoritmos de satisfazibilidade

2. Lógica de primeira ordem (de predicados)• linguagens; sintaxe; semântica (interpretações, modelos,

satisfazibilidade, validade); sistema dedutivo de deduçãonatural; completude e integridade do DN; teorias eaxiomatizações; indecidibilidade da lógica de primeira ordem;limite dos métodos formais (Teorema de Gödel)

3. Programação em lógica• resolução; fórmulas de Horn e programas definidos; unificação

de termos, resolução-SLD, completude e integridade.

Page 8: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

O que é a lógica?

A distinção entre o raciocínio correcto e incorrecto é oprincipal problema que aborda a lógica.

Irving CopiA lógica estuda a razão como ferramenta doconhecimento.

Jacques MaritainA lógica é a ciência do pensamento correcto.

Raymond McCall

Page 9: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas
Page 10: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

O que é a lógica matemática?

Boole ! Frege ! . . .! Hilbert ! Gödel ! . . .

Formalizações simbólicas essencialmente associadas com problemasdos fundamentos da matemática...

• teoria de modelos• teoria da dedução (ou demonstração)• sistemas axiomáticos (p.e., teoria dos conjuntos)

Page 11: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Uma variedade de lógicas

• Lógica clássica: proposicional e de predicados (primeira ordem)• Lógicas de ordem superior• Lógicas subestruturais (p.e intuicionista): modificação das

propriedades das conectivas lógicas. Ex: ¬¬A 6⌘ A;A ^ A 6⌘ A

• Lógicas modais: necessidade, conhecimento, temporais,descrições, etc. A noção de verdade éparametrizada...Exemplo: Hoje é segunda-feira

• · · ·

Page 12: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

O que é “uma lógica”?

• uma linguagem de um alfabeto em que se define o que sãofórmulas e outros objectos.

• Uma maneira de definir uma semântica (=noção do que éverdadeiro) para as fórmulas. Uma mesma lógica pode tervárias semânticas...

• Um sistema de dedução que, usando um número finito deregras permita a obtenção de fórmulas a partir de outras(=raciocínio). Deve ser íntegro: o que se deduz deve serverdadeiro...Mas também será bom que o que é verdadeirodeve ser deduzível (completo)...Mas isto nem sempre épossível.

Page 13: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Lógica e Ciência de Computadores

Circuitos lógicos: lógicas BooleanasBases de dados: lógicas em modelos finitos (SQL=FO)Inteligência artificial: sistemas periciais, linguagem natural, web

semântica, data mining, etc. Robert Kowalski :www.youtube.com/watch?v=H2gOQbEFtMU

Autómatos Finitos: lógica de segunda ordem monádica com umsucessor (os modelos são conjuntos de palavras)

XML: Um documento estruturado é uma árvore de umalinguagem representada por autómatos de árvores aque correspondem fórmulas duma lógica de segundaordem.

Page 14: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Algoritmos e complexidade: classes de complexidade de problemaspodem ser caracterizadas por classes de fórmulaslógicas

Linguagens de programação:• programação em lógica (p.e prolog)• teoria de tipos (sistemas tipos= sistemas

dedutivos) para linguagens funcionais

Page 15: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Especificação formal e verificação:• verificação de hardware (circuitos)• testes de correção de software: lógicas de

programas (dinâmicas,temporais, etc)• cyber-sistemas• protocolos de segurança• sistemas multi-agentes

Demonstração automática Teorias específicas (inteiros, arrays,listas, . . . ) SAT/SMT solvers

Assistentes de demonstração de teoremas Extracção de programasa partir de especificações

• Isabelle• Coq• KeYmaera

Page 16: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Lógica proposicional

Consideram-se frases declarativas (proposições), que podem serverdadeiras (V ) ou falsas (F )

• Os elefantes são mamíferos V• Lisboa é uma cidade V• 2 + 3 = 7 F• 5 2 N V• 3 > 7 F• Um quadrado tem 6 lados F

e estuda-se o processo de construção e a veracidade de outrasproposições usando conectivasou, e , não , se. . . então. . .

Page 17: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Os elefantes são mamíferos e Lisboa é uma cidade V

porque é uma conjunção de proposições V2 + 3 = 7 ou 5 2 N V

porque é uma disjunção de proposições das quais uma é Vnão 3 > 7 V

porque é uma negação de uma proposição FSe 7 > 3 então 3 + 3 = 6 V

porque uma implicação é V sse o consequente é V sempre que oantecedente é V

Se 3 > 7 então 2 + 3 = 6 V

porque é uma implicação cujo antecedente é F

Page 18: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Conectivas lógicas

Cada proposição vai ser representada por uma variávelproposicional e as conectivas lógicas por símbolos n-ários:

Conectiva Símbolos Aridade Outros símbolos equivalentesConjunção ^ 2 &, &&, ·Disjunção _ 2 |, +Negação ¬ 1 ⇠, ,̄ !Implicação ! 2 ), �

Page 19: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Linguagens da lógica proposicional

Uma linguagem da lógica proposicional é formada a partir dosseguintes conjuntos de símbolos primitivos (alfabetos):

• um conjunto numerável de variáveis proposicionaisVProp

= {p, q, r , . . . , p1, . . .}• conectivas lógicas ^ , _ , ¬, !• os parêntesis ( e )

Page 20: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Fórmulas

Uma fórmula bem-formada (�, , ✓, . . . ) é definida indutivamentepelas seguintes regras:

1. uma variável proposicional p é uma fórmula2. se � é uma fórmula então (¬�) é uma fórmula3. se � e são fórmulas então (� ^ ), (� _ ) e (�! )

são fórmulas

� := p | (¬�) | (� ^ �) | (� _ �) | (�! �)

Exemplo

((p ^ (¬p)) ! (¬(p ^ (q _ r))))

Page 21: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Árvore sintáctica duma fórmula (omitindo parêntesis)

((p ^ (¬p)) ! (¬(p ^ (q _ r))))

!

¬

^

_

rq

p

^

¬

p

p

Page 22: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Convenção para omissão de parêntesis

• os parêntesis exteriores podem ser omitidos• ¬ tem precedência sobre ^• ^ tem precedência sobre _• _ tem precedência sobre !• ^ e _ são associativas à esquerda• ! é associativa à direita

Exemplos

� ^ _ ✓ é uma abreviatura de ((� ^ ) _ ✓) ^ � ^ ✓ corresponde a (( ^ �) ^ ✓)p ^ ¬p ! ¬(p ^ (q _ r)) corresponde a((p ^ (¬p)) ! (¬(p ^ (q _ r))))p ! q ! r corresponde a p ! (q ! r)

Page 23: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Sub-fórmulas

Uma sub-fórmula imediata é definida indutivamente pelas seguintesregras:

1. uma variável proposicional não tem sub-fórmulas imediatas2. (¬�) tem � como sub-fórmula imediata3. as fórmulas (� ^ ), (� _ ) e (�! ) têm � e como

sub-fórmulas imediatasUma fórmula � é uma sub-fórmula duma fórmula se e só se:

1. � é uma sub-fórmula imediata de 2. existe uma fórmula ✓ tal que � é uma sub-fórmula de ✓ e ✓ é

uma sub-fórmula de

Quais as sub-fórmulas e quais as sub-fórmulas imediatas de

((¬p ^ q) ! (p ^ (q _ ¬r)))

Page 24: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Semântica da lógica proposicional

Os valores de verdade são V e F .

Atribuição de valores de verdade (ou valoração)

v : VProp

�! {V ,F } que atribuí um valor de verdade a cadavariável

Uma valoração v pode ser estendida ao conjunto das fórmulas:1. para p 2 V

Prop

v(p) já está definido2.

v(¬�) = V se v(�) = Fv(¬�) = F se v(�) = V

Page 25: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

3.

v(� ^ ) = V se v(�) = V e v( ) = Vv(� ^ ) = F caso contrário

4.

v(� _ ) = V se v(�) = V ou v( ) = Vv(� _ ) = F caso contrário

5.

v(�! ) = F se v(�) = V e v( ) = Fv(�! ) = V caso contrário

Page 26: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Tabelas de verdade

� ¬ �F VV F

Page 27: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Tabelas de verdade

� ¬ �F VV F

� � ^ F F FF V FV F FV V V

Page 28: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Tabelas de verdade

� ¬ �F VV F

� � ^ F F FF V FV F FV V V

� � _ F F FF V VV F VV V V

Page 29: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Tabelas de verdade

� ¬ �F VV F

� � ^ F F FF V FV F FV V V

� � _ F F FF V VV F VV V V

� �! F F VF V VV F FV V V

Page 30: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Se v(p) = V , v(q) = F e v(r) = V , podemos calcular o valor dev((p ^ q) _ ¬r)):

p q r ( p ^ q ) _ ¬ rV F V F F F

Page 31: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Tabela de verdade duma fórmula

Uma fórmula � com n variáveis proposicionais tem 2n valorizações.Porquê? Podemos construir uma tabela em que cada linhacorresponde a uma delas:

p q r ( p ^ q ) _ ¬ rV V V V V FV V F V V VV F V F F FV F F F V VF V V F F FF V F F V VF F V F F FF F F F V V

Page 32: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Satisfazibilidade, Tautologias e Contradições

Uma fórmula � é

satisfazível se existe uma valoração v tal que v(�) = V ,escreve-se |=

v

� e diz-se que v satisfaz �tautologia se para todas as valorizações v , v(�) = V e

escreve-se |= � Ex: |= p _ ¬p (Terceiro excluído)contradição se para todas as valorizações v , v(�) = F e

escreve-se 6|= �. Ex: 6|= p ^ ¬p.

Uma fórmula é não-satisfazível se e só se é uma contradição.

Page 33: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Relação de satisfazibilidade

Seja v uma valoração, a relação |=v

pode ser definidaindutivamente na estrutura de � por:

1. |=v

p se v(p) = V ;2. |=

v

¬� se 6|=v

�;3. |=

v

� ^ se |=v

� e |=v

;4. |=

v

� _ se |=v

� ou |=v

;5. |=

v

�! se 6|=v

� ou |=v

;Dizemos que v satisfaz � se |=

v

�.

Page 34: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Exemplo

Sendo v(p) = V , v(q) = v(r) = F determinar se

|=v

(p ! (q _ r)) _ (r ! ¬p).

Para tal, |=v

(p ! (q _ r)) ou |=v

(r ! ¬p).A segunda verifica-se porque 6|=

v

r .Pelo que podemos também concluir que

|=v

(p ! (q _ r)) _ (r ! ¬p).

Page 35: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Exemplo

Sendo v(p) = V , v(q) = v(r) = F determinar se

|=v

(p ! (q _ r)) _ (r ! ¬p).

Para tal, |=v

(p ! (q _ r)) ou |=v

(r ! ¬p).

A segunda verifica-se porque 6|=v

r .Pelo que podemos também concluir que

|=v

(p ! (q _ r)) _ (r ! ¬p).

Page 36: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Exemplo

Sendo v(p) = V , v(q) = v(r) = F determinar se

|=v

(p ! (q _ r)) _ (r ! ¬p).

Para tal, |=v

(p ! (q _ r)) ou |=v

(r ! ¬p).A segunda verifica-se porque 6|=

v

r .

Pelo que podemos também concluir que

|=v

(p ! (q _ r)) _ (r ! ¬p).

Page 37: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Exemplo

Sendo v(p) = V , v(q) = v(r) = F determinar se

|=v

(p ! (q _ r)) _ (r ! ¬p).

Para tal, |=v

(p ! (q _ r)) ou |=v

(r ! ¬p).A segunda verifica-se porque 6|=

v

r .Pelo que podemos também concluir que

|=v

(p ! (q _ r)) _ (r ! ¬p).

Page 38: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Exemplo

Determinar se (p ^ q) _ ¬r é válida, isto é, |= (p ^ q) _ ¬r .

Mas,se v(r) = V e v(p) = F então 6|=

v

(p ^ q) _ ¬r : porque 6|=v

¬r e6|=

v

(p ^ q).Logo, não é válida.

Page 39: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Exemplo

Determinar se (p ^ q) _ ¬r é válida, isto é, |= (p ^ q) _ ¬r .Mas,se v(r) = V e v(p) = F então 6|=

v

(p ^ q) _ ¬r : porque 6|=v

¬r e6|=

v

(p ^ q).Logo, não é válida.

Page 40: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Consequência e equivalência semântica

Satisfazibilidade de um conjunto de fórmulas

� um conjunto de fórmulas.

Uma valoração v satisfaz � se e só se v satisfaz toda a fórmula 2 �.

8 2 �, |=v

� é satisfazível se existe uma valoração que o satisfaz

Consequência

Uma fórmula � é uma consequência semântica de � se para toda avaloração v que satisfaz �, se tem v(�) = V ; e escreve-se � |= �

; |= � é equivalente a |= �Se � = { } e � |= � então diz-se que � é consequência semânticade ( |= �)

Page 41: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Consequência e equivalência semântica

Satisfazibilidade de um conjunto de fórmulas

� um conjunto de fórmulas.Uma valoração v satisfaz � se e só se v satisfaz toda a fórmula 2 �.

8 2 �, |=v

� é satisfazível se existe uma valoração que o satisfaz

Consequência

Uma fórmula � é uma consequência semântica de � se para toda avaloração v que satisfaz �, se tem v(�) = V ; e escreve-se � |= �

; |= � é equivalente a |= �Se � = { } e � |= � então diz-se que � é consequência semânticade ( |= �)

Page 42: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Consequência e equivalência semântica

Satisfazibilidade de um conjunto de fórmulas

� um conjunto de fórmulas.Uma valoração v satisfaz � se e só se v satisfaz toda a fórmula 2 �.

8 2 �, |=v

� é satisfazível se existe uma valoração que o satisfaz

Consequência

Uma fórmula � é uma consequência semântica de � se para toda avaloração v que satisfaz �, se tem v(�) = V ; e escreve-se � |= �

; |= � é equivalente a |= �Se � = { } e � |= � então diz-se que � é consequência semânticade ( |= �)

Page 43: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Consequência e equivalência semântica

Satisfazibilidade de um conjunto de fórmulas

� um conjunto de fórmulas.Uma valoração v satisfaz � se e só se v satisfaz toda a fórmula 2 �.

8 2 �, |=v

� é satisfazível se existe uma valoração que o satisfaz

Consequência

Uma fórmula � é uma consequência semântica de � se para toda avaloração v que satisfaz �, se tem v(�) = V ; e escreve-se � |= �

; |= � é equivalente a |= �Se � = { } e � |= � então diz-se que � é consequência semânticade ( |= �)

Page 44: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Consequência e equivalência semântica

Satisfazibilidade de um conjunto de fórmulas

� um conjunto de fórmulas.Uma valoração v satisfaz � se e só se v satisfaz toda a fórmula 2 �.

8 2 �, |=v

� é satisfazível se existe uma valoração que o satisfaz

Consequência

Uma fórmula � é uma consequência semântica de � se para toda avaloração v que satisfaz �, se tem v(�) = V ; e escreve-se � |= �

; |= � é equivalente a |= �Se � = { } e � |= � então diz-se que � é consequência semânticade ( |= �)

Page 45: Lógica Computacional - DCCsandra/Home/LC1920_files/aula1.pdf · 2019. 9. 26. · Objectivos Introdução à lógica matemática numa perspectiva computacional. • noções básicas

Fórmulas semânticamente equivalentes

Equivalência semântica

Se |= � e � |= então e � são semânticamente equivalentes eescreve-se ⌘ �.

� ^ ⌘ ^ � (comutatividade)� _ ⌘ _ � (comutatividade)

¬(� ^ ) ⌘ (¬� _ ¬ ) (Lei de DeMorgan)¬(� _ ) ⌘ (¬� ^ ¬ ) (Lei de DeMorgan)

(� ^ ) ^ ✓ ⌘ � ^ ( ^ ✓) (associatividade)(� _ ) _ ✓ ⌘ � _ ( _ ✓) (associatividade)

(� _ �) ⌘ � (idempotência)(� ^ �) ⌘ � (idempotência)

(� ^ ) _ ✓ ⌘ (� _ ✓) ^ ( _ ✓) (distributividade)(� _ ) ^ ✓ ⌘ (� ^ ✓) _ ( ^ ✓) (distributividade)

¬¬� ⌘ � (Dupla negação)�! ⌘ ¬� _