« Élimination de la conjonction » : différence entre les versions

Navigation interactive dans l’historique

← Modification précédente

Contenu supprimé Contenu ajouté

VisuelWikicode

Intégrés

Dernière version du 10 mars 2021 à 13:13

Si ce bandeau n'est plus pertinent, retirez-le. Cliquez ici pour en savoir plus.

Cet article doit être recyclé (novembre 2016).

Une réorganisation et une clarification du contenu paraissent nécessaires. Améliorez-le, discutez des points à améliorer ou précisez les sections à recycler en utilisant {{section à recycler}}.

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^[Quoi ?] 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.^[pas clair] La règle permet de raccourcir les démonstrations en dérivant l'un des conjontifs^[Quoi ?] d'une conjonction sur une ligne^[Quoi ?] par lui-même.

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

{\frac {P\land Q}{\therefore P}}

et

{\frac {P\land Q}{\therefore Q}}

Les deux sous-règles signifient en même temps que, chaque fois qu'une instance " $P\land Q$ " apparaît sur une ligne^[Quoi ?] d'une démonstration, soit " $P$ ", soit " $Q$ " peut être placé sur une ligne subséquente^[Quoi ?] par lui-même^[Qui ?].

Notation formelle^{[pourquoi ?]}[modifier | modifier le code]

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

(P\land Q)\vdash P

et

(P\land Q)\vdash Q

où $\vdash$ est un symbole métalogique^[pas clair] qui signifie que $P$ est une déduction logique de $P\land Q$ et $Q$ est également une conséquence de $P\land Q$

et exprimée en tautologies^[Quoi ?] ou en théorèmes de la logique propositionnelle:

(P\land Q)\to P

et

(P\land Q)\to Q

où $P$ et $Q$ sont des propositions exprimées dans un système formel^[Lequel ?].

Références[modifier | modifier le code]

(en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Conjunction elimination » (voir la liste des auteurs).

↑ (en) David A. Duffy, Principles of Automated Theorem Proving, New York, Wiley, 1991 Sect.3.1.2.1, p.46
↑ Copi and Cohen ^{[citation nécessaire]}
↑ Moore and Parker ^{[citation nécessaire]}
↑ Hurley ^{[citation nécessaire]}

Portail de la logique

[1] (en) David A. Duffy, Principles of Automated Theorem Proving, New York, Wiley, 1991 Sect.3.1.2.1, p.46

[2] Copi and Cohen ^{[citation nécessaire]}

[3] Moore and Parker ^{[citation nécessaire]}

[4] Hurley ^{[citation nécessaire]}

[1]

[2]

[3]

[4]

@@ Ligne 1 : / Ligne 1 : @@
-{{à recycler |date=3 novembre 2016}}
+{{à recycler |date=novembre 2016|thème=logique}}
-En [[calcul des propositions]], l'<nowiki/>'''élimination de la conjonction '''(aussi appelé '''élimination du ''et''''', '''élimination du''' '''∧'''<ref>{{cite book | author=David A. Duffy | title=Principles of Automated Theorem Proving | location=New York | publisher=Wiley | year=1991 }} Sect.3.1.2.1, p.46</ref>, ou '''simplification''')<ref>Copi and Cohen
+En [[calcul des propositions]], l'<nowiki/>'''élimination de la conjonction '''(aussi appelé '''élimination du ''et''''', '''élimination du''' '''∧'''<ref>{{Ouvrage|langue=en|auteur1=David A. Duffy|titre=Principles of Automated Theorem Proving|lieu=New York|éditeur=[[John Wiley & Sons|Wiley]]|année=1991|isbn=}} Sect.3.1.2.1, p.46</ref>, ou '''simplification''')<ref>Copi and Cohen
-<sup class="noprint Inline-Template Template-Fact" style="white-space:nowrap;">&#x5B;''[[Aide:Citation nécessaire|<span title="Without title, this is hardly a useful reference. (February 2014)">citation needed</span>]]''&#x5D;</sup></ref>{{,}}<ref>Moore and Parker
+{{Citation nécessaire|date=février 2014}}</ref>{{,}}<ref>Moore and Parker
+{{Citation nécessaire|date=février 2014}}</ref>{{,}}<ref>Hurley
-<sup class="noprint Inline-Template Template-Fact" style="white-space:nowrap;">&#x5B;''[[Aide:Citation nécessaire|<span title="This claim needs references to reliable sources. (February 2014)">citation needed</span>]]''&#x5D;</sup></ref>{{,}}<ref>Hurley
-<sup class="noprint Inline-Template Template-Fact" style="white-space:nowrap;">&#x5B;''[[Aide:Citation nécessaire|<span title="This claim needs references to reliable sources. (February 2014)">citation needed</span>]]''&#x5D;</sup></ref>est une {{quoi | [[inférence immédiate]]}} [[valide]], {{pas clair | 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émonstration formelle|démonstrations]] en dérivant l'un des {{quoi | conjontifs}} d'une conjonction {{quoi | sur une ligne}} par lui-même.
+{{Citation nécessaire|date=février 2014}}</ref> est une {{quoi | [[inférence immédiate]]}} [[valide]], {{pas clair | 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émonstration formelle|démonstrations]] en dérivant l'un des {{quoi | conjontifs}} d'une conjonction {{quoi | sur une ligne}} par lui-même.
 La règle est composée de deux {{quoi |sous-règles}} distinctes, qui peuvent être exprimées en {{comment | [[langage formel]]}}:
@@ Ligne 12 : / Ligne 12 : @@
 == {{pourquoi | Notation formelle}} ==
-Les sous-règles de l'''élimination de la conjonction ''peuvent être écrites en notation {{quoi | séquent}}:
+Les {{quoi | sous-règles}} de l'''élimination de la conjonction ''peuvent être écrites en notation {{quoi | séquent}}:
 : <math>(P \land Q) \vdash P</math>
 et
 : <math>(P \land Q) \vdash Q</math>
-où <math>\vdash</math> est un {{pas clair | symbole [[métalogique]]}} qui signifie que <math>P</math> est une [[déduction logique]] de <math>P \land Q</math> et <math>Q</math> est également une conséquence <math>P \land Q</math>
+où <math>\vdash</math> est un {{pas clair | symbole [[métalogique]]}} qui signifie que <math>P</math> est une [[déduction logique]] de <math>P \land Q</math> et <math>Q</math> est également une conséquence de <math>P \land Q</math>
-et exprimée en {{quoi | [[Tautologie|tautologies]]}} ou en[[ théorèmes]] de la logique propositionnelle:
+et exprimée en {{quoi | [[tautologie]]s}} ou en [[théorèmes]] de la logique propositionnelle:
 : <math>(P \land Q) \to P</math>
 et
 : <math>(P \land Q) \to Q</math>
-où <math>P</math> et <math>Q</math> sont des propositions exprimées dans un [[système formel]].
+où <math>P</math> et <math>Q</math> sont des propositions exprimées dans un {{lequel | [[système formel]]}}.
 == Références ==
 {{Traduction/Référence|lang1=en|art1=Conjunction elimination|id1=662661702}}
-{{Reflist}}
+{{Références}}
-{{Palette Règles de transformation}}
+{{Palette|Règles de transformation}}
 {{Portail|logique}}

Dernière version du 10 mars 2021 à 13:13

Notation formelle[pourquoi ?][modifier | modifier le code]

Références[modifier | modifier le code]

Notation formelle^{[pourquoi ?]}[modifier | modifier le code]