Substructural logic and partial correctness

DOI10.1145/772062.772066MaRDI QIDQ5267434zbMATH OpenOpenAlexWikidataFDO

Authors Dexter Kozen, Jerzy Tiuryn

Publication date 13 June 2017

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/772062.772066

zbMATH Keywords

substructural logiclinear logicspecificationdynamic logicHoare logicsequent calculusKleene algebraKleene algebra with tests

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Structure of proofs (03F07)

Recommendations

• Substructural logic of proofs
• Structural Completeness in Substructural Logics
• scientific article; zbMATH DE number 4053610
• Substructural Logics in Natural Deduction
• Proof complexity of substructural logics
• scientific article; zbMATH DE number 1406811
• Substructural logics: a primer
• scientific article; zbMATH DE number 1907195
• scientific article; zbMATH DE number 5289966
• Theorem provers for substructural logics

Cited in

(14)

• Current trends in substructural logics
• scientific article; zbMATH DE number 1107619 (Why is no real title available?)
• scientific article; zbMATH DE number 1984270 (Why is no real title available?)
• Embedding Kozen-Tiuryn logic into residuated one-sorted Kleene algebra with tests
• Proper semantics for substructural logics, from a stalker theoretic point of view
• Concurrent Kleene algebra with tests and branching automata
• KAT-ML: an interactive theorem prover for Kleene algebra with tests
• Off-line parsability and the well-foundedness of subsumption
• Local variable scoping and Kleene algebra with tests
• Left-handed completeness
• Left-handed completeness
• Sequential dynamic logic
• Implicational Kleene algebra with domain and the substructural logic of partial correctness
• Advancements in resource-driven substructural defeasible logic

This page was built for publication: Substructural logic and partial correctness

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