Linear logic can be used as a meta-logic for the specification of some sequent calculus proof systems. We explore in this paper properties of such linear logic specifications. We show that derivability of one proof system from another has a simple decision procedure that is implemented simply via bounded logic programming search. We also provide conditions to ensure that an encoded proof system has the cut-elimination property and show that this can be decided again by simple, bounded proof search algorithms. © Springer-Verlag Berlin Heidelberg 2002.
CITATION STYLE
Miller, D., & Pimentel, E. (2002). Using linear logic to reason about sequent systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2381 LNAI, pp. 2–23). Springer Verlag. https://doi.org/10.1007/3-540-45616-3_2
Mendeley helps you to discover research relevant for your work.