lc1-2020-1

Table of Contents

tags
(no term)
coq

Projeto

enunciado: tex pdf

arquivo coq para os alunos: coq

gabarito: coq

Referências bibliográficas

Questões

Para gerar o pdf: C-c C-e l o

Equivalência da implicação

\[ \inferrule*[Right={$\lore{x}{y}$}]{ \inferrule*[Right={$\lem$}]{ } {\varphi \lor \lnot \varphi} \and \and \inferrule*[Right={$\lori$}]{ \inferrule*[Right={$\toe$}]{ [\varphi]^x \and \varphi \to \psi } {\psi} } {\lnot \varphi \lor \psi} \and \and \inferrule*[Right={$\lori$}]{ [\lnot \varphi]^y } {\lnot \varphi \lor \psi} } {\lnot \varphi \lor \psi} \]

\[ \inferrule*[Right={$\lore{x}{y}$}]{ \inferrule*[Right={$\lem$}]{ } {\varphi \lor \lnot \varphi} \and \and \inferrule*[Right={$\lori$}]{ \inferrule*[Right={$\toe$}]{ [\varphi]^x \and \varphi \to \psi } {\psi} } {\lnot \varphi \lor \psi} \and \and \inferrule*[Right={$\lori$}]{ [\lnot \varphi]^y } {\lnot \varphi \lor \psi} } {\lnot \varphi \lor \psi} \]

\[ \inferrule*[Right={$\toi{w}$}]{ \inferrule*[Right={$\lore{x}{y}$}]{ (\lnot \varphi) \lor \psi \and \inferrule*[Right={$\bote$}]{ \inferrule*[Right={$\nege$}]{ [\varphi]^w \and [\lnot \varphi]^x } {\bot} } {\psi} \and \and [\psi]^y } {\psi} } {\varphi \to \psi} \]

\[ \inferrule*[Right={$\lore{x}{y}$}]{ (\lnot \varphi) \lor \psi \and \inferrule*[Right={$\toi{w}$}]{ \inferrule*[Right={$\bote$}]{ \inferrule*[Right={$\nege$}]{ [\varphi]^w \and [\lnot \varphi]^x } {\bot} } {\psi}} {\varphi \to \psi} \and \and \inferrule*[Right={$\toi{w}$}]{ [\psi]^y} {\varphi \to \psi} } {\varphi \to \psi} \]

Comutatividade da conjunção

\[ \inferrule{ \inferrule{ \inferrule{[\phi \land \psi]}{\psi} \and \inferrule{[\phi \land \psi]}{\phi}}{(\psi \land \phi)}}{(\phi \land \psi) \to (\psi \land \phi)} \]

\[ \inferrule*[Right={$\toi{u}$}]{ \inferrule*[Right={$\landi$}]{ \inferrule*[Right={$\lande$}]{[\phi \land \psi]^u}{\psi} \and \inferrule*[Right={$\lande$}]{[\phi \land \psi]^u}{\phi}}{(\psi \land \phi)}}{(\phi \land \psi) \to (\psi \land \phi)} \]

Propagação da dupla negação sobre a implicação

\[ \inferrule*[Right={$\toi{u}$}]{ \inferrule*[Right={$\negi{v}$}]{ \inferrule*[Right={$\nege$}]{ \lnot\lnot(\phi\to\psi) \and \\ \inferrule*[Right={$\negi{x}$}]{ \inferrule*[Right={$\nege$}]{ [\lnot\lnot\phi]^u \and \\ \inferrule*[Right={$\negi{y}$}]{ \inferrule*[Right={$\nege$}]{ [\lnot\psi]^v \and \\ \inferrule*[Right={$\toe$}]{ [\phi\to\psi]^x \and \\ [\phi]^y} {\psi}} {\bot}} {\lnot\phi}} {\bot}} {\lnot(\phi\to\psi)}} {\bot}} {\lnot\lnot\psi}} {(\lnot\lnot\phi)\to(\lnot\lnot\psi)} \]

\[ \inferrule*[Right={$\toi{u}$}]{ \inferrule*[Right={$\negi{v}$}]{ \inferrule*[Right={$\nege$}]{ [\lnot\lnot\phi]^u \and \\ \inferrule*[Right={$\negi{y}$}]{ \inferrule*[Right={$\nege$}]{ [\lnot\psi]^v \and \\ \inferrule*[Right={$\toe$}]{ [\phi\to\psi]^x \and \\ [\phi]^y} {\psi}} {\bot}} {\lnot\phi}} {\bot}} {\neg\neg\psi}} {(\lnot\lnot\phi)\to(\lnot\lnot\psi)} \]

\[ \inferrule*[Right={$\toi{u}$}]{ \inferrule*[Right={$\negi{v}$}]{ \inferrule*[Right={$\nege$}]{ \inferrule*[Right={$\toe$}]{ \inferrule*[Right={$\nne$}]{ \neg\neg(\phi \to \psi)} {\phi \to \psi} \and \inferrule*[Right={$\nne$}]{ [\neg\neg\phi]^u }{\phi}} {\psi} \and [\neg\psi]^v} {\bot} }{\neg\neg\psi} } {(\lnot\lnot\phi)\to(\lnot\lnot\psi)} \]

\[ \inferrule*[Right={$\toi{u}$}]{ \inferrule*[Right={$\negi{v}$}]{ \inferrule*[Right={$\nege$}]{ \inferrule*[Right={$\toe$}]{ \inferrule*[Right={$\nne$}]{ \neg\neg(\phi \to \psi)} {\phi \to \psi} \and \inferrule*[Right={$\nne$}]{ [\neg\neg\phi]^u }{\phi}} {\psi} \and [\neg\psi]^v} {\bot} }{\neg\neg\psi} } {(\lnot\lnot\phi)\to(\lnot\lnot\psi)} \]

\[ \inferrule*[Right={$\nni$}]{ \inferrule*[Right={$\nne$}]{ \neg\neg(\phi \to \psi)} {\phi \to \psi}} {(\lnot\lnot\phi)\to(\lnot\lnot\psi)} \]

\[ \inferrule*[Right={$\toi{\emptyset}$}]{ \inferrule*[Right={$\negi{v}$}]{ \inferrule*[Right={$\nege$}]{ \inferrule*[Right={$\toe$}]{ [\phi]^u \and \inferrule*[Right={$\nne$}]{ \neg\neg(\phi \to \psi)} {\phi \to \psi}} {\psi} \and [\neg\psi]^v} {\bot} }{\neg\neg\psi} } {(\lnot\lnot\phi)\to(\lnot\lnot\psi)} \]

Eliminação do existencial:

\[ \inferrule*[Right={$\exie{u}$}]{\exists_x p(x) \and [p(x_0)]^u } {p(x_0)} \]

Introdução do universal:

\[ \inferrule*[Right={$\exie{u}$}]{\exists_x p(x) \and \inferrule*[Right={$\alli$}]{[p(x_0)]^u}{\forall_x p(x)} } {\forall_x p(x)} \]

Plano de Ensino (Novo plano de ensino para o ensino remoto)

Quadro de avisos

[2020-08-13 Qui 09:30]: Informações de acesso enviadas para o email cadastrado no SIGAA.

[2020-08-04 Ter 05:39]: O ajuste de matrícula já começou! O prazo final para o ajuste é [2020-08-10 Seg].

[2020-08-04 Ter 05:26]: De acordo com a decisão do CEPE, as atividades acadêmicas serão retomadas de forma remota a partir de [2020-08-17 Seg]. O curso será feito via a plataforma institucional Aprender3. O cadastro na página da disciplina no Aprender3 será feito via uma senha (chave de acesso) que será enviado para o seu email cadastrado no SIGAA (Faça o autocadastro!).

[2020-03-25 Qua 17:08]: Dada a suspensão do calendário acadêmico pelo CEPE, retomaremos as atividades assim que o novo calendário for divulgado.

[2020-03-23 Seg 09:24]: Um arquivo de introdução à lógica proposicional foi disponibilizado para leitura na página da disciplina no moodle http://aprender.unb.br. Este material também inclui exercícios ao longo do texto. Resolva cada um destes exercícios porque esta é uma etapa importante do aprendizado. Posteriormente serão disponibilizadas atividades para avaliar a sua compreensão sobre lógica proposicional no moodle.

[2020-03-20 Sex 08:59]: Uma nova versão do plano de ensino será disponibilizada, e as atividades do curso serão realizadas a partir de segunda-feira [2020-03-23 Seg] de forma remota a partir desta página e do moodle link.

[2020-03-16 Seg 15:36]: As aulas presenciais canceladas. Atividades serão oportunamente propostas via a página da disciplina no moodle http://aprender.unb.br.

Link para página do curso no Moodle.

Arquivos: ProofWeb.v

Author: Flávio L. C. de Moura

Email: flavio@flaviomoura.info

Created: 2021-01-22 Sex 15:54

Validate