Index

⊥

1.1

F_Σ

4.3.2

n-expansion

4.3.7.2

T_Σ

4.3.2

v[L : = 1]

2.1.3

2.1.3

Γ[L : = 1]

2.1.3

algèbre de Boole

1.5.1

algorithme d'unification

5.3.2

algorithme DPLL

Plan | 2.3

arbre

1.1.1

Aristote

4.

arité

4.3.1

assignation

1.2.2 | 4.3.3

assignation propositionnelle caractéristique

5.1.2

axiome

6.1.3

Baader, Franz

5.3

base de Herbrand

5.1.1

BDDC

1.7

Boole, George

1.5

brouillon de preuve

3.1.5.1

Church, Alonzo

5. | 6.

clause

1.4 | 2. | 5.2.3

clause minimale pour la conséquence

2.1.6

clause minimale pour la déduction

2.1.5

clause unitaire

2.3.2

complétude pour la réfutation

2.1.3

composition

2.1.1

conclusion

3.1.5.3

conflit

2.3.5.3

conjonction

1.1

connecteur

1. | 1.1

conséquence

1.2.3

consistant

1.2.3

constante

1.1 | 4.3.2 | 4.3.2

contexte

3.1.5.2

contradiction

1.2.3

contre-modèle

1.2.3

contre-modèle d'un ensemble de formules

1.2.3

copie d'une clause

5.4.1.2

Davis, Martin

Plan

déclaration de symbole

4.3.1

déduction

2.

dénombrable

1.2.4

diagramme de décision binaire

1.7

disjonction

1.1

domaine

4.3.3

domaine de Herbrand

5.1.1

égalité booléenne

1.5.3

éléments d'une clause

2.1.1

ensemble de clauses réduites

2.1.4

ensemble de formules insatisfaisable

1.2.3

ensemble de formules satisfaisable

1.2.3

équivalence

1.1

état

4.3.3 | 4.3.3

évaluation

4.3.4.1

expression

5.3.1

facteur

5.4.1.1

faux

1.1

fermeture universelle

5.1.1

fonction

1.2.4

fonction booléenne

1.6

forme clausale

5.2.3

Forme clausale d'un ensemble de formules

5.2.3

forme de Skolem

5.2.1

forme normale

1.4.1

forme normale conjonctive

1.4.3

forme normale disjonctive

1.4.2

formule

1.1.1 | 4.1.1 | 4.3.2

formule à priorité

1.1.2 | 4.1.2

formule atomique

4.1.1 | 4.3.2

formule atomique sur une signature

4.3.2

formule de Peirce

3.2

formule décomposable

1.1.1 | 3.4

formule duale

1.5.3

formule équivalente

1.2.3

formule fermée

4.2.2

formule insatisfaisable

1.2.3

formule propre

5.2.1

formule satisfaisable

1.2.3

formule stricte

no title

formule sur une signature

4.3.2

formule utilisable

3.1.5.3

formules égales à un changement près de variables liées

4.4.3

Gentzen, Gerhard

3. | 3.1.5 | 3.1.5.3

graphe d'implication

2.3.5.4

Herbrand, Jacques

5.

heuristique JW

2.3.5.1

heuristique MOMS

2.3.5.1

heuristique UP

2.3.5.1

Huet, Gérard

5.3

implication

1.1

instanciation

4.3.6

interprétation

4.3.3 | 4.3.3

interprétation d'un ensemble de formules

4.3.3

interprétation de Herbrand

5.1.2

inverse du renommage

5.4.1.2

Kleene, Stephen Cole

4.3.8

ligne de preuve

3.1.5.1

littéral

1.4 | 2.1.1

littéral complémentaire

2.1.1

littéral isolé

2.3.1

littéral négatif

5.2.3

littéral positif

5.2.3

Logemann, George W.

Plan

longueur d'une formule

1.1.1

Loveland, Donald W.

Plan

Martelli, Alberto

5.3

modèle d'un ensemble de formules

1.2.3

modèle d'une formule

1.2.3

modus ponens

3.1.3 | 4.

monôme

1.4

monotonie

2.1.1

Montanari, Ugo

5.3

négation

1.1

occurence libre

4.2.1

occurence liée

4.2.1

ordre de priorité des connecteurs

1.1.2

parenthèse

1.1

Peirce, Charles Sanders

3.2

portée de liaison

4.2.1

Prawitz, Dag

3.5.2

préfixe

1.1.1

préfixe strict

1.1.1

preuve

2.1.1 | 3.1.5.3

preuve d'une formule

3.1.5.3

problème NP-complet

2.3.5

problème 3-SAT

2.3.5

problème SAT

2.3.5

prolongement

1.2.4

Putnam, Hilary

Plan

Raymond, Pascal

Plan

réduction linéaire

2.3.5

règle

3.1

remplacement

1.3.2

renommage

5.4.1.2

résolution

2.

résolution restreinte

2.3.5.2

résolution unitaire

no title

résolvant

2.1.1 | 2.1.1

résolvant au premier ordre

5.4.3

résolvant binaire

5.4.1.3

Robinson, Alan

Plan | 5.3

sens des formules

4.3.4.3

sens des formules atomiques

4.3.4.2

signature

4.3.2

signature associée à un ensemble de formules

4.3.2

signature associée à une formule

4.3.2

Skolem, Thoralf Albert

5.2

skolémisation

5.2

Snyder, Ayne

5.3

Socrate

4.

solution de l'équation

5.3.1

solution la plus générale

5.3.1

solveur SAT

2.3.5

solveur SAT complet

2.3.5

solveur SAT incomplet

2.3.5

sous-clause

2.1.1

sous-formule

1.1.1

stratégie complète

Plan | 2.2

structure paresseuse

2.3.5.6

substitution

1.3.1

substitution à support fini

1.3.1

support d'une substitution

1.3.1

symbole de fonction

4.3.2

symbole de relations

4.3.2

symbole surchargé

4.3.2

table de vérité

1.2.2

taille d'une formule

1.1.1

taille de preuve

2.1.1

tautologie

1.2.3

terme

4.1.1 | 4.3.2

terme sur une signature

4.3.2

théorie

5.2.2

Théry, Laurent

3.5.2

tiers-exclus

1.2.5

Türing, Alan

5. | 6.

unaire

4.3.1

unificateur le plus général

5.3.1

unification

no title

valeur d'une formule

1.2.2

valide

1.2.3

variable

1.1 | 4.3.2

variable libre

4.2.2

variable liée

4.2.2

variable propositionnelle

4.3.2

vrai

1.1