Annuler
connectez vous
logique en post-bac
- Description de mathématique formelle-termes et relations
- Théorèmes
- Théories logiques
- Équations différentielles : un Cours complet avec des exemples
- Ensemble et application Partie II
- Ensemble et application Partie I
- Espaces vectoriels et Applications linéaires - supérieur
- Généralités sur les matrices, applications linéaires, changement de base, rang d'une matrice - supérieur
Inscription / Connexion Nouveau Sujet
Accueil l'île des mathématiques Forum de mathématiquesListe de tous les forums de mathématiques SupérieurOn parle exclusivement de maths, pour le supérieur principalement, les BTS, IUT, prépas... École ingénieur LogiqueTopics traitant de logique [tout]Lister tous les topics de mathématiques
Niveau école ingénieur
Résolution p V q, non q |-- p
Posté par Vayfen
Bonjour,
J'ai la consigne suivante : par déduction naturelle, déterminez le séquent suivant ;
p V q, non q |-- p
pour le moment je pense qu'il faut supprimer le V.
Cependant, je ne comprends pas bien dans le cours quel(les) doit(doivent) être l'hypothèse pour l'élimination ?
Et quand bien même, que je suppose p ou q, je ne trouve pas p en sortie.
Merci d'avance pour une quelconque aide.
Bonne journée.
Bonjour,
Pourquoi vouloir supprimer V ?
Il est même fondamental.
Si (p ou q) alors on a bien non q implique p.
Ok je pense avoir compris l'idée
mais je ne vois toujours pas comment le formaliser avec la déduction naturelle car pour l'introduction de l'implication il me faudrait selon la formule, avoir q et supposer p (ici je pense qu'il faudrait supposer non q mais selon moi je n'ai rien d'autre sur lequel m'appuyer),
j'espère que j'aurai été clair et merci pour votre aide.
Bonsoir,
de façon informelle : on a p ou q vrai, si q est faux alors p est vrai.
Pour avoir une démonstration formelle il faut connaître le formalisme utilisé.
Le formalisme c'est la "déduction naturelle", je suis allé voir, j'ai décroché dès le début : il faut assimiler la notation.
Si quelqu'un connait ...
C'est bizarre, cette étude de logique formelle en école d'ingénieur, c'est quel type d'étude ?
Au boulot, de collègues utilisaient des méthodes formelles d'écriture de spécifications de logiciel.
L'idée était d'avoir la preuve mathématique de la complétude de et de l'exactitude de l'analyse.
L'objectif était de s'attaquer aux logiciels dits de sécurité. (Aérien, ferroviaire...)
Je n'en sais pas plus. Ainsi, cette description mérite probablement d'être relue 
En fait il faut quand même préciser les règles utilisées.
Par exemple en utilisant le système de règles de ce PDF
il n'y a rien à faire.
Une dernière remarque, peut-être fausse.
J'ai l'impression qu'il faut faire une déduction non intuitionniste c'est à dire utiliser une règle de raisonnement par l'absurde.
Le lien réparé :
On voit que la démonstration demandée se résume à utiliser la règle d'élimination de .
Bonjour,
Où peut-on trouver une définition des notations utilisées ?
J'ai réussi à en trouver des brides, auriez-vous un lien qui donne ces notations de manière un peu plus exhaustive ?
Bonsoir gts2.
Les notations utilisées en déduction naturelle ne sont pas définies, bien que l'on sache qu'elles sont faites pour représenter le sens usuel d'icelles.
On a juste des règles de manipulation qui varient suivant les auteurs, la règle la plus sujette à variation étant celle d'élimination de ( ou ).
L'écriture signifiant que l'on peut démontrer
à partir des hypothèses
.
Par exemple la règle de Wikipédia
est immédiatement équivalente à la règle