@inproceedings{8eb1f59ea5404200ad748a34942a2c77,
title = "Using linear logic to reason about sequent systems",
abstract = "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.",
author = "Dale Miller and Elaine Pimentel",
year = "2002",
month = jan,
day = "1",
doi = "10.1007/3-540-45616-3\_2",
language = "English",
isbn = "3540439293",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "2--23",
editor = "Uwe Egly and Fermuller, \{Christian G.\}",
booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 2002, Proceedings",
note = "International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2002 ; Conference date: 30-07-2002 Through 01-08-2002",
}