Name
Abstract | ||
|---|---|---|
Intuitionistic logic and intuitionistic type systems are commonly used as frameworks for the specification of natural deduction proof systems. In this paper we show how to use classical linear logic as a logical framework to specify sequent calculus proof systems and to establish some simple consequences of the specified sequent calculus proof systems. In particular, derivability of an inference rule from a set of inference rules can be decided by bounded (linear) logic programming search on the specified rules. We also present two simple and decidable conditions that guarantee that the cut rule and non-atomic initial rules can be eliminated. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1016/j.tcs.2012.12.008 | Theor. Comput. Sci. |
Keywords | DocType | Volume |
Intuitionistic logic,simple consequence,specified sequent calculus proof,natural deduction proof system,non-atomic initial rule,logic programming search,classical linear logic,formal framework,sequent calculus proof system,inference rule,cut rule | Journal | 474, |
ISSN | Citations | PageRank |
0304-3975 | 17 | 0.80 |
References | Authors | |
31 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Dale Miller | 1 | 2485 | 232.26 |
| Elaine Pimentel | 2 | 119 | 14.78 |