- ... BDDC1.1
- http://www-verimag.imag.fr/~raymond/tools/bddc-manual/bddc-manual-pages.html.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ... droite1.2
- C'est-à-dire
a⇒b⇒c est
l'abréviation de
(a⇒(b⇒c)).
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ... vérité1.3
- Nous laissons le soin au lecteur de se
convaincre de la véracité de ces équivalences en construisant les
tables correspondantes.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ... SAT2.1
- Dans ces programmes, le formalisme 3-SAT est
généralement préféré au formalisme SAT, car son aspect régulier
permet d'obtenir des solutions plus efficaces.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ...Peirce, Charles Sanders3.1
- Charles Sanders Peirce était
un logicien et philosophe américain (1839 - 1914).
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ... syllogisme4.1
- La notion de
syllogisme fut introduite par Aristote et signifie
littéralement «parole (qui va) avec (une autre)», aussi connu
en latin par modus ponendo ponens = «manière d'affirmer,
d'établir en affirmant» et plus brièvement modus ponens.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ... formules4.2
- Attention, x peut ne pas exister
dans A.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ...
ordre4.3
- Notons que dans le livre de Stephen Cole
Kleene [19], cette notion de
substitution sur les variables propositionnelles est étendue à une
substitution plus générale applicable à tous les symboles de
relation.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ... fonction5.1
- En
affirmant l'existence de g, nous utilisons implicitement
l'axiome du choix.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ... >5.2
- Si n = 0,
f est une constante.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ...c5.3
- En affirmant l'existence de g, nous
utilisons implicitement l'axiome du choix.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ... supprim\'ee5.4
- Nous pouvons nous
limiter à la suppression des équations de la forme x = x où x
est une variable.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ... résolues)5.5
- Un algorithme efficace évite ce
remplacement systématique.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.