|
Abstract : |
A great deal of insight about a logic can be derived from the study of the difficulty of deciding if a given formula is provable in that logic. Most first order logics are undecidable and are linear time decidable with no quantifiers and no propositional symbols. However, logics differ greatly in the complexity of deciding propositional formulas. For example, first-order classical logic is undecidable, propositional classical logic is np-complete, and constant-only classical logic is decidable in linear time. Intuitionistic logic shares the same complexity characterization as classical logic except at the propositional level, where intuitionistic logic is pspace-complete. In this survey we review the available results characterizing various fragments of linear logic. Surprises include the fact that both propositional and constant-only linear logic are undecidable. The results of these studies can be used to guide further proof-theoretic exploration, the study of semantics, and the construction of theorem provers and logic programming languages. 1, |
