| Information | |
|---|---|
| has gloss | eng: In proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934 as a tool for studying natural deduction in first-order logic (in classical and intuitionistic versions, respectively). Gentzens so-called "Main Theorem" (Hauptsatz) about LK and LJ was the cut-elimination theorem, a result with far-reaching meta-theoretic consequences, including consistency. Gentzen further demonstrated the power and flexibility of this technique a few years later, applying a cut-elimination argument to give a (transfinite) proof of the consistency of Peano arithmetic, in surprising response to Gödels incompleteness theorems. Since this early work, sequent calculi (also called Gentzen systems) and the general concepts relating to them have been widely applied in the fields of proof theory, mathematical logic, and automated deduction. |
| lexicalization | eng: sequent calculus |
| instance of | e/Formal methods |
| Meaning | |
|---|---|
| German | |
| lexicalization | deu: Sequenzenkalkül |
| French | |
| has gloss | fra: En logique mathématique et plus précisément en théorie de la démonstration, le calcul des séquents est un système de déduction créé par Gerhard Gentzen . |
| lexicalization | fra: Calcul des sequents |
| lexicalization | fra: calcul des séquents |
| Japanese | |
| has gloss | jpn: シークエント計算（）は、一階述語論理や特殊な命題論理で広く用いられる演繹手法である。類似の手法もシークエント計算と呼ぶことがあるので、LK と呼んで区別することがある。また類似の手法も含め、総称してゲンツェン・システムとも呼ばれる。 |
| lexicalization | jpn: シークエント計算 |
| Polish | |
| has gloss | pol: Sekwenty Gentzena to jeden z najprostszych sposobów automatycznego dowodzenia twierdzeń rachunku zdań. Został opracowany przed Gerharda Gentzena w 1934 roku. Znany jest również pod nazwą system LK od niemieckiej nazwy Logischer Kalkül. Jest to jednocześnie jedna z formalizacji rachunku predykatów |
| lexicalization | pol: Sekwenty Gentzena |
| Ukrainian | |
| has gloss | ukr: Чи́слення секве́нцій — система формального виведення формул логіки першого порядку (і як часткового випадку логіки висловлень) запропонована німецьким логіком Генріхом Генценом. Після праці Генцена розроблено кілька варіантів числення секвенцій, що є еквівалентними між собою і альтернативою аксіоматичному підходу. |
| lexicalization | ukr: числення секвенцій |
| Chinese | |
| has gloss | zho: 在证明论和数理逻辑中，相继式演算是众所周知的一阶逻辑(和作为它的特殊情况的命题逻辑)的演绎系统。这个系统也叫做 LK 系统，用以区别于后来建立的有时也叫做相继式演算的类似风格的各种其他系统。另一个给这种系统的术语是 Gentzen 系统。 |
| lexicalization | zho: 相继式演算 |
| Media | |
|---|---|
| media:img | Excluded middle proof.png |
| media:img | LK dem contraposition.png |
Lexvo © 2008-2024 Gerard de Melo. Contact Legal Information / Imprint
