| dbo:abstract
|
- 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. Der Gentzensche Hauptsatz über LK und LJ besagt, dass die Schnittregel in diesen Systemen gilt, ein Satz mit weitreichenden Konsequenzen in der Metalogik. Die Flexibilität des Sequenzenkalküls zeigte sich später, im Jahr 1936, als Gentzen die Technik der Schnitt-Elimination verwendete, um die Widerspruchsfreiheit der Peano-Arithmetik zu beweisen. Die auf Gentzen zurückgehenden Sequenzenkalküle und die allgemeinen Konzepte, die dahinterstehen, werden in weiten Bereichen der Beweistheorie, mathematischen Logik und des maschinengestützten Beweisens standardmäßig verwendet. (de)
- 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. Ĉar sekvaĵaj kalkuloj kaj la ĝeneralaj konceptoj rilatante al ili estas de majora graveco al la tuta kampo de pruva teorio kaj matematika logiko, la sistemo LK estos eksplikita en pli granda detalo pli sube. Iu familiareco kun la bazaj nocioj de predikata logiko (aparte ĝia sintaksa strukturo) estas alprenita. (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 primer orden, en vez de tautologías condicionales.
* Datos: Q1771121 (es)
- 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. Un séquent représente une étape d'une démonstration, le calcul des séquents explicitant les opérations possibles sur ce séquent en vue d'obtenir une démonstration complète et correcte. (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. Sequent calculus is one of several extant styles of proof calculus for expressing line-by-line logical arguments.
* Hilbert style. Every line is an unconditional tautology (or theorem).
* Gentzen style. Every line is a conditional tautology (or theorem) with zero or more conditions on the left.
* Natural deduction. Every (conditional) line has exactly one asserted proposition on the right.
* Sequent calculus. Every (conditional) line has zero or more asserted propositions on the right. In other words, natural deduction and sequent calculus systems are particular distinct kinds of Gentzen-style systems. Hilbert-style systems typically have a very small number of inference rules, relying more on sets of axioms. Gentzen-style systems typically have very few axioms, if any, relying more on sets of rules. Gentzen-style systems have significant practical and theoretical advantages compared to Hilbert-style systems. For example, both natural deduction and sequent calculus systems facilitate the elimination and introduction of universal and existential quantifiers so that unquantified logical expressions can be manipulated according to the much simpler rules of propositional calculus. In a typical argument, quantifiers are eliminated, then propositional calculus is applied to unquantified expressions (which typically contain free variables), and then the quantifiers are reintroduced. This very much parallels the way in which mathematical proofs are carried out in practice by mathematicians. Predicate calculus proofs are generally much easier to discover with this approach, and are often shorter. Natural deduction systems are more suited to practical theorem-proving. Sequent calculus systems are more suited to theoretical analysis. (en)
- シークエント計算（シークエントけいさん、英: Sequent calculus）は、一階述語論理や特殊な命題論理で広く用いられる演繹手法である。類似の手法もシークエント計算と呼ぶことがあるので、LK と呼んで区別することがある。また類似の手法も含め、総称してゲンツェン・システムとも呼ばれる。 シークエント計算とその概念全般は証明論や数理論理学において重要な意味を持つ。以下では LK について解説する。 (ja)
- 시퀀트 계산(sequent calculus)은 1차 논리나 특수한 명제 논리에서 쓰이는 연역 계산법의 일종으로, 논리식으로 이루어진 특수한 열인 시퀀트를 이용한다. 유사한 수법까지 총칭하여 겐첸 체계(Gentzen system)라고도 불리며, 다른 것들과 구분하기 위해 LK라 특별히 일컫기도 한다. 자연 연역과 유사하게 이미 제시된 식들로부터 추론 규칙에 근거한 추론을 행하여 새로운 식을 이끌어내는 방식이며, 이는 공리에 근거하여 정리들을 나열하는 방식의 증명법을 가진 (Hilbert System)와는 대비된다. 시퀀트(sequent)란 논리식의 나열인데, 전건의 명제들의 논리곱을 전제로 삼고 후건의 명제들의 논리합을 귀결로 삼는 것이 특징이다. 곧, "A이고 B이고 C이고 D이고... 이면, (가)이거나 (나)이거나 (다)이거나 (라)이거나...이다."와 같은 식이다. 시퀀트 계산에서 증명은 일련의 시퀀트들의 나열로 기술되는데, 각 시퀀트는 증명과정에서 이미 출현한 시퀀트에 특정 추론규칙을 적용하는 것으로써 도출된다. (ko)
- 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. Dowodzenie zaczyna się od jednego sekwentu z pustym zbiorem poprzedników i zbiorem następników składających się z twierdzenia, które zamierzamy udowodnić. Wykonujemy następujące kroki:
* złożone zależności, takie jak implikacja, równoważność itd. zastępujemy alternatywami, koniunkcjami i negacjami;
* następnik będący alternatywą (M ∨ N) zastępujemy dwoma następnikami: M, N;
* poprzednik będący koniunkcją (M ∧ N) zastępujemy dwoma poprzednikami: M, N;
* następnik będący negacją (¬ M) zastępujemy poprzednikiem bez negacji: M;
* poprzednik będący negacją (¬ M) zastępujemy następnikiem bez negacji: M;
* jeśli kilka następników jest identycznych można zachować tylko jeden z nich;
* jeśli kilka poprzedników jest identycznych można zachować tylko jeden z nich;
* jeśli następnik jest koniunkcją (M ∧ N) zamieniamy sekwent na dwa, o tych samych poprzednikach, i następniku (M ∧ N) zastąpionym odpowiednio przez M i N;
* analogicznie, jeśli poprzednik jest alternatywą (M ∨ N) zamieniamy sekwent na dwa, o tych samych następnikach, i poprzedniku (M ∨ N) zastąpionym odpowiednio przez M i N;
* jeśli wszystkie następniki i poprzedniki sekwentu są zmiennymi zdaniowymi i żadna z nich nie występuje jednocześnie w następniku i poprzedniku, twierdzenie jest fałszywe;
* jeśli wszystkie następniki i poprzedniki sekwentu są zmiennymi zdaniowymi i chociaż jedna z nich występuje jednocześnie w następniku i poprzedniku, sekwent jest poprawny i przystępujemy do analizy kolejnego sekwentu; jeśli był to już ostatni sekwent twierdzenie jest prawdziwe. Przykład działania:
* {}, {p ∨ ¬ p} – rozbijamy alternatywę w następniku
* {}, {p, ¬ p} – przenosimy negację na drugą stronę
* {p}, {p} – zmienna p się powtarza
* prawda W logice pierwszego rzędu można pokazać zupełność i poprawność systemu Gentzena. (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, numa resposta surpreendente aos teoremas de incompletude de Gödel. Desde esse trabalho inicial, o cálculo de sequentes(também conhecido como sistemas de Gentzen) e os conceitos gerais relativos a ele são amplamente aplicados nos campos da teoria de prova, lógica matemática e dedução automática. (pt)
- Чи́слення секве́нцій — система формального виведення формул логіки першого порядку (і як часткового випадку логіки висловлень) запропонована німецьким логіком Ґергардом Ґенценом. Після праці Ґенцена розроблено кілька варіантів числення секвенцій, що є еквівалентними між собою і альтернативою аксіоматичному підходу. (uk)
- Исчисление секвенций — вариант логических исчислений, использующий для доказательства утверждений не произвольные цепочки тавтологий, а последовательности условных суждений — секвенций. Наиболее известные исчисления секвенций — и для классического и интуиционистского исчислений предикатов — построены Генценом в 1934 году, позднее сформулированы секвенциальные варианты для широкого класса прикладных исчислений (арифметики, анализа), теорий типов, неклассических логик. В секвенциальном подходе вместо широких наборов аксиом используются развитые системы правил вывода, а доказательство ведётся в форме дерева вывода; по этому признаку (наряду с системами натурального вывода) исчисления секвенций относятся к , в противоположность аксиоматическим , в которых при развитом наборе аксиом количество правил вывода сведено к минимуму. Основное свойство секвенциальной формы — симметричное устройство, обеспечивающее удобство доказательства устранимости сечений, и, как следствие, исчисления секвенций являются основными исследуемыми системами в теории доказательств. (ru)
- 在证明论和数理逻辑中，相继式演算（又译矢列演算、矢列式演算、序贯演算）是一阶逻辑（和作为它的特殊情况的命题逻辑）、模态逻辑等逻辑的一类。第一个相继式演算和由格哈德·根岑（Gerhard Gentzen）在1934年/1935年引入，作为研究自然演绎的工具；它的名字得来自德语的“Logischer Kalkül”，意思是“逻辑演算”。相继式演算系统有时被称为Gentzen系统，但使用时应避免与同为Gentzen发明的证明演算自然演绎混淆。自然演绎、公理系统和相继式演算是常见的证明演算。 相继式演算是逻辑研究的重要工具。许多逻辑学者会为其所研究的逻辑构造出一个或多个相继式演算，并研究其性质（如切消定理）。 (zh)
|
| 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)
|
