This HTML5 document contains 149 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

Prefix	IRI
dbpedia-de	http://de.dbpedia.org/resource/
dcterms	http://purl.org/dc/terms/
dbo	http://dbpedia.org/ontology/
n36	http://dbpedia.org/resource/File:
foaf	http://xmlns.com/foaf/0.1/
dbpedia-ko	http://ko.dbpedia.org/resource/
dbpedia-hu	http://hu.dbpedia.org/resource/
n32	http://lt.dbpedia.org/resource/
dbpedia-es	http://es.dbpedia.org/resource/
dbpedia-eo	http://eo.dbpedia.org/resource/
n14	https://global.dbpedia.org/id/
dbpedia-ru	http://ru.dbpedia.org/resource/
dbt	http://dbpedia.org/resource/Template:
dbpedia-uk	http://uk.dbpedia.org/resource/
rdfs	http://www.w3.org/2000/01/rdf-schema#
freebase	http://rdf.freebase.com/ns/
dbpedia-pt	http://pt.dbpedia.org/resource/
dbpedia-pl	http://pl.dbpedia.org/resource/
n18	http://commons.wikimedia.org/wiki/Special:FilePath/
rdf	http://www.w3.org/1999/02/22-rdf-syntax-ns#
n31	http://scienceblogs.com/goodmath/2006/07/17/a-brief-diversion-sequent-calc/
owl	http://www.w3.org/2002/07/owl#
wikipedia-en	http://en.wikipedia.org/wiki/
dbpedia-zh	http://zh.dbpedia.org/resource/
dbpedia-fr	http://fr.dbpedia.org/resource/
n4	https://archive.org/details/
dbc	http://dbpedia.org/resource/Category:
dbp	http://dbpedia.org/property/
prov	http://www.w3.org/ns/prov#
xsdh	http://www.w3.org/2001/XMLSchema#
n12	http://gdz.sub.uni-goettingen.de/dms/resolveppn/
n15	http://math.ucsd.edu/~sbuss/ResearchWeb/handbookI/
wikidata	http://www.wikidata.org/entity/
gold	http://purl.org/linguistics/gold/
dbr	http://dbpedia.org/resource/
dbpedia-ja	http://ja.dbpedia.org/resource/
n13	http://gdz.sub.uni-goettingen.de/dms/resolveppn/%3FPPN=GDZPPN002375605%7Cdoi=10.1007/
n19	http://logitext.mit.edu/logitext.fcgi/

Statements

Subject Item

dbr:Sequent_calculus

rdfs:label

Sequent calculus Числення секвенцій Cálculo de secuentes Calcul des séquents 相继式演算 시퀀트 계산 Sequenzenkalkül Sekvaĵa kalkulo Sekwenty Gentzena Cálculo de sequentes シークエント計算 Исчисление секвенций

rdfs:comment

在证明论和数理逻辑中，相继式演算（又译矢列演算、矢列式演算、序贯演算）是一阶逻辑（和作为它的特殊情况的命题逻辑）、模态逻辑等逻辑的一类。第一个相继式演算和由格哈德·根岑（Gerhard Gentzen）在1934年/1935年引入，作为研究自然演绎的工具；它的名字得来自德语的“Logischer Kalkül”，意思是“逻辑演算”。相继式演算系统有时被称为Gentzen系统，但使用时应避免与同为Gentzen发明的证明演算自然演绎混淆。自然演绎、公理系统和相继式演算是常见的证明演算。 相继式演算是逻辑研究的重要工具。许多逻辑学者会为其所研究的逻辑构造出一个或多个相继式演算，并研究其性质（如切消定理）。 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. 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 シークエント計算（シークエントけいさん、英: Sequent calculus）は、一階述語論理や特殊な命題論理で広く用いられる演繹手法である。類似の手法もシークエント計算と呼ぶことがあるので、LK と呼んで区別することがある。また類似の手法も含め、総称してゲンツェン・システムとも呼ばれる。 シークエント計算とその概念全般は証明論や数理論理学において重要な意味を持つ。以下では LK について解説する。 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. 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. Чи́слення секве́нцій — система формального виведення формул логіки першого порядку (і як часткового випадку логіки висловлень) запропонована німецьким логіком Ґергардом Ґенценом. Після праці Ґенцена розроблено кілька варіантів числення секвенцій, що є еквівалентними між собою і альтернативою аксіоматичному підходу. 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. 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 시퀀트 계산(sequent calculus)은 1차 논리나 특수한 명제 논리에서 쓰이는 연역 계산법의 일종으로, 논리식으로 이루어진 특수한 열인 시퀀트를 이용한다. 유사한 수법까지 총칭하여 겐첸 체계(Gentzen system)라고도 불리며, 다른 것들과 구분하기 위해 LK라 특별히 일컫기도 한다. 자연 연역과 유사하게 이미 제시된 식들로부터 추론 규칙에 근거한 추론을 행하여 새로운 식을 이끌어내는 방식이며, 이는 공리에 근거하여 정리들을 나열하는 방식의 증명법을 가진 (Hilbert System)와는 대비된다. 시퀀트(sequent)란 논리식의 나열인데, 전건의 명제들의 논리곱을 전제로 삼고 후건의 명제들의 논리합을 귀결로 삼는 것이 특징이다. 곧, "A이고 B이고 C이고 D이고... 이면, (가)이거나 (나)이거나 (다)이거나 (라)이거나...이다."와 같은 식이다. 시퀀트 계산에서 증명은 일련의 시퀀트들의 나열로 기술되는데, 각 시퀀트는 증명과정에서 이미 출현한 시퀀트에 특정 추론규칙을 적용하는 것으로써 도출된다. Исчисление секвенций — вариант логических исчислений, использующий для доказательства утверждений не произвольные цепочки тавтологий, а последовательности условных суждений — секвенций. Наиболее известные исчисления секвенций — и для классического и интуиционистского исчислений предикатов — построены Генценом в 1934 году, позднее сформулированы секвенциальные варианты для широкого класса прикладных исчислений (арифметики, анализа), теорий типов, неклассических логик. 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:

foaf:depiction

n18:Sequent_calculus_proof_tree_example.png

dcterms:subject

dbc:Automated_theorem_proving dbc:Proof_theory dbc:Logical_calculi

dbo:wikiPageID

252329

dbo:wikiPageRevisionID

1102174974

dbo:wikiPageWikiLink

dbr:Inference dbr:Turnstile_(symbol) dbr:Gödel's_incompleteness_theorems dbc:Automated_theorem_proving dbr:Logical_conjunction dbr:David_Hilbert dbr:Sequent dbr:Hilbert_system dbr:Tautology_(logic) dbr:Rule_of_inference dbr:Logical_disjunction dbr:Formal_proof dbr:Formal_system dbr:Propositional_calculus dbr:De_Morgan's_laws dbr:Set_(mathematics) dbr:Higher-order_logic dbr:Mathematical_logic dbr:Quantification_(logic) dbr:Propositional_logic dbr:Cut-elimination_theorem dbr:Classical_logic dbr:Method_of_analytic_tableaux dbr:Axiom dbr:Proof_theory dbr:Semantics dbr:Free_variables_and_bound_variables dbr:Metatheory dbr:Hilbert-style_deduction_system dbr:Quantifier_(logic) dbc:Proof_theory dbr:Gerhard_Gentzen dbr:Nested_sequent_calculus dbr:Sequence dbr:Completeness_(logic) dbr:Completeness_of_atomic_initial_sequents dbr:Sequent_calculus dbr:Modal_logic dbr:Formal_logic dbr:First-order_logic dbr:Argument dbr:Gentzen's_consistency_proof dbr:Intuitionistic_logic dbr:Consistency dbr:Cut-elimination dbr:Proof_calculus dbr:Resolution_(logic) dbr:Frege's_propositional_calculus dbr:Atomic_formula dbr:Judgment_(mathematical_logic) dbr:Stephen_Cole_Kleene dbr:Well-formed_formula dbr:Disjunction_and_existence_properties dbr:Tree_(graph_theory) dbr:Multiset dbr:Automated_deduction dbr:Soundness dbr:Substructural_logic dbc:Logical_calculi dbr:Computer_science dbr:Artificial_intelligence dbr:Theorem dbr:Natural_deduction dbr:Principle_of_explosion dbr:Law_of_excluded_middle dbr:Logical_consequence dbr:Cirquent_calculus n36:Sequent_calculus_proof_tree_example.png dbr:Deduction_theorem dbr:If_and_only_if

dbo:wikiPageExternalLink

n4:proofstypes0000gira n12:%3FPPN=GDZPPN002375508 n13:bf01201363%7Cs2cid=186239837 n15: n19:tutorial n31:

owl:sameAs

freebase:m.01lfnc n14:j4og dbpedia-pl:Sekwenty_Gentzena dbpedia-de:Sequenzenkalkül wikidata:Q1771121 dbpedia-ja:シークエント計算 dbpedia-uk:Числення_секвенцій dbpedia-zh:相继式演算 dbpedia-es:Cálculo_de_secuentes dbpedia-hu:Szekvenskalkulus dbpedia-ko:시퀀트_계산 n32:Sekvencinis_skaičiavimas dbpedia-fr:Calcul_des_séquents dbpedia-pt:Cálculo_de_sequentes dbpedia-ru:Исчисление_секвенций dbpedia-eo:Sekvaĵa_kalkulo

dbp:wikiPageUsesTemplate

dbt:Short_description dbt:Citation_needed dbt:Cite_book dbt:Cite_journal dbt:Slink dbt:Reflist dbt:Main_article dbt:Springer

dbo:thumbnail

n18:Sequent_calculus_proof_tree_example.png?width=300

dbp:id

p/s084580

dbp:title

Sequent calculus

dbo:abstract

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 시퀀트 계산(sequent calculus)은 1차 논리나 특수한 명제 논리에서 쓰이는 연역 계산법의 일종으로, 논리식으로 이루어진 특수한 열인 시퀀트를 이용한다. 유사한 수법까지 총칭하여 겐첸 체계(Gentzen system)라고도 불리며, 다른 것들과 구분하기 위해 LK라 특별히 일컫기도 한다. 자연 연역과 유사하게 이미 제시된 식들로부터 추론 규칙에 근거한 추론을 행하여 새로운 식을 이끌어내는 방식이며, 이는 공리에 근거하여 정리들을 나열하는 방식의 증명법을 가진 (Hilbert System)와는 대비된다. 시퀀트(sequent)란 논리식의 나열인데, 전건의 명제들의 논리곱을 전제로 삼고 후건의 명제들의 논리합을 귀결로 삼는 것이 특징이다. 곧, "A이고 B이고 C이고 D이고... 이면, (가)이거나 (나)이거나 (다)이거나 (라)이거나...이다."와 같은 식이다. 시퀀트 계산에서 증명은 일련의 시퀀트들의 나열로 기술되는데, 각 시퀀트는 증명과정에서 이미 출현한 시퀀트에 특정 추론규칙을 적용하는 것으로써 도출된다. 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. 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. 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. 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. Чи́слення секве́нцій — система формального виведення формул логіки першого порядку (і як часткового випадку логіки висловлень) запропонована німецьким логіком Ґергардом Ґенценом. Після праці Ґенцена розроблено кілька варіантів числення секвенцій, що є еквівалентними між собою і альтернативою аксіоматичному підходу. 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. 在证明论和数理逻辑中，相继式演算（又译矢列演算、矢列式演算、序贯演算）是一阶逻辑（和作为它的特殊情况的命题逻辑）、模态逻辑等逻辑的一类。第一个相继式演算和由格哈德·根岑（Gerhard Gentzen）在1934年/1935年引入，作为研究自然演绎的工具；它的名字得来自德语的“Logischer Kalkül”，意思是“逻辑演算”。相继式演算系统有时被称为Gentzen系统，但使用时应避免与同为Gentzen发明的证明演算自然演绎混淆。自然演绎、公理系统和相继式演算是常见的证明演算。 相继式演算是逻辑研究的重要工具。许多逻辑学者会为其所研究的逻辑构造出一个或多个相继式演算，并研究其性质（如切消定理）。 シークエント計算（シークエントけいさん、英: Sequent calculus）は、一階述語論理や特殊な命題論理で広く用いられる演繹手法である。類似の手法もシークエント計算と呼ぶことがあるので、LK と呼んで区別することがある。また類似の手法も含め、総称してゲンツェン・システムとも呼ばれる。 シークエント計算とその概念全般は証明論や数理論理学において重要な意味を持つ。以下では LK について解説する。 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. Исчисление секвенций — вариант логических исчислений, использующий для доказательства утверждений не произвольные цепочки тавтологий, а последовательности условных суждений — секвенций. Наиболее известные исчисления секвенций — и для классического и интуиционистского исчислений предикатов — построены Генценом в 1934 году, позднее сформулированы секвенциальные варианты для широкого класса прикладных исчислений (арифметики, анализа), теорий типов, неклассических логик. В секвенциальном подходе вместо широких наборов аксиом используются развитые системы правил вывода, а доказательство ведётся в форме дерева вывода; по этому признаку (наряду с системами натурального вывода) исчисления секвенций относятся к , в противоположность аксиоматическим , в которых при развитом наборе аксиом количество правил вывода сведено к минимуму. Основное свойство секвенциальной формы — симметричное устройство, обеспечивающее удобство доказательства устранимости сечений, и, как следствие, исчисления секвенций являются основными исследуемыми системами в теории доказательств.

gold:hypernym

dbr:Tautology

prov:wasDerivedFrom

wikipedia-en:Sequent_calculus?oldid=1102174974&ns=0

dbo:wikiPageLength

53178

foaf:isPrimaryTopicOf

wikipedia-en:Sequent_calculus