lc1-2020-1
Table of Contents
- Projeto
- Referências bibliográficas
- Questões
- Plano de Ensino (Novo plano de ensino para o ensino remoto)
- Quadro de avisos
- : Informações de acesso enviadas para o email cadastrado no SIGAA.
- : O ajuste de matrícula já começou! O prazo final para o ajuste é .
- : De acordo com a decisão do CEPE, as atividades acadêmicas serão retomadas de forma remota a partir de . 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!).
- : Dada a suspensão do calendário acadêmico pelo CEPE, retomaremos as atividades assim que o novo calendário for divulgado.
- : 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.
- : Uma nova versão do plano de ensino será disponibilizada, e as atividades do curso serão realizadas a partir de segunda-feira de forma remota a partir desta página e do moodle link.
- : 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
- tags
- (no term)
- coq
Referências bibliográficas
cite:schoningLogicComputerScientists2008 (sem pdf)
cite:moreiraLogicaComputacional2016
cite:huthLogicComputerScience2004
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)}
\]