Accueil🇫🇷Chercher

Élimination de la conjonction

En calcul des propositions, l'élimination de la conjonction (aussi appelé Ã©limination du et, élimination du âˆ§[1], ou simplification)[2] - [3] - [4] est une inférence immédiate valide, sous forme d'argument et de règle d'inférence qui rend la conclusion selon laquelle, si la conjonction A et B est vrai, alors A est vrai et B est vrai. La règle permet de raccourcir les démonstrations en dérivant l'un des conjontifs d'une conjonction sur une ligne par lui-même.

La règle est composée de deux sous-règles distinctes, qui peuvent être exprimées en langage formel:

et

Les deux sous-règles signifient en même temps que, chaque fois qu'une instance "" apparaît sur une ligne d'une démonstration, soit "", soit "" peut être placé sur une ligne subséquente par lui-même.

Notation formelle

Les sous-règles de l'élimination de la conjonction peuvent être écrites en notation séquent:

et

où  est un symbole métalogique qui signifie que  est une déduction logique de  et  est également une conséquence de

et exprimée en tautologies ou en théorèmes de la logique propositionnelle:

et

où  et  sont des propositions exprimées dans un système formel.

Références

  1. (en) David A. Duffy, Principles of Automated Theorem Proving, New York, Wiley, Sect.3.1.2.1, p.46
  2. Copi and Cohen
  3. Moore and Parker
  4. Hurley
Cet article est issu de wikipedia. Text licence: CC BY-SA 4.0, Des conditions supplémentaires peuvent s’appliquer aux fichiers multimédias.