Cut elimination for a calculus with context-dependent rules

DOI10.1007/S001530000058MaRDI QIDQ5945008zbMATH OpenOpenAlexFDO

Authors Birgit Elbl

Publication date 14 July 2002

Published in Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s001530000058

zbMATH Keywords

context-dependent rulecut eliminationlogic programmingSchütte-type systemsequent calculussubstructural logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Logic programming (68N17) Semantics in the theory of computing (68Q55)

Review text

In a sequential formulation of a logical calculus, context-dependent rules are often an obstacle to eliminate cut by the standard procedure featuring the permutability of rules. Focusing on a fragment of logic programming calculus, the author shows that the problem is cleared by reformulating it in a generalized sequential style to employ deep inference rules of the so-called Schütte type. The usual sequential formulation of the fragment, which is a kind of substructural multiplicative propositional logic, is shown not to enjoy the cut-elimination property, so that the reformulation is essential. The author discusses also the problems induced by adjoining non-logical axioms to the system, and extends the results to the case with additive connectives and quantifiers, of which an application to propositional programs is given.

Recommendations

• Cut Elimination in ε‐Calculi
• Cut elimination for a simple formulation of epsilon calculus
• scientific article; zbMATH DE number 7324390
• Cut elimination for Gentzen's sequent calculus with equality and logic of partial terms
• Cut Elimination in the Presence of Axioms
• CUT ELIMINATION IN HYPERSEQUENT CALCULUS FOR SOME LOGICS OF LINEAR TIME
• Cut elimination theorem for non-commutative hypersequent calculus
• The calculus of dependent lambda eliminations
• Typed Lambda Calculi and Applications
• Cut-elimination for quantified conditional logic

Cited in

(1)

• Cut rules and explicit substitutions

This page was built for publication: Cut elimination for a calculus with context-dependent rules

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5945008)