Recherche:Théorie des matrices logiques/Choix d'un invariant
| La validité des opérations de la TML se fonde sur le choix d'un invariant. Il peut s'agir de la table, ou d'une projection. |
Par définition, tous les éléments de la matrice logique sont dans un état déterminé. En fonction du contexte, certains éléments, dits transfuges, possèdent cependant la propriété de pouvoir changer d'état sans que la table
n'en soit affectée. Ces éléments, qu’ils soient initialement des 0 ou des 1, sont dépistés au moyen d'une preuve logique.
Dans la première bande horizontale de la matrice logique de l’ensemble E deux 1 peuvent être convertis en 0 (fermeture de transfuges):
De son côté, l'opération de séparation prend pour invariant l'une des projections primaires:
- et les tables des vecteurs n'ont plus de 1 en commun.
- La transformation n'a pas ici pour cadre l’ensemble de clauses, mais s'effectue à l'intérieur d'une clause, au niveau subatomique. La logique propositionnelle, quant à elle, s'arrête au concept d'atome.
- Cette différence est essentielle à la compréhension de certaines opérations. Elle est aussi en grande partie responsable du 'surcroît de capacité analytique' évoqué dans le résumé.
Replacée dans la matrice logique de l’ensemble E, la bande modifiée n'affecte pas la projection 1:
En revanche, la table et la projection 2 (cinq 0 ont remplacé des 1 dans sa partie inférieure) ont été modifiées.
Par voie de conséquence, l’ensemble E' a également été modifié: la décomposition fera apparaître de nouvelles clauses.
