Next:
Contents
Contents
Introducció a la deducció natural
Daniel Clemente Laboreo
Agost 2004 (revisat en Maig 2005)
Contents
1
Abans de res...
1
.
1
Qui soc
1
.
2
Per què escric això
1
.
3
A qui va dirigit
1
.
4
Llicència
2
Conceptes bàsics
2
.
1
Formalització
2
.
2
Símbols usats
2
.
3
Precedència dels operadors
3
Deducció natural
3
.
1
Per a què serveix
3
.
2
Per a què no serveix
3
.
3
Funcionament
3
.
4
Notació
4
Les regles
4
.
1
Iteració
4
.
2
Introducció de la conjunció
4
.
3
Eliminació de la conjunció
4
.
4
Introducció de la implicació
4
.
5
Eliminació de la implicació
4
.
6
Introducció de la disjunció
4
.
7
Eliminació de la disjunció
4
.
8
Introducció de la negació
4
.
9
Eliminació de la negació
4
.
10
No hi ha més regles
5
Exercicis explicats
5
.
1
Un molt senzill.
5
.
2
Una mica més complicat.
5
.
3
Començant a suposar coses.
5
.
4
Usant la iteració.
5
.
5
Reducció a l'absurd.
5
.
6
Amb subdemostracions.
5
.
7
Un de prova per casos.
5
.
8
Un per pensar-hi.
5
.
9
La part esquerra buida.
5
.
10
Suposar el contrari.
5
.
11
Aquest sembla fàcil.
5
.
12
Un d'interessant.
5
.
13
Aquest me'l van posar a un examen.
5
.
14
Un ``curt''.
6
Coses incorrectes
6
.
1
Introducció i eliminació d'
``allò que em vagi bé''
6
.
2
Iterar una fórmula d'una subdemostració no accesible
6
.
3
Posar malament els parèntesis
6
.
4
Acabar dins d'una subdemostració
6
.
5
Saltar-se passos
7
Complicant-ho una mica més
7
.
1
Regles de cert i fals
7
.
1
.
1
Introducció de cert
7
.
1
.
2
Eliminació de fals
7
.
2
Regles de quantificadors
7
.
2
.
1
Què és això
7
.
2
.
2
Introducció de l'existencial
7
.
2
.
3
Eliminació de l'existencial
7
.
2
.
4
Introducció de l'universal
7
.
2
.
5
Eliminació de l'universal
7
.
2
.
6
Exemples
7
.
3
Regles derivades
8
Extra
8
.
1
Per què es diu deducció natural?
8
.
2
La solució és única?
8
.
3
Altres formes de demostrar validesa
8
.
3
.
1
Força bruta
8
.
3
.
2
Teorema de refutació
8
.
4
Com demostrar la invalidesa
8
.
5
Fes-te els teus exercicis
8
.
6
Programes que facin deducció natural
9
Exemples, molts exemples
9
.
1
9
.
2
9
.
3
9
.
4
9
.
5
9
.
6
9
.
7
9
.
8
9
.
9
9
.
10
9
.
11
9
.
12
9
.
13
9
.
14
9
.
15
9
.
16
9
.
17
9
.
18
9
.
19
9
.
20
9
.
21
9
.
22
9
.
23
9
.
24
9
.
25
9
.
26
About this document ...
Daniel Clemente Laboreo 2005-05-17