In proof theory and mathematical logic, the sequent calculus is a widely known proof calculus for first-order logic (and propositional logic as a special case of it). The term "sequent calculus" applies both to a family of formal systems sharing a certain style of formal inference, and to its individual members, of which the first, and best known, is known under the name LK, distinguishing it from other systems in the family, such as LJ.

PropertyValue
dbpprop:abstract
  • In proof theory and mathematical logic, the sequent calculus is a widely known proof calculus for first-order logic (and propositional logic as a special case of it). The term "sequent calculus" applies both to a family of formal systems sharing a certain style of formal inference, and to its individual members, of which the first, and best known, is known under the name LK, distinguishing it from other systems in the family, such as LJ. Another term for such systems in general is Gentzen systems. The sequent calculus LK was introduced by Gerhard Gentzen as a tool for studying natural deduction in 1934. It has turned out to be a very useful calculus for constructing logical derivations. The name itself is derived from the German term Logischer Kalkül, meaning "logical calculus". Sequent calculi and the general concepts relating to them are used widely in the whole field of proof theory and mathematical logic.
  • Der Sequenzenkalkül (manchmal auch Gentzenkalkül) ist ein von Gerhard Gentzen entwickelter, primär für metalogische Zwecke konzipierter logischer Kalkül.
  • 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
  • シークエント計算（英: Sequent calculus）は、一階述語論理や特殊な命題論理で広く用いられる演繹手法である。類似の手法もシークエント計算と呼ぶことがあるので、LK と呼んで区別することがある。また類似の手法も含め、総称してゲンツェン・システムとも呼ばれる。 シークエント計算とその概念全般は証明論や数理論理学において重要な意味を持つ。以下では LK について解説する。
  • 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 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 następniku (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
  • 在证明论和数理逻辑中，相继式演算是众所周知的一阶逻辑的演绎系统。这个系统也叫做 LK 系统，用以区别于后来建立的有时也叫做相继式演算的类似风格的各种其他系统。另一个给这种系统的术语是 Gentzen 系统。 相继式演算 LK 由 Gerhard Gentzen 介入为研究自然演绎的工具。它已经变成构造逻辑推导的非常有用的演算。它的名字得来自德语的 Logischer Kalkül，意思是"逻辑演算"。相继式演算是关于这个主题的很多研究所选择的方法。
dbpprop:hasPhotoCollection
dbpprop:reference
rdfs:comment
  • In proof theory and mathematical logic, the sequent calculus is a widely known proof calculus for first-order logic (and propositional logic as a special case of it). The term "sequent calculus" applies both to a family of formal systems sharing a certain style of formal inference, and to its individual members, of which the first, and best known, is known under the name LK, distinguishing it from other systems in the family, such as LJ.
  • Der Sequenzenkalkül (manchmal auch Gentzenkalkül) ist ein von Gerhard Gentzen entwickelter, primär für metalogische Zwecke konzipierter logischer Kalkül.
  • 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
  • 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.
rdfs:label
  • Sequent calculus
  • Sequenzenkalkül
  • Calcul des séquents
  • シークエント計算
  • Sekwenty Gentzena
  • 相继式演算
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of