Cut elimination for a calculus with context-dependent rules (Q5945008)
From MaRDI portal
scientific article; zbMATH DE number 1655894
Language | Label | Description | Also known as |
---|---|---|---|
English | Cut elimination for a calculus with context-dependent rules |
scientific article; zbMATH DE number 1655894 |
Statements
Cut elimination for a calculus with context-dependent rules (English)
0 references
14 July 2002
0 references
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.
0 references
sequent calculus
0 references
cut elimination
0 references
context-dependent rule
0 references
Schütte-type system
0 references
logic programming
0 references
substructural logic
0 references