Journal of Logic and Computation Advance Access originally published online on July 21, 2008
Journal of Logic and Computation 2008 18(6):983-1028; doi:10.1093/logcom/exn019
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||
Original Articles |
Cirquent Calculus Deepened
Institute of Artificial Intelligence, Xiamen University, China; Department of Computing Sciences, Villanova University, USA.
E-mail: giorgi.japaridze{at}villanova.edu
Received 10 September 2007.
 |
Abstract |
|---|
Cirquent calculus is a new proof-theoretic and semantic framework, whose main distinguishing feature is being based on circuit-style structures (called cirquents), as opposed to the more traditional approaches that deal with tree-like objects such as formulas, sequents or hypersequents. Among its advantages are greater efficiency, flexibility and expressiveness. This article presents a detailed elaboration of a deep-inference cirquent logic, which is naturally and inherently resource conscious. It shows that classical logic, both syntactically and semantically, can be seen to be just a special, conservative fragment of this more general and, in a sense, more basic logic—the logic of resources in the form of cirquent calculus. The reader will find various arguments in favour of switching to the new framework, such as arguments showing the insufficiency of the expressive power of linear logic or other formula-based approaches to developing resource logics, exponential improvements over the traditional approaches in both representational and proof complexities offered by cirquent calculus (including the existence of polynomial size cut-, substitution- and extension-free cirquent calculus proofs for the notoriously hard pigeonhole principle), and more. Among the main purposes of this article is to provide an introductory-style starting point for what, as the author wishes to hope, might have chances to become a new line of research in proof theory—a proof theory based on circuits instead of formulas.
Keywords: Proof theory; cirquent calculus; resource semantics; deep inference; computability logic; pigeonhole principle