« Élimination de la conjonction » : différence entre les versions
catégorisation |
Aucun résumé des modifications |
||
Ligne 1 : | Ligne 1 : | ||
{{à recycler |date=novembre 2016|thème= |
{{à 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>{{ouvrage|langue=en| auteur=David A. Duffy | titre=Principles of Automated Theorem Proving | lieu=New York | éditeur=Wiley | année=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| auteur=David A. Duffy | titre=Principles of Automated Theorem Proving | lieu=New York | éditeur=Wiley | année=1991 }} Sect.3.1.2.1, p.46</ref>, ou '''simplification''')<ref>Copi and Cohen |
||
{{Citation nécessaire|date=février 2014}}</ref>{{,}}<ref>Moore and Parker |
{{Citation nécessaire|date=février 2014}}</ref>{{,}}<ref>Moore and Parker |
Version du 21 juillet 2020 à 12:35
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 ?]:
et
Les deux sous-règles signifient en même temps que, chaque fois qu'une instance "" apparaît sur une ligne[Quoi ?] d'une démonstration, soit "", soit "" peut être placé sur une ligne subséquente[Quoi ?] par lui-même[Qui ?].
Notation formelle[pourquoi ?]
Les sous-règles[Quoi ?] de l'élimination de la conjonction peuvent être écrites en notation séquent[Quoi ?]:
et
où est un symbole métalogique[pas clair] qui signifie que est une déduction logique de et est également une conséquence de
et exprimée en tautologies[Quoi ?] ou enthéorèmes de la logique propositionnelle:
et
où et sont des propositions exprimées dans un système formel[Lequel ?].
Références
- (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, Sect.3.1.2.1, p.46
- Copi and Cohen [citation nécessaire]
- Moore and Parker [citation nécessaire]
- Hurley [citation nécessaire]