| rdfs:comment
| - シークエント計算（シークエントけいさん、英: Sequent calculus）は、一階述語論理や特殊な命題論理で広く用いられる演繹手法である。類似の手法もシークエント計算と呼ぶことがあるので、LK と呼んで区別することがある。また類似の手法も含め、総称してゲンツェン・システムとも呼ばれる。 シークエント計算とその概念全般は証明論や数理論理学において重要な意味を持つ。以下では LK について解説する。 (ja)
- 시퀀트 계산(sequent calculus)은 1차 논리나 특수한 명제 논리에서 쓰이는 연역 계산법의 일종으로, 논리식으로 이루어진 특수한 열인 시퀀트를 이용한다. 유사한 수법까지 총칭하여 겐첸 체계(Gentzen system)라고도 불리며, 다른 것들과 구분하기 위해 LK라 특별히 일컫기도 한다. 자연 연역과 유사하게 이미 제시된 식들로부터 추론 규칙에 근거한 추론을 행하여 새로운 식을 이끌어내는 방식이며, 이는 공리에 근거하여 정리들을 나열하는 방식의 증명법을 가진 (Hilbert System)와는 대비된다. 시퀀트(sequent)란 논리식의 나열인데, 전건의 명제들의 논리곱을 전제로 삼고 후건의 명제들의 논리합을 귀결로 삼는 것이 특징이다. 곧, "A이고 B이고 C이고 D이고... 이면, (가)이거나 (나)이거나 (다)이거나 (라)이거나...이다."와 같은 식이다. 시퀀트 계산에서 증명은 일련의 시퀀트들의 나열로 기술되는데, 각 시퀀트는 증명과정에서 이미 출현한 시퀀트에 특정 추론규칙을 적용하는 것으로써 도출된다. (ko)
- Чи́слення секве́нцій — система формального виведення формул логіки першого порядку (і як часткового випадку логіки висловлень) запропонована німецьким логіком Ґергардом Ґенценом. Після праці Ґенцена розроблено кілька варіантів числення секвенцій, що є еквівалентними між собою і альтернативою аксіоматичному підходу. (uk)
- 在证明论和数理逻辑中，相继式演算（又译矢列演算、矢列式演算、序贯演算）是一阶逻辑（和作为它的特殊情况的命题逻辑）、模态逻辑等逻辑的一类。第一个相继式演算和由格哈德·根岑（Gerhard Gentzen）在1934年/1935年引入，作为研究自然演绎的工具；它的名字得来自德语的“Logischer Kalkül”，意思是“逻辑演算”。相继式演算系统有时被称为Gentzen系统，但使用时应避免与同为Gentzen发明的证明演算自然演绎混淆。自然演绎、公理系统和相继式演算是常见的证明演算。 相继式演算是逻辑研究的重要工具。许多逻辑学者会为其所研究的逻辑构造出一个或多个相继式演算，并研究其性质（如切消定理）。 (zh)
- En pruva teorio kaj , la sekvaĵa kalkulo estas larĝe sciata konkluda sistemo por (kaj kiel speciala okazo de ĝi). La sistemo estas ankaŭ konata sub la nomo LK, distinganta ĝin de diversaj aliaj sistemoj de simila maniero, kiuj estas kreitaj poste kaj kiuj estas iam ankaŭ nomitaj sekvaĵaj kalkuloj. Alia termino por tiaj sistemoj en ĝeneralo estas gentzen-sistemoj. (eo)
- El cálculo de secuentes es, en esencia, un estilo de argumentación lógica formal donde cada línea de la demostración es una tautología condicional (llamada secuente por Gerhard Gentzen) en vez de una tautología no condicional. Cada tautología condicional se infiere de otras tautologías condicionales en líneas anteriores de la demostración, de acuerdo a reglas y procedimientos de inferencia, dando así una mejor aproximación al estilo de deducción natural utilizado por los matemáticos que el estilo de David Hilbert, donde cada línea era una tautología no condicional. Puede que haya distinciones más sutiles: por ejemplo, podría haber axiomas no lógicos sobre los que todas las proposiciones son implícitamente dependientes. Entonces los secuentes son teoremas condicionales en un lenguaje de pri (es)
- In der Beweistheorie und der mathematischen Logik bezeichnet man mit Sequenzenkalkül formale Systeme (oder Kalküle), die einen bestimmten Stil der Ableitung und gewisse Eigenschaften teilen. Die ersten Sequenzenkalküle, LK für die klassische und LJ für die intuitionistische Logik, sind von Gerhard Gentzen im Jahre 1934 als formaler Rahmen für die Untersuchung von Systemen des natürlichen Schließens in der Prädikatenlogik 1. Ordnung eingeführt worden. (de)
- 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. Le nom de ce formalisme fait référence à un style particulier de déduction ; le système original a été adapté à diverses logiques, telles que la logique classique, la logique intuitionniste et la logique linéaire. Un séquent est une suite d'hypothèses suivie d'une suite de conclusions, les deux suites étant usuellement séparées par le symbole (taquet droit), « : » (deux-points) ou encore (flèche droite) dans l'œuvre originale de Gentzen. (fr)
- In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautology is inferred from other conditional tautologies on earlier lines in a formal argument according to rules and procedures of inference, giving a better approximation to the natural style of deduction used by mathematicians than to David Hilbert's earlier style of formal logic, in which every line was an unconditional tautology. More subtle distinctions may exist; for example, propositions may implicitly depend upon non-logical axioms. In that case, sequents signify conditional theorems in a first-order language rather than conditional tautologies. (en)
- Sekwenty Gentzena – jeden z najprostszych sposobów automatycznego dowodzenia twierdzeń rachunku zdań. Został opracowany przez 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. Każdy sekwent składa się ze zbioru {ai} poprzedników i zbioru {bj} następników, połączonych zależnością (którą mamy udowodnić) – jeśli wszystkie ai są prawdziwe, to któreś z bi jest prawdziwe. Wykonujemy następujące kroki: Przykład działania: (pl)
- Na teoria da prova e lógica matemática, o cálculo de sequentes é um grupo de sistemas formais que compartilham de um certo estilo de inferência e propriedades formais. Os primeiros cálculos de sequente, os sistemas LK e LJ, foram introduzidos por Gerhard Gentzen em 1934 como uma ferramenta para o estudo de dedução natural na lógica de primeira ordem (nas versões clássica e intuicionista, respectivamente). O teorema de Gentzen chamado de "Teorema Principal" sobre LK e LJ foi o teorema do corte, um resultado com longo alcance nas consequências da metateoria, incluindo a consistência. Alguns anos depois, Gentzen demonstrou ainda mais o poder e a flexibilidade dessa técnica, aplicando o argumento da eliminação de corte para dar uma prova(transfinita) da consistência da aritmética de Peano, num (pt)
- Исчисление секвенций — вариант логических исчислений, использующий для доказательства утверждений не произвольные цепочки тавтологий, а последовательности условных суждений — секвенций. Наиболее известные исчисления секвенций — и для классического и интуиционистского исчислений предикатов — построены Генценом в 1934 году, позднее сформулированы секвенциальные варианты для широкого класса прикладных исчислений (арифметики, анализа), теорий типов, неклассических логик. (ru)
|
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)
![[RDF Data]](/fct/images/sw-rdf-blue.png)