Non-commutative logic. III: Focusing proofs. (Q1427855): Difference between revisions

From MaRDI portal
Import240304020342 (talk | contribs)
Set profile property.
ReferenceBot (talk | contribs)
Changed an Item
 
Property / cites work
 
Property / cites work: Non-commutative logic. I: The multiplicative fragment / rank
 
Normal rank
Property / cites work
 
Property / cites work: Logic Programming with Focusing Proofs in Linear Logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4938434 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3357521 / rank
 
Normal rank
Property / cites work
 
Property / cites work: On proof normalization in linear logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Linear logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: The Mathematics of Sentence Structure / rank
 
Normal rank
Property / cites work
 
Property / cites work: Uniform proofs as a foundation for logic programming / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4918387 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Non-commutative logic II: sequent calculus and phase semantics / rank
 
Normal rank
Property / cites work
 
Property / cites work: Quantales and (noncommutative) linear logic / rank
 
Normal rank

Latest revision as of 15:35, 6 June 2024

scientific article
Language Label Description Also known as
English
Non-commutative logic. III: Focusing proofs.
scientific article

    Statements

    Non-commutative logic. III: Focusing proofs. (English)
    0 references
    0 references
    0 references
    14 March 2004
    0 references
    The paper studies the focalization property in the framework of \textit{V. M. Abrusci} and \textit{P. Ruet}'s non-commutative logic [Ann. Pure Appl. Logic 101, 29--64 (2000; Zbl 0962.03054)]. Abrusci and Ruet introduced sequent calculus and proof-nets for multiplicative non-commutative logic (MNL), and later \textit{P. Ruet} [Math. Struct. Comput. Sci. 10, 277--312 (2000; Zbl 0999.03056)] extended the sequent calculus to full propositional non-commutative logic (NL). In this paper, the authors define a focalized sequent calculus for NL. The main problem to overcome is related to the extra structure (the order variety) of NL: does it fit in with the (now standard) splitting of connectives into reversible/irreversible? It is shown that one can ``push'' the entropy rule of NL towards the rules of conjunction, and thus give a positive answer. A nice thing is how completeness of the focalized system is proven for MNL: it is shown that every MNL proof-net can be sequentialized into a focalized sequent calculus proof. In the general NL case, completeness is achieved thanks to a careful study of the permutability of the rules.
    0 references
    0 references
    0 references
    0 references
    0 references
    focalization
    0 references
    order varieties
    0 references
    linear logic
    0 references
    sequent calculus
    0 references