sequent calculus
E846921
Sequent calculus is a formal logical system introduced by Gerhard Gentzen that represents deductions as sequences (sequents) to analyze and structure proofs, especially in proof theory and logic.
All labels observed (2)
| Label | Occurrences |
|---|---|
| sequent calculus canonical | 1 |
| sequent calculus LK | 1 |
How this entity was disambiguated
This entity first appeared as the object of triple T10197989 — resolving that mention is where its identity was fixed. The disambiguator weighed these candidate entities and picked the highlighted one (or “None”, minting a new entity). This is how homonymy is resolved: the same surface form can point to different entities.
NED1
Entity disambiguation (via context triple)
gpt-5-mini-2025-08-07
Target entity: sequent calculus Context triple: [Gerhard Gentzen, knownFor, sequent calculus]
-
A.
Jones calculus
Jones calculus is a mathematical formalism used in optics to represent and analyze the polarization state of light and its transformation by optical elements using complex vectors and matrices.
-
B.
Mueller calculus
Mueller calculus is a mathematical framework in polarization optics that uses matrix operations to describe how optical elements transform the Stokes parameters of light.
-
C.
Curry–Howard correspondence
The Curry–Howard correspondence is a foundational principle in logic and computer science that establishes a deep analogy between proofs and programs, and between logical propositions and types in programming languages.
-
D.
Brouwer–Heyting–Kolmogorov interpretation
The Brouwer–Heyting–Kolmogorov interpretation is a foundational explanation of intuitionistic logic that interprets logical connectives and proofs in terms of explicit constructions and algorithms rather than classical truth values.
-
E.
Scholastic logic
Scholastic logic is the medieval and early modern tradition of logical theory and teaching, rooted in Aristotelian philosophy and developed in European universities by scholastic theologians and philosophers.
- F. None of above. chosen
- G. Unsure - the case is ambiguous/there is not enough information to decide.
NED2
Entity disambiguation (via description)
gpt-5-mini-2025-08-07
Target entity: sequent calculus Target entity description: Sequent calculus is a formal logical system introduced by Gerhard Gentzen that represents deductions as sequences (sequents) to analyze and structure proofs, especially in proof theory and logic.
-
A.
Jones calculus
Jones calculus is a mathematical formalism used in optics to represent and analyze the polarization state of light and its transformation by optical elements using complex vectors and matrices.
-
B.
Mueller calculus
Mueller calculus is a mathematical framework in polarization optics that uses matrix operations to describe how optical elements transform the Stokes parameters of light.
-
C.
Curry–Howard correspondence
The Curry–Howard correspondence is a foundational principle in logic and computer science that establishes a deep analogy between proofs and programs, and between logical propositions and types in programming languages.
-
D.
Brouwer–Heyting–Kolmogorov interpretation
The Brouwer–Heyting–Kolmogorov interpretation is a foundational explanation of intuitionistic logic that interprets logical connectives and proofs in terms of explicit constructions and algorithms rather than classical truth values.
-
E.
Scholastic logic
Scholastic logic is the medieval and early modern tradition of logical theory and teaching, rooted in Aristotelian philosophy and developed in European universities by scholastic theologians and philosophers.
- F. None of above. chosen
Statements (57)
| Predicate | Object |
|---|---|
| instanceOf |
deductive system
ⓘ
formal system ⓘ logical calculus ⓘ proof calculus ⓘ |
| appliesTo |
classical logic
ⓘ
intuitionistic logic ⓘ modal logic ⓘ substructural logics ⓘ |
| basedOn | sequents ⓘ |
| centralResult |
cut elimination theorem
ⓘ
linked to:
cut-elimination theorem
|
| enables |
normalization of proofs
ⓘ
subformula property ⓘ |
| field |
mathematical logic
ⓘ
philosophical logic ⓘ proof theory ⓘ |
| hasComponent |
antecedent
ⓘ
succedent ⓘ |
| hasFeature |
explicit structural rules
ⓘ
fine-grained control of inference steps ⓘ symmetry between left and right rules ⓘ |
| hasLogicalRule |
elimination rule
ⓘ
introduction rule ⓘ |
| hasProperty | cut elimination theorem ⓘ |
| hasRuleType |
initial sequent
ⓘ
logical rule ⓘ structural rule ⓘ |
| hasStructuralRule |
contraction
ⓘ
cut ⓘ exchange ⓘ weakening ⓘ |
| hasVariant |
LJ
ⓘ
LK ⓘ classical sequent calculus ⓘ intuitionistic sequent calculus ⓘ multiple-conclusion sequent calculus ⓘ single-conclusion sequent calculus ⓘ |
| influenced |
linear logic
ⓘ
separation logic ⓘ structural proof theory ⓘ type theory ⓘ |
| introducedBy | Gerhard Gentzen ⓘ |
| purpose |
analyze structure of proofs
ⓘ
establish consistency proofs ⓘ formalize logical deduction ⓘ study proof transformations ⓘ |
| relatedTo |
Hilbert-style systems
ⓘ
natural deduction ⓘ |
| represents | deductions as sequents ⓘ |
| typicalSequentForm | Γ ⊢ Δ ⓘ |
| usedFor |
automated theorem proving
ⓘ
completeness proofs ⓘ consistency proofs ⓘ interpolation theorems ⓘ proof search ⓘ |
| usesNotation | Γ ⊢ Δ ⓘ |
| yearIntroduced |
1934
ⓘ
1935 ⓘ |
How these facts were elicited
The pipeline generated the facts above by prompting gpt-5.1 with this entity's name + description and the instruction below.
Instruction
You are a knowledge base construction expert. Given a subject entity and a description of it, return factual statements that you know for the subject as a JSON list of dictionaries(triples), where keys must be "subject", "predicate" and "object". The number of facts may be very high, between 25 to 50 or more, for very popular subjects. For less popular subjects, the number of facts can be very low, like 5 or 10. # Requirements - If you don't know the subject at all, return an empty list. - If the subject is not a named entity, return an empty list. - Include at least one triple where predicate is "instanceOf". - Do not get too wordy. - Separate several objects into multiple triples with one object.
Input
Subject: sequent calculus Description of subject: Sequent calculus is a formal logical system introduced by Gerhard Gentzen that represents deductions as sequences (sequents) to analyze and structure proofs, especially in proof theory and logic.
Referenced by (2)
Full triples — surface form annotated when it differs from this entity's canonical label.