scientific article; zbMATH DE number 1215493

Publication date: 16 May 1999

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

sequent calculus proof theory cut-elimination resolution method

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Cut-elimination and normal-form theorems (03F05) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items (60)

Logic and majority voting ⋮ The NP Search Problems of Frege and Extended Frege Proofs ⋮ Inferences and metainferences in \(\mathsf{ST}\) ⋮ The proof complexity of linear algebra ⋮ Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \) ⋮ Introspection, Normality and Agglomeration ⋮ A logic and computation for Popper's conditional probabilities ⋮ The mathematical significance of proof theory ⋮ Quantified propositional calculus and a second-order theory for NC\(^{\text \textbf{1}}\) ⋮ Slow reflection ⋮ Short proofs for slow consistency ⋮ Paraconsistency, paracompleteness, Gentzen systems, and trivalent semantics ⋮ Taming Paraconsistent (and Other) Logics ⋮ Checking Proofs ⋮ First-degree entailment and its relatives ⋮ ABSTRACT FORMS OF QUANTIFICATION IN THE QUANTIFIED ARGUMENT CALCULUS ⋮ On the complexity of finding falsifying assignments for Herbrand disjunctions ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ To be or not to be constructive, that is not the question ⋮ Logical Closure Properties of Propositional Proof Systems ⋮ Alternating (in)dependence-friendly logic ⋮ A sequent calculus for a negative free logic ⋮ Algebraic proof theory for substructural logics: cut-elimination and completions ⋮ Monstrous content and the bounds of discourse ⋮ Mining the surface: witnessing the low complexity theorems of arithmetic ⋮ Proof theory and mathematical meaning of paraconsistent C-systems ⋮ A Computable Solution to Partee’s Temperature Puzzle ⋮ Strict finitism and the happy sorites ⋮ More infinity for a better finitism ⋮ On theories of bounded arithmetic for \(\mathrm{NC}^1\) ⋮ The canonical pairs of bounded depth Frege systems ⋮ On the elimination of quantifier-free cuts ⋮ Sufficient conditions for cut elimination with complexity analysis ⋮ Primitive recursive selection functions for existential assertions over abstract algebras ⋮ Priest on Negation ⋮ INCOMPLETENESS IN THE FINITE DOMAIN ⋮ Harrington's conservation theorem redone ⋮ A proof-theoretic study of the correspondence of classical logic and modal logic ⋮ Degrees of relative provability ⋮ Extracting Herbrand disjunctions by functional interpretation ⋮ On the computational content of intuitionistic propositional proofs ⋮ Herbrand's theorem and term induction ⋮ Unnamed Item ⋮ Paraconsistent informational logic ⋮ On the form of witness terms ⋮ Common knowledge does not have the Beth property ⋮ Corrected upper bounds for free-cut elimination ⋮ Unnamed Item ⋮ On the correspondence between arithmetic theories and propositional proof systems – a survey ⋮ A proof-theoretic study of the correspondence of hybrid logic and classical logic ⋮ A formal framework for stringology ⋮ Prawitz, Proofs, and Meaning ⋮ PROOF-THEORETIC ANALYSIS OF THE QUANTIFIED ARGUMENT CALCULUS ⋮ Proof Complexity of Non-classical Logics ⋮ Reverse formalism 16 ⋮ Bounded linear-time temporal logic: a proof-theoretic investigation ⋮ Compressibility of Finite Languages by Grammars ⋮ The G4i analogue of a G3i sequent calculus ⋮ Towards a semantic characterization of cut-elimination ⋮ The epsilon calculus and Herbrand complexity

This page was built for publication: