Hacktoberfest 2026 : les issues que les mainteneurs ont marquées pour octobre, ouvertes et accessibles aux débutants. Parcourir les issues Hacktoberfest

Typo errors in the sequent calculus and natural deduction sections

Ouverte Adaptée aux débutants
  • Quelque chose ne va pas ?
#437 0 commentaires 0 réactions 0 personnes assignées Voir sur GitHub

Personne n'a encore pris cette issue.

Évaluation

Difficulté
2/5
Temps estimé
1-3 heures
Accessibilité débutants
70/100
Type d'issue
Documentation
Clarté
Plutôt claire
Activité
Active
Stack technique
latex
Domaine
documentation

Piste de recherche

Commence par les trois emplacements mentionnés dans l'issue : content/first-order-logic/sequent-calculus/soundness.tex près des lignes 157 et 288, et content/first-order-logic/natural-deduction/proving-things.tex près de la ligne 133. Les numéros de ligne renvoient à un commit épinglé, retrouve donc le texte correspondant dans le fichier actuel. Avant de modifier, vérifie les définitions de macros du dépôt pour \Sequent et la convention d'étiquetage des règles \Intro, car la première correction se prête à interprétation. C'est terminé lorsque les trois passages sont corrigés et que l'étiquette de règle correspond à la règle d'élimination décrite dans l'issue.

Rédigé par le modèle d'indexation à partir du texte de l'issue.

Description

First typo:
Typo location:
https://github.com/OpenLogicProject/OpenLogic/blob/1e960beff9ed7835bf3e3f1335e21af3439cd107/content/first-order-logic/sequent-calculus/soundness.tex#L157

What is the typo:
Writing the contexts rather than the entire sequent

Proposed correction:
The symbols should be preceded by the conjunction and comma, or simply the entire sequent should be theta and xi

Second typo:
Typo location:
https://github.com/OpenLogicProject/OpenLogic/blob/1e960beff9ed7835bf3e3f1335e21af3439cd107/content/first-order-logic/sequent-calculus/soundness.tex#L288

What is the typo:
wrong symbol ($\setminus$) for the sequent symbol

Proposed correction:
The symbol should be $\Rightarrow$ or in this doc $\Sequent$

Third typo:
Typo location:
https://github.com/OpenLogicProject/OpenLogic/blob/1e960beff9ed7835bf3e3f1335e21af3439cd107/content/first-order-logic/natural-deduction/proving-things.tex#L133

What is the typo:
The symbol "\Intro{\lfalse}"

Proposed correction:
It should be ~elim not "Intro $\bot$" which is here written as "\Intro{\lfalse}", and "\Intro{\lfalse}" is not a rule used anywhere else in the repo as far as I can tell

Langage dominant
TeX
Étoiles
1.4k
Forks
289
Aucune PR mergée en 30 j

Préparer son environnement

Ce projet ne fournit ni conteneur de développement, ni Dockerfile, ni guide de contribution : l'installation est à votre charge. Commencez par son README, et consultez notre guide de la première contribution pour les étapes générales.

Par où commencer

  1. Lisez l'issue en entier, puis le guide de contribution du projet.
  2. Signalez en commentaire que vous la prenez — cela évite que deux personnes fassent le même travail.
  3. Forkez le dépôt et travaillez sur une branche.
  4. Ouvrez une pull request qui référence le numéro de l'issue.

Autres issues de OpenLogicProject/OpenLogic

Toutes les issues de OpenLogicProject/OpenLogic

Issues similaires

Plus d'issues Documentation

Recevez les nouvelles issues par e-mail

Un résumé court des issues GitHub adaptées aux débutants.