Merge pull request #52 from TiagoRG/dev-tiagorg

[LSD] pratica04 CounterDemo enable/disable added and added FreqDevider by itself
[C2] material added
[LABI] material added
This commit is contained in:
Tiago Garcia 2023-04-04 22:13:25 +01:00 committed by GitHub
commit 13fe5c48f5
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
23 changed files with 406 additions and 459 deletions

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

View File

@ -31,6 +31,13 @@ https://fpgasoftware.intel.com/eula.
(text "binInput[3..0]" (rect 21 27 70 39)(font "Arial" ))
(line (pt 0 32)(pt 16 32)(line_width 3))
)
(port
(pt 0 48)
(input)
(text "enable" (rect 0 0 24 12)(font "Arial" ))
(text "enable" (rect 21 43 45 55)(font "Arial" ))
(line (pt 0 48)(pt 16 48)(line_width 1))
)
(port
(pt 208 32)
(output)

View File

@ -4,14 +4,16 @@ use IEEE.STD_LOGIC_1164.all;
entity Bin7SegDecoder is
port
(
binInput : in std_logic_vector(3 downto 0);
binInput : in std_logic_vector(3 downto 0);
enable : in std_logic;
decOut_n : out std_logic_vector(6 downto 0)
);
end Bin7SegDecoder;
architecture Behavioral of Bin7SegDecoder is
begin
decOut_n <= "1111001" when (binInput = "0001") else --1
decOut_n <= "0111111" when (enable = '0' ) else -- disabled
"1111001" when (binInput = "0001") else --1
"0100100" when (binInput = "0010") else --2
"0110000" when (binInput = "0011") else --3
"0011001" when (binInput = "0100") else --4

View File

@ -20,23 +20,6 @@ refer to the applicable agreement for further details, at
https://fpgasoftware.intel.com/eula.
*/
(header "graphic" (version "1.4"))
(pin
(input)
(rect 256 232 424 248)
(text "INPUT" (rect 125 0 154 10)(font "Arial" (font_size 6)))
(text "KEY[1]" (rect 5 0 39 11)(font "Arial" ))
(pt 168 8)
(drawing
(line (pt 84 12)(pt 109 12))
(line (pt 84 4)(pt 109 4))
(line (pt 113 8)(pt 168 8))
(line (pt 84 12)(pt 84 4))
(line (pt 109 4)(pt 113 8))
(line (pt 109 12)(pt 113 8))
)
(text "VCC" (rect 128 7 149 17)(font "Arial" (font_size 6)))
(annotation_block (location)(rect 192 248 256 264))
)
(pin
(input)
(rect 256 248 424 264)
@ -58,7 +41,7 @@ https://fpgasoftware.intel.com/eula.
(input)
(rect 152 176 320 192)
(text "INPUT" (rect 125 0 154 10)(font "Arial" (font_size 6)))
(text "CLOCK_50" (rect 5 0 63 11)(font "Arial" ))
(text "CLOCK_50" (rect 5 0 62 11)(font "Arial" ))
(pt 168 8)
(drawing
(line (pt 84 12)(pt 109 12))
@ -71,9 +54,43 @@ https://fpgasoftware.intel.com/eula.
(text "VCC" (rect 128 7 149 17)(font "Arial" (font_size 6)))
(annotation_block (location)(rect 88 192 152 208))
)
(pin
(input)
(rect 496 304 664 320)
(text "INPUT" (rect 125 0 154 10)(font "Arial" (font_size 6)))
(text "SW[1]" (rect 5 0 36 11)(font "Arial" ))
(pt 168 8)
(drawing
(line (pt 84 12)(pt 109 12))
(line (pt 84 4)(pt 109 4))
(line (pt 113 8)(pt 168 8))
(line (pt 84 12)(pt 84 4))
(line (pt 109 4)(pt 113 8))
(line (pt 109 12)(pt 113 8))
)
(text "VCC" (rect 128 7 149 17)(font "Arial" (font_size 6)))
(annotation_block (location)(rect 496 320 560 336))
)
(pin
(input)
(rect 256 232 424 248)
(text "INPUT" (rect 125 0 154 10)(font "Arial" (font_size 6)))
(text "KEY[0]" (rect 5 0 40 11)(font "Arial" ))
(pt 168 8)
(drawing
(line (pt 84 12)(pt 109 12))
(line (pt 84 4)(pt 109 4))
(line (pt 113 8)(pt 168 8))
(line (pt 84 12)(pt 84 4))
(line (pt 109 4)(pt 113 8))
(line (pt 109 12)(pt 113 8))
)
(text "VCC" (rect 128 7 149 17)(font "Arial" (font_size 6)))
(annotation_block (location)(rect 192 248 256 264))
)
(pin
(output)
(rect 872 216 1048 232)
(rect 896 216 1072 232)
(text "OUTPUT" (rect 1 0 41 10)(font "Arial" (font_size 6)))
(text "HEX0[6..0]" (rect 90 0 144 11)(font "Arial" ))
(pt 0 8)
@ -86,7 +103,7 @@ https://fpgasoftware.intel.com/eula.
(line (pt 82 8)(pt 78 12))
(line (pt 78 12)(pt 82 8))
)
(annotation_block (location)(rect 1048 232 1112 248))
(annotation_block (location)(rect 1072 232 1136 248))
)
(symbol
(rect 432 224 480 256)
@ -113,28 +130,6 @@ https://fpgasoftware.intel.com/eula.
(circle (rect 31 12 39 20))
)
)
(symbol
(rect 672 192 880 272)
(text "Bin7SegDecoder" (rect 5 0 89 11)(font "Arial" ))
(text "hex" (rect 8 64 28 75)(font "Arial" ))
(port
(pt 0 32)
(input)
(text "binInput[3..0]" (rect 0 0 63 11)(font "Arial" ))
(text "binInput[3..0]" (rect 21 27 84 38)(font "Arial" ))
(line (pt 0 32)(pt 16 32)(line_width 3))
)
(port
(pt 208 32)
(output)
(text "decOut_n[6..0]" (rect 0 0 73 11)(font "Arial" ))
(text "decOut_n[6..0]" (rect 126 27 199 38)(font "Arial" ))
(line (pt 208 32)(pt 192 32)(line_width 3))
)
(drawing
(rectangle (rect 16 16 192 64))
)
)
(symbol
(rect 488 192 664 304)
(text "CounterUpDown4" (rect 5 0 94 11)(font "Arial" ))
@ -193,6 +188,35 @@ https://fpgasoftware.intel.com/eula.
(rectangle (rect 16 16 128 64))
)
)
(symbol
(rect 680 192 888 272)
(text "Bin7SegDecoder" (rect 5 0 89 11)(font "Arial" ))
(text "inst4" (rect 8 64 33 77)(font "Intel Clear" ))
(port
(pt 0 32)
(input)
(text "binInput[3..0]" (rect 0 0 63 11)(font "Arial" ))
(text "binInput[3..0]" (rect 21 27 84 38)(font "Arial" ))
(line (pt 0 32)(pt 16 32)(line_width 3))
)
(port
(pt 0 48)
(input)
(text "enable" (rect 0 0 34 11)(font "Arial" ))
(text "enable" (rect 21 43 55 54)(font "Arial" ))
(line (pt 0 48)(pt 16 48))
)
(port
(pt 208 32)
(output)
(text "decOut_n[6..0]" (rect 0 0 73 11)(font "Arial" ))
(text "decOut_n[6..0]" (rect 126 27 199 38)(font "Arial" ))
(line (pt 208 32)(pt 192 32)(line_width 3))
)
(drawing
(rectangle (rect 16 16 192 64))
)
)
(connector
(pt 480 224)
(pt 488 224)
@ -205,16 +229,6 @@ https://fpgasoftware.intel.com/eula.
(pt 432 240)
(pt 424 240)
)
(connector
(pt 664 224)
(pt 672 224)
(bus)
)
(connector
(pt 872 224)
(pt 880 224)
(bus)
)
(connector
(pt 424 256)
(pt 488 256)
@ -231,3 +245,25 @@ https://fpgasoftware.intel.com/eula.
(pt 328 184)
(pt 320 184)
)
(connector
(pt 664 224)
(pt 680 224)
(bus)
)
(connector
(pt 888 224)
(pt 896 224)
(bus)
)
(connector
(pt 680 240)
(pt 672 240)
)
(connector
(pt 664 312)
(pt 672 312)
)
(connector
(pt 672 240)
(pt 672 312)
)

View File

@ -0,0 +1,145 @@
/*<simulation_settings>
<ftestbench_cmd>quartus_eda --gen_testbench --tool=modelsim_oem --format=vhdl --write_settings_files=off FreqDivider_Demo -c FreqDivider_Demo --vector_source="/home/tiagorg/repos/uaveiro-leci/1ano/2semestre/lsd/pratica04/FreqDivider_Demo/FreqDevider.vwf" --testbench_file="/home/tiagorg/repos/uaveiro-leci/1ano/2semestre/lsd/pratica04/FreqDivider_Demo/simulation/qsim/FreqDevider.vwf.vht"</ftestbench_cmd>
<ttestbench_cmd>quartus_eda --gen_testbench --tool=modelsim_oem --format=vhdl --write_settings_files=off FreqDivider_Demo -c FreqDivider_Demo --vector_source="/home/tiagorg/repos/uaveiro-leci/1ano/2semestre/lsd/pratica04/FreqDivider_Demo/FreqDevider.vwf" --testbench_file="/home/tiagorg/repos/uaveiro-leci/1ano/2semestre/lsd/pratica04/FreqDivider_Demo/simulation/qsim/FreqDevider.vwf.vht"</ttestbench_cmd>
<fnetlist_cmd>quartus_eda --write_settings_files=off --simulation --functional=on --flatten_buses=off --tool=modelsim_oem --format=vhdl --output_directory="/home/tiagorg/repos/uaveiro-leci/1ano/2semestre/lsd/pratica04/FreqDivider_Demo/simulation/qsim/" FreqDivider_Demo -c FreqDivider_Demo</fnetlist_cmd>
<tnetlist_cmd>quartus_eda --write_settings_files=off --simulation --functional=off --flatten_buses=off --timescale=1ps --tool=modelsim_oem --format=vhdl --output_directory="/home/tiagorg/repos/uaveiro-leci/1ano/2semestre/lsd/pratica04/FreqDivider_Demo/simulation/qsim/" FreqDivider_Demo -c FreqDivider_Demo</tnetlist_cmd>
<modelsim_script>onerror {exit -code 1}
vlib work
vcom -work work FreqDivider_Demo.vho
vcom -work work FreqDevider.vwf.vht
vsim -c -t 1ps -L cycloneive -L altera -L altera_mf -L 220model -L sgate -L altera_lnsim work.FreqDivider_vhd_vec_tst
vcd file -direction FreqDivider_Demo.msim.vcd
vcd add -internal FreqDivider_vhd_vec_tst/*
vcd add -internal FreqDivider_vhd_vec_tst/i1/*
proc simTimestamp {} {
echo "Simulation time: $::now ps"
if { [string equal running [runStatus]] } {
after 2500 simTimestamp
}
}
after 2500 simTimestamp
run -all
quit -f
</modelsim_script>
<modelsim_script_timing>onerror {exit -code 1}
vlib work
vcom -work work FreqDivider_Demo.vho
vcom -work work FreqDevider.vwf.vht
vsim -novopt -c -t 1ps -sdfmax FreqDivider_vhd_vec_tst/i1=FreqDivider_Demo_vhd.sdo -L cycloneive -L altera -L altera_mf -L 220model -L sgate -L altera_lnsim work.FreqDivider_vhd_vec_tst
vcd file -direction FreqDivider_Demo.msim.vcd
vcd add -internal FreqDivider_vhd_vec_tst/*
vcd add -internal FreqDivider_vhd_vec_tst/i1/*
proc simTimestamp {} {
echo "Simulation time: $::now ps"
if { [string equal running [runStatus]] } {
after 2500 simTimestamp
}
}
after 2500 simTimestamp
run -all
quit -f
</modelsim_script_timing>
<hdl_lang>vhdl</hdl_lang>
</simulation_settings>*/
/*
WARNING: Do NOT edit the input and output ports in this file in a text
editor if you plan to continue editing the block that represents it in
the Block Editor! File corruption is VERY likely to occur.
*/
/*
Copyright (C) 2020 Intel Corporation. All rights reserved.
Your use of Intel Corporation's design tools, logic functions
and other software and tools, and any partner logic
functions, and any output files from any of the foregoing
(including device programming or simulation files), and any
associated documentation or information are expressly subject
to the terms and conditions of the Intel Program License
Subscription Agreement, the Intel Quartus Prime License Agreement,
the Intel FPGA IP License Agreement, or other applicable license
agreement, including, without limitation, that your use is for
the sole purpose of programming logic devices manufactured by
Intel and sold by Intel or its authorized distributors. Please
refer to the applicable agreement for further details, at
https://fpgasoftware.intel.com/eula.
*/
HEADER
{
VERSION = 1;
TIME_UNIT = ns;
DATA_OFFSET = 0.0;
DATA_DURATION = 1000.0;
SIMULATION_TIME = 0.0;
GRID_PHASE = 0.0;
GRID_PERIOD = 10.0;
GRID_DUTY_CYCLE = 50;
}
SIGNAL("clkIn")
{
VALUE_TYPE = NINE_LEVEL_BIT;
SIGNAL_TYPE = SINGLE_BIT;
WIDTH = 1;
LSB_INDEX = -1;
DIRECTION = INPUT;
PARENT = "";
}
SIGNAL("clkOut")
{
VALUE_TYPE = NINE_LEVEL_BIT;
SIGNAL_TYPE = SINGLE_BIT;
WIDTH = 1;
LSB_INDEX = -1;
DIRECTION = OUTPUT;
PARENT = "";
}
TRANSITION_LIST("clkIn")
{
NODE
{
REPEAT = 1;
NODE
{
REPEAT = 50;
LEVEL 0 FOR 10.0;
LEVEL 1 FOR 10.0;
}
}
}
TRANSITION_LIST("clkOut")
{
NODE
{
REPEAT = 1;
LEVEL X FOR 1000.0;
}
}
DISPLAY_LINE
{
CHANNEL = "clkIn";
EXPAND_STATUS = COLLAPSED;
RADIX = Binary;
TREE_INDEX = 0;
TREE_LEVEL = 0;
}
DISPLAY_LINE
{
CHANNEL = "clkOut";
EXPAND_STATUS = COLLAPSED;
RADIX = Binary;
TREE_INDEX = 1;
TREE_LEVEL = 0;
}
TIME_BAR
{
TIME = 0;
MASTER = TRUE;
}
;

View File

@ -0,0 +1,44 @@
/*
WARNING: Do NOT edit the input and output ports in this file in a text
editor if you plan to continue editing the block that represents it in
the Block Editor! File corruption is VERY likely to occur.
*/
/*
Copyright (C) 2020 Intel Corporation. All rights reserved.
Your use of Intel Corporation's design tools, logic functions
and other software and tools, and any partner logic
functions, and any output files from any of the foregoing
(including device programming or simulation files), and any
associated documentation or information are expressly subject
to the terms and conditions of the Intel Program License
Subscription Agreement, the Intel Quartus Prime License Agreement,
the Intel FPGA IP License Agreement, or other applicable license
agreement, including, without limitation, that your use is for
the sole purpose of programming logic devices manufactured by
Intel and sold by Intel or its authorized distributors. Please
refer to the applicable agreement for further details, at
https://fpgasoftware.intel.com/eula.
*/
(header "symbol" (version "1.1"))
(symbol
(rect 16 16 160 96)
(text "FreqDivider" (rect 5 0 52 12)(font "Arial" ))
(text "inst" (rect 8 64 20 76)(font "Arial" ))
(port
(pt 0 32)
(input)
(text "clkIn" (rect 0 0 17 12)(font "Arial" ))
(text "clkIn" (rect 21 27 38 39)(font "Arial" ))
(line (pt 0 32)(pt 16 32)(line_width 1))
)
(port
(pt 144 32)
(output)
(text "clkOut" (rect 0 0 24 12)(font "Arial" ))
(text "clkOut" (rect 99 27 123 39)(font "Arial" ))
(line (pt 144 32)(pt 128 32)(line_width 1))
)
(drawing
(rectangle (rect 16 16 128 64)(line_width 1))
)
)

View File

@ -0,0 +1,33 @@
library IEEE;
use IEEE.STD_LOGIC_1164.all;
use IEEE.NUMERIC_STD.all;
entity FreqDivider is
port (clkIn : in std_logic;
clkOut : out std_logic
);
end FreqDivider;
architecture Behavioral of FreqDivider is
signal s_counter : unsigned(31 downto 0);
signal s_halfWay : unsigned(31 downto 0);
signal k : std_logic_vector(31 downto 0);
begin
k <= x"017D7840";
s_halfWay <= unsigned(k);
process(clkIn)
begin
if (rising_edge(clkIn)) then
if (s_counter = s_halfWay - 1) then
clkOut <= '0';
s_counter <= (others => '0');
else
if (s_counter = s_halfWay/2 - 1) then
clkOut <= '1';
end if;
s_counter <= s_counter + 1;
end if;
end if;
end process;
end Behavioral;

View File

@ -0,0 +1,84 @@
/*
WARNING: Do NOT edit the input and output ports in this file in a text
editor if you plan to continue editing the block that represents it in
the Block Editor! File corruption is VERY likely to occur.
*/
/*
Copyright (C) 2020 Intel Corporation. All rights reserved.
Your use of Intel Corporation's design tools, logic functions
and other software and tools, and any partner logic
functions, and any output files from any of the foregoing
(including device programming or simulation files), and any
associated documentation or information are expressly subject
to the terms and conditions of the Intel Program License
Subscription Agreement, the Intel Quartus Prime License Agreement,
the Intel FPGA IP License Agreement, or other applicable license
agreement, including, without limitation, that your use is for
the sole purpose of programming logic devices manufactured by
Intel and sold by Intel or its authorized distributors. Please
refer to the applicable agreement for further details, at
https://fpgasoftware.intel.com/eula.
*/
(header "graphic" (version "1.4"))
(pin
(input)
(rect 304 192 472 208)
(text "INPUT" (rect 125 0 154 10)(font "Arial" (font_size 6)))
(text "CLOCK_50" (rect 5 0 63 11)(font "Arial" ))
(pt 168 8)
(drawing
(line (pt 84 12)(pt 109 12))
(line (pt 84 4)(pt 109 4))
(line (pt 113 8)(pt 168 8))
(line (pt 84 12)(pt 84 4))
(line (pt 109 4)(pt 113 8))
(line (pt 109 12)(pt 113 8))
)
(text "VCC" (rect 128 7 149 17)(font "Arial" (font_size 6)))
)
(pin
(output)
(rect 632 192 808 208)
(text "OUTPUT" (rect 1 0 41 10)(font "Arial" (font_size 6)))
(text "LEDR[0]" (rect 90 0 132 11)(font "Arial" ))
(pt 0 8)
(drawing
(line (pt 0 8)(pt 52 8))
(line (pt 52 4)(pt 78 4))
(line (pt 52 12)(pt 78 12))
(line (pt 52 12)(pt 52 4))
(line (pt 78 4)(pt 82 8))
(line (pt 82 8)(pt 78 12))
(line (pt 78 12)(pt 82 8))
)
)
(symbol
(rect 480 168 624 248)
(text "FreqDivider" (rect 5 0 64 11)(font "Arial" ))
(text "inst" (rect 8 64 26 75)(font "Arial" ))
(port
(pt 0 32)
(input)
(text "clkIn" (rect 0 0 24 11)(font "Arial" ))
(text "clkIn" (rect 21 27 45 38)(font "Arial" ))
(line (pt 0 32)(pt 16 32))
)
(port
(pt 144 32)
(output)
(text "clkOut" (rect 0 0 33 11)(font "Arial" ))
(text "clkOut" (rect 96 27 129 38)(font "Arial" ))
(line (pt 144 32)(pt 128 32))
)
(drawing
(rectangle (rect 16 16 128 64))
)
)
(connector
(pt 472 200)
(pt 480 200)
)
(connector
(pt 632 200)
(pt 624 200)
)

View File

@ -1,10 +0,0 @@
# Matemática Discreta - Apontamentos
### Conteúdos:
* Diretório com todo o código latex das aulas: [classes](https://github.com/TiagoRG/uaveiro-leci/tree/master/1ano/2semestre/md/apontamentos/classes)
* Diretório com todos os PDF com os apontamentos: [pdf](https://github.com/TiagoRG/uaveiro-leci/tree/master/1ano/2semestre/md/apontamentos/pdf)
* Diretório com o template usado: [template](https://github.com/TiagoRG/uaveiro-leci/tree/master/1ano/2semestre/md/apontamentos/template)
* Script em shell para a automação do sistema: [setup.sh](https://github.com/TiagoRG/uaveiro-leci/tree/master/1ano/2semestre/md/apontamentos/setup.sh)
---
*Pode conter erros, caso encontre algum, crie um* [*ticket*](https://github.com/TiagoRG/uaveiro-leci/issues/new)

View File

@ -1,3 +0,0 @@
%! Author = tiagorg
%! Date = 31/01/2023

View File

@ -1,291 +0,0 @@
%! Author = tiagorg
%! Date = 31/01/2023
\documentclass[11pt]{report}
\usepackage{amsmath}
\usepackage[T1]{fontenc} % Fontes T1
\usepackage[utf8]{inputenc} % Input UTF8
\usepackage[backend=biber, style=ieee]{biblatex} % para usar bibliografia
\usepackage{csquotes}
\usepackage[portuguese]{babel} %Usar língua portuguesa
\usepackage{blindtext} % Gerar texto automaticamente
\usepackage{hyperref} % para autoref
\usepackage{graphicx}
\usepackage{indentfirst}
\usepackage[printonlyused]{acronym}
\usepackage{color}
\begin{document}
\def\titulo{Matemática Discreta}
\def\autores{Tiago Garcia}
\def\autorescontactos{tiago.rgarcia@ua.pt}
\def\empresa{Universidade de Aveiro}
\def\logotipo{ua.pdf}
%
\def\tema{Lógica de 1ª Ordem}
%
\begin{titlepage}
\begin{center}
\vspace*{50mm}
{\Huge\textbf{\titulo}}\\
\vspace{10mm}
{\Large \empresa}\\
\vspace{10mm}
{\LARGE \autores}\\
\vspace{30mm}
\begin{figure}[h]
\center
\includegraphics{ua}\label{fig:ua-title}
\end{figure}
\vspace{30mm}
\end{center}
\end{titlepage}
\title{
{\LARGE\textbf{\titulo} }\\\\
{\Large \aula\\ \empresa}
}
\author{
\href{https://github.com/TiagoRG}{\autores} \\
\href{mailto:tiago.rgarcia@ua.pt}{\autorescontactos}
}
\date{\today}
\maketitle
\pagenumbering{arabic}
\clearpage
% Content
\chapter*{Consequências Semânticas}
\section*{Teorema}
Uma fórmula $\Psi$ é consequência lógica (ou semântica) das fórmulas $\psi_1, \psi_2, \ldots, \psi_n$ se e só se $(\psi_1 \wedge \psi_2 \wedge \ldots \wedge \psi_n) \rightarrow \Psi$ é uma tautologia (fórmula válida).
\subsection*{Notação}
$ \psi_1, \ldots, \psi_n \models \Psi $\\
$\Psi$ é consequência lógica (ou semântica) de $\psi_1, \ldots, \psi_n$\\
\par $\psi_1, \ldots, \psi_n \vdash \Psi$ existe uma prova de $\Psi$ a partir de $\psi_1, \ldots, \psi_n$\\
A prova recorre a regras de dedução designadas por regras de inferência, e a tautologias conhecidas.
\section*{Teorema}
$\psi_1, \ldots, \psi_n \models \Psi$\\
($\Psi$ é consequẽncia lógica de $\psi_1, \ldots, \psi_n$) se e só se o conjunto ${{\psi_1, \ldots, \psi_n, \neg\Psi}}$ é inconsistente, isto é, não existe uma interpretação para a qual todas as fórmulas do conjunto tomam valor 1.
\par Para verificar se este conjunto de fórmulas é inconsistente usamos uma nova regra designada por resolução:\\\\
$ \frac{\psi \rightarrow \theta~~~\Psi\vee\psi}{\theta\vee\psi} res $\\Indicam que aplicámos a regra/método da resolução.
\subsection*{Casos particulares}
\begin{enumerate}
\item{Se $ \theta \equiv \bot $ obtemos\\
$\frac{\Psi \rightarrow \bot~~~\Psi\vee\psi}{\bot\vee\psi}$\\
simplificando como: $\bot\vee\psi\equiv\psi~~$ e $~~\Psi\rightarrow\bot\equiv\ned\Psi\vee\bot\equiv\ned\Psi$
\par Para este caso particular a regra da resolução é:\\
$\frac{\neg\Psi~~~\Psi\vee\psi}{\psi} res ~~ \rightarrow \neg\Psi, \Psi $ são lineares complementares.
}
\item {
Se $ \theta\equiv\bot~~~e~~~\psi\equiv\bot $ (este é um caso particular do caso 1.)
\par Se $\psi\equiv\bot$ então $\Psi\vee\psi\equiv\Psi\vee\bot\equiv\Psi$\\
Substituindo no caso particular da regra de resolução obtida em 1. tem-se\\
$ \frac{\neg\Psi~~~\Psi}{\bot} res $
}
\end{enumerate}
\chapter*{Lógica Proposicional}
\section*{Definição}
\subsection*{Simbolos}
Variáveis proposicionais: $p, q, \Psi, \psi, \ldots$\\
Constantes: $\bot e \top$
Conetivos lógicos: $\wedge, \vee, \rightarrow, \leftrightarrow, \neg, \equiv$
\subsection*{Regras de construção}
\begin{enumerate}
\item{Se $\psi$ é uma fórmula proposicional então $\neg\neg\psi$ é uma fórmula proposicional.}
\item{Se $\psi$ e $\theta$ são fórmulas proposicionais então $\psi\wedge\theta$ é uma fórmula proposicional.}
\item{Se $\psi$ e $\theta$ são fórmulas proposicionais então $\psi\vee\theta$ é uma fórmula proposicional.}
\item{Se $\psi$ e $\theta$ são fórmulas proposicionais então $\psi\rightarrow\theta$ é uma fórmula proposicional.}
\item{Se $\psi$ e $\theta$ são fórmulas proposicionais então $\psi\leftrightarrow\theta$ é uma fórmula proposicional.}
\end{enumerate}
\section*{Dedução na lógica proposicional}
\begin{itemize}
\item {Verificar se uma fórmula é consequência lógica de um conjunto finito de fórmulas.\\
$\psi_1, \ldots, \psi_n \models \Psi$
}
\item {Vimos que a consequência lógica é válida se e só se a implicação\\
$\psi_1 \wedge \psi_2 \wedge \ldots \wedge \psi_n \rightarrow \Psi$ é uma tautologia.
}
\end{itemize}
\subsection*{Para verificar se uma consequência lógica é válida:}
\begin{enumerate}
\item Verificar se a implicação associada é uma tautologia.
\item Verificar se é possível obter (também são usados os termos deduzir, derivar, entre outros) $\Psi$ a partir de $\psi_1, \ldots, \psi_n$, recorrendo a regras de inferência e tautologias conhecidas (propriedades dos conetivos lógicos).\\ (através de uma sequência de deduções em que aplicamos as regras de inferências e tautologias), diz-se que existe uma prova de $\Psi$ a partir de $\psi_1, \ldots, \psi_n$ e escreve-se $\psi_1, \ldots, \psi_n \vdash \Psi$.
\item Aplicar a regra de resolução - Método de resolução.
\end{enumerate}
\subsubsection*{Método de resolução}
A consequência lógica $\psi_1, \ldots, \psi_n \models, \Psi$ é válida se e só se o conjunto de fórmulas {$\psi_1, \ldots, \psi_n, \neg\Psi$} é inconsistente, ou seja, este conjunto contém $\bot$ ou é possível deduzir $\bot$ a partir deste conjunto de fórmulas, isto é, existe uma prova de $\bot$ a partir de $\psi_1,\ldots,\psi_n,\neg\Psi$.
\chapter*{Lógica de 1ª ordem}
\section*{Definição} {
Exemplo de uma fórmula da lógica proposicional:\\
$(p \wedge q) \rightarrow r $\\
Para traduzir frases do tipo:\\
i) \color{red} todos \color{black} os gatos têm garras.\\
ii) \color{red} alguns \color{black} alunos de MD têm 20.\\
\par Passamos da lógica proposicional para a lógica de 1ª ordem (esta última engloba a outra).
}
\section*{Linguagem da lógica de 1ª ordem} {
\subsection*{Alfabeto} {
\begin{enumerate}
\item Variáveis: x, y, z, \ldots;
\item Conetivos lógicos da lógica proposicional: $\wedge, \vee, \rightarrow, \leftrightarrow, \neg, \equiv$;
\item Constantes da lógica proposicional: $\bot e \top$;
\item Os quantificadores $\forall~e~\exists$;
\item O símbolo de igualdade: =;
\item Símbolos de constantes;
\item Símbolos de funções com aridade $n \in N$ (isto é, com $n$ argumentos);
\item Símbolos de predicados.
\end{enumerate}
}
\subsection*{Termo} {
\begin{enumerate}
\item Cada variável e cada símbolo de constante é um termo;
\item { Se f é símbolo de função com aridade $n$ e $t_1, \ldots, t_n$ são termos então $f(t_1, \ldots, t_n)$ é um termo.\\\\
Exemplo: {
\begin{itemize}
\item Variáveis: $x, y, z$;
\item Constantes: $a = 1$, $b = $ Maria, $c = $ Gato tareco;
\item Funções: pai(Maria), onde\\ Pai: $P\rightarrow P$, onde $P$ é o conjunto das pessoas.
\item Predicado: $par(x)="x$ é par\("\), $D=N$\\ $par(2)=1,~~par(3)=0$, etc.
\end{itemize}
Como é que se constroem as fórmulas da lógica de 1.ª ordem?\\
Definição (recursiva) de fórmula:
\begin{itemize}
\item $P(t_1, \ldots, t_n)$ é uma fórmla, considerando $P$ um simbolo de predicado e $t_1,\ldots,t_n$ termos.
\item Se $\psi$ e $\Psi$ sao fórmulas então:\\ $\psi \wedge \Psi$, $\psi \vee \Psi$, $\psi \rightarrow \Psi$, $\psi \leftrightarrow \Psi$, $\neg\psi$, $\bot$ e $\top$ são fórmulas.
\item Se $\psi$ é uma fórmula e $x$ é uma variável então $\forall x \psi$ e $\exists x \psi$ também são fórmulas.
\item Se $t_1$ e $t_2$ são termos então $t_1 = t_2$ é uma fórmula.
\end{itemize}
}
}
\end{enumerate}
}
\subsection*{Átomo} {
Na lógica proposicional, os átomos são as proposições atómicas (ex: $p =$ "chove", $q = $ "vou à aula de MD")\\
\par Os átomos da lógica de 1ª ordem são:
\begin{enumerate}
\item $\bot, \top$
\item $t_1=t_2$, com $t_1$ e $t_2$ termos
\item $P(t_1,\ldots,t_n)$, onde $t_1,\ldots,t_n$ são termos e $P$ é um simbolo de predicado.
\end{enumerate}
\subsubsection*{Exemplo} {
Consideremos os espaços vetoriais estudados na ALGA.\\
O alfabeto inclui:
\begin{itemize}
\item O símbolo de constante o que representa o elemento nulo dos espaço vetorial
\item Símbolos de funções
\begin{enumerate}
\item Para cada $\alpha \in R$, o símbolo de funções\\ $\alpha \cdot \_$\\ que tem aridade 1 correspondente à multiplicação escalar.
\item O símbolo de função + com aridade 2, que corresponde à adição de elementos do espaço vetorial.
\end{enumerate}
\end{itemize}
}
\subsubsection*{Exemplos} {
Converta as seguintes afirmações para linguagem simbólica da lógica de 1ª ordem:
\begin{enumerate}
\item{ \color{red}Todos \color{black} os gatos têm garras.\\
\color{red} $\forall x$ \color{black} [$g(x) \rightarrow t(x)$]\\
\color{red} Universo: $U$ = conjunto dos animais.
}
\item{ \color{red} Alguns \color{black} alunos de MD têm 20.\\
\color{red} $\exists x$ \color{black} ($MD(x) \wedge V(x)$)\\
MD(x) = "x é aluno de MD"\\
V(x) = "x tem 20"
\color{red} Universo: $U$ = alunos da UA em 22/23
}
\end{enumerate}
}
}
}
\section*{Folha 1}
\subsection*{Exercício 2.}
\subsubsection*{c)}
\color{red} Todos \color{black} os insetos são mais leves do que \color{red} algum \color{black} mamífero.~~~~~\color{red} $\forall$ $\exists$\\
\color{black} Predicados:\\
$I(x)$ = ``x é um inseto``\\
$L(y,z)$ = ``y é mais leve do que z``\\
$M(w)$ = ``w é um mamífero``\\
\par $\forall x \left(I(x) \rightarrow \exists y \left( M(y) \wedge L(x, y) \right) \right)$
\par Obs: Alcance de cada quantificador:\\
\begin{itemize}
\item Ocorrência de x ligada: $I(x)$
\item Alcance de $\forall x$: $\left(I(x) \rightarrow \exists y \left( M(y) \wedge L(x, y \right) \right)$
\item Ocorrências de y ligadas: $M(y)$ e $L(x, y)$
\item Alcance de $\exists y$: $\left( M(y) \wedge L(x, y \right)$
\end{itemize}
\chapter*{Fórmula fechada} {
\section*{Definição} {
Fórmula que não tem variáveis com occorrências livres.
\subsection*{Exemplo} {
$\forall x~\exists y~(P(x)~\rightarrow~R(x,y))$ é uma fórmula fechada.
\par $\exists y~((\forall x~P(x))~\wedge~R(x,y))$, esta fórmula não é uma fórmula fechada.
}
\subsection*{Negação de fórmula com quantificadores} {
\begin{enumerate}
\item $\neg (\forall x~\psi)~\equiv~\exists x~\neg \psi$.
\item $\neg (\exists x~\psi)~\equiv~\forall x~\neg \psi$.
\end{enumerate}
$\psi$ - parte da fórmula que está sob o quantificador.
}
}
\section*{Introdução das fórmulas da lógica de 1ª ordem} {
\subsection*{Definição} {
\begin{itemize}
\item Estrututa;
\item Valoração,~~~V:$var~\rightarrow~D$, onde $D$ é o conjunto das variáveis.
\end{itemize}
O conceito de valoração pode ser entendido por forma a podermos considerar a valoração de um termo.\\
$V(a) = a$, se $a$ é uma constante $V(f(t_1,\ldots,t_n)) = f^M(V(t_1),\ldots,V(t_n))$.
\textbf{Obs:} Frequentemente denotamos o símbolo de função $f$ e a função correspondente na estrutura $f^M$, pela mesma letra.
}
\subsection*{Exemplo dos slides} {
$V(M(A, x)) = M^M(V(A), V(x)) = M(A^M, 2) = M(1,2) = |1-2| = |-1| = 1$,~~~~~~$V(A) = A$ porque $A$ é uma constante.
}
}
\section*{Interpretação de fórmulas} {
\subsection*{Exemplo de interpretação de fórmulas (ver slides)} {
\subsubsection*{i)} {
Mostre que $R(x, A)$ não é válida na interpretação $(M,V)$\\
\par Note-se que $\neg (M,V)\models R(x,A)$ se e só se $(M,V) \models \neg R(x,A)$ ($\neg R(x,A)$ é válida na interpretação $(M,V)$)\\
\par $V(\neg R(x,A))\equiv\neg R(V(x),V(A))\equiv\neg R(2, A^M)\equiv\neg R(2, 1)\\\equiv\neg(2 < 1)\equiv\neg\bot\equiv\top $\\Logo, $\neg R(x, A)$ é valida na interpretação $(M,V)$, isto é, $(M,V)\models\neg R(x, A)$\\
Isto é equivalente a afirmar que $R(x,A)$ não é válida nesta interpretação.
}
}
}
}
\chapter*{Forma normal de Skolem} {
\section*{Definição} {
Uma fórmula $\phi$ é dita em forma normal de Skolem se $\phi$ é uma fórmula na forma normal conjuntiva e não contém nenhum quantificador universal.
}
\section*{Exemplo} {
\subsection*{1)} {
$\forall x~P(x, f(x))\wedge\neg R(x) $, onde $f$ é uma função e $R$ e $P$ são predicados.\\
}
\subsection*{2)} {
$\forall x~\forall y~(P(x, f(x)) \wedge (\neg R(x)~\vee~P(x,y)))$
\subsubsection*{Ideia} {
\begin{enumerate}
\item Convertemos $F$ numa fórmula $G$ que está na FNC prenex.\\ Note-se que $F \equiv G$
\item A partir de $G$ obtemos uma fórmula $H$ que está na forma normal de Skolem.
\end{enumerate}
\textbf{Para tal:}\\
\begin{itemize}
\item Se no início da fórmula temos um quantificador do tipo $\exists x$, substituimos todas as ocorrências de $x$ por um símbolo $a$ que represente uma constante e eliminamos o quantificador $\equiv x$.
\item Se na fórmula existe um quantificador existencial $\exists x_k$ com os quantificadores universais $\forall x_1~\forall x_2~\dots~\forall x_{k-1}$, à sua esquerda, substituimos todas as ocorrências de $x_k$ por um símbolo de função que ainda não esteja na fórmula, por exemplo $f$, que tem nos seus argumentos as variáveis $x_1, x_2, \dots, x_{k-1}$, isto é, $x_k$ é substituido por $f(x_1,\ldots,x_{k-1})$.\\\textbf{Atenção:} A fórmula $H$ que obtemos na forma normal de Skolen pode não ser (logicamente) equivalente à fórmula $G$ escrita na FNC prenex ou à fórmula $F$ original.
\end{itemize}
}
}
}
}
\end{document}

View File

@ -1,34 +0,0 @@
# Confirma que o script está a ser executado no diretório correto
# shellcheck disable=SC2164
parent_path=$( cd "$(dirname "${BASH_SOURCE[0]}")" ; pwd -P )
cd "$parent_path"
if [ $# != 1 ]
then
# Isto executa se o comando tiver mais do que 1 argumento
echo "Correct usage: md [class name (may not include spaces!)]"
else
if [ "$1" == "reset" ]
then
# Reinicializa o template usando o git restore
git checkout 657720aba1fa3bde17d30f2021e001a972c18795 -- "$parent_path/template/"
# Termina o script
exit 0
fi
# Cria o diretório da determinada aula
mkdir "classes/$1"
# Copia o conteúdo da aula para o diretório respetivo
cp -a "template/out" "classes/$1"
cp -a "template/src" "classes/$1"
# Reinicializa o template usando o git restore
git checkout 657720aba1fa3bde17d30f2021e001a972c18795 -- "$parent_path/template/"
# Copia o pdf da aula para a pasta que contém todos os pdf
cp "classes/$1/out/main.pdf" "pdf"
mv "pdf/main.pdf" "pdf/$1.pdf"
fi

View File

@ -1,3 +0,0 @@
%! Author = tiagorg
%! Date = 31/01/2023

View File

@ -1,63 +0,0 @@
%! Author = tiagorg
%! Date = 31/01/2023
\documentclass[11pt]{report}
\usepackage{amsmath}
\usepackage[T1]{fontenc} % Fontes T1
\usepackage[utf8]{inputenc} % Input UTF8
\usepackage[backend=biber, style=ieee]{biblatex} % para usar bibliografia
\usepackage{csquotes}
\usepackage[portuguese]{babel} %Usar língua portuguesa
\usepackage{blindtext} % Gerar texto automaticamente
\usepackage{hyperref} % para autoref
\usepackage{graphicx}
\usepackage{indentfirst}
\usepackage[printonlyused]{acronym}
\usepackage{color}
\begin{document}
\def\titulo{Matemática Discreta}
\def\autores{Tiago Garcia}
\def\autorescontactos{tiago.rgarcia@ua.pt}
\def\empresa{Universidade de Aveiro}
\def\logotipo{ua.pdf}
%
\def\tema{}
%
\begin{titlepage}
\begin{center}
\vspace*{50mm}
{\Huge\textbf{\titulo}}\\
\vspace{10mm}
{\Large \empresa}\\
\vspace{10mm}
{\LARGE \autores}\\
\vspace{30mm}
\begin{figure}[h]
\center
\includegraphics{ua}\label{fig:ua-title}
\end{figure}
\vspace{30mm}
\end{center}
\end{titlepage}
\title{
{\LARGE\textbf{\titulo} }\\\\
{\Large \aula\\ \empresa}
}
\author{
\href{https://github.com/TiagoRG}{\autores} \\
\href{mailto:tiago.rgarcia@ua.pt}{\autorescontactos}
}
\date{\today}
\maketitle
\pagenumbering{arabic}
\clearpage
% Content
\end{document}