CMU-CS-06-162Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-06-162
Kaustuv Chaudhuri December 2006 Ph.D. Thesis
Keywords: Linear logic presents a unified framework for describing and reasoning about stateful systems. Because of its view of hypotheses as resources, it supports such phenomena as concurrency, external and internal choice, and state transitions that are common in such domains as protocol verification, concurrent computation, process calculi and games. It accomplishes this unifying view by providing logical connectives whose behaviour is closely tied to the precise collection of resources. The interaction of the rules for multiplicative, additive and exponential connectives gives rise to a wide and expressive array of behaviours. This expressivity comes with a price: even simple fragments of the logic are highly complex or undecidable.
Various approaches have been taken to produce automated reasoning
systems for fragments of linear logic. This thesis addresses the
need for automated reasoning for the The goal of this thesis is to establish the focused inverse method as the premier means of automated reasoning in linear logic. To this end, the technical claims are substantiated with an implementation of a competitive first-order theorem prover for linear logic – as of this writing, the only one of its kind. 222 pages
| |

Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |