Hacktoberfest 2026: le issue che i maintainer hanno segnato per ottobre, aperte e adatte ai principianti. Sfoglia le issue Hacktoberfest

Typo errors in the sequent calculus and natural deduction sections

Aperta Adatta ai principianti
#437 0 commenti 0 reazioni 0 assegnatari Vedi su GitHub

Nessuno ha ancora preso questa issue.

Valutazione

Difficoltà
2/5
Tempo stimato
1-3 ore
Idoneità per principianti
70/100
Tipo di issue
Documentazione
Chiarezza
Abbastanza chiara
Stato di attività
Attiva
Stack tecnologico
latex
Ambito
documentation

Direzione di ricerca

Inizia dalle tre posizioni indicate nell'issue: content/first-order-logic/sequent-calculus/soundness.tex vicino alle righe 157 e 288, e content/first-order-logic/natural-deduction/proving-things.tex vicino alla riga 133. I numeri di riga si riferiscono a un commit fissato, quindi cerca il testo corrispondente nel file attuale. Prima di modificare, controlla le definizioni delle macro del repository per \Sequent e la convenzione delle etichette delle regole \Intro, perché la prima correzione è aperta a interpretazione. È completato quando i tre passaggi sono corretti e l'etichetta della regola corrisponde alla regola di eliminazione descritta nell'issue.

Scritto dal modello di indicizzazione a partire dal testo della issue.

Descrizione

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

Lingua principale
TeX
Stelle
1.4k
Fork
289
Metriche di merge delle PR
Nessuna PR unita negli ultimi 30g

Preparare l'ambiente

Questo progetto non fornisce container di sviluppo, Dockerfile né guida per i contributori, quindi l'ambiente è a tuo carico: parti dal suo README e consulta la nostra guida al primo contributo per i passaggi generali.

Come iniziare

  1. Leggi tutta la issue e poi la guida ai contributi del progetto.
  2. Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
  3. Fai un fork del repository e lavora su un branch.
  4. Apri una pull request che faccia riferimento al numero della issue.

Altre issue di OpenLogicProject/OpenLogic

Tutte le issue di OpenLogicProject/OpenLogic

Issue simili

Altre issue su Documentation

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.