The computational complexity of propositional cirquent calculus

DOI10.2168/LMCS-11(1:12)2015MaRDI QIDQ5246717zbMATH OpenFDO

Authors Matthew S. Bauer

Publication date 22 April 2015

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1401.1849

zbMATH Keywords

cirquent calculuscomputability logicproof theoryresource semanticssubstructural logics

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Complexity of computation (including implicit computational complexity) (03D15) Structure of proofs (03F07)

Abstract: Introduced in 2006 by Japaridze, cirquent calculus is a refinement of sequent calculus. The advent of cirquent calculus arose from the need for a deductive system with a more explicit ability to reason about resources. Unlike the more traditional proof-theoretic approaches that manipulate tree-like objects (formulas, sequents, etc.), cirquent calculus is based on circuit-style structures called cirquents, in which different "peer" (sibling, cousin, etc.) substructures may share components. It is this resource sharing mechanism to which cirquent calculus owes its novelty (and its virtues). From its inception, cirquent calculus has been paired with an abstract resource semantics. This semantics allows for reasoning about the interaction between a resource provider and a resource user, where resources are understood in the their most general and intuitive sense. Interpreting resources in a more restricted computational sense has made cirquent calculus instrumental in axiomatizing various fundamental fragments of Computability Logic, a formal theory of (interactive) computability. The so-called "classical" rules of cirquent calculus, in the absence of the particularly troublesome contraction rule, produce a sound and complete system CL5 for Computability Logic. In this paper, we investigate the computational complexity of CL5, showing it is $Sigm{a}_2^p$-complete. We also show that CL5 without the duplication rule has polynomial size proofs and is NP-complete.

Recommendations

• Introduction to Cirquent Calculus and Abstract Resource Semantics
• Cirquent Calculus Deepened
• A cirquent calculus system with clustering and ranking
• The taming of recurrences in computability logic through cirquent calculus. I
• The taming of recurrences in computability logic through cirquent calculus. II

Cited in

(22)

• The expected complexity of analytic tableaux analyses in propositional calculus. II
• On compact representations of propositional circumscription
• Build your own clarithmetic. I: Setup and completeness
• A cirquent calculus system with clustering and ranking
• Simulating non-prenex cuts in quantified propositional calculus
• Deduction theorem for symmetric cirquent calculus
• scientific article; zbMATH DE number 5599076 (Why is no real title available?)
• Introduction to Cirquent Calculus and Abstract Resource Semantics
• Cirquent Calculus Deepened
• The Complexity of Circumscriptive Inference in Post’s Lattice
• scientific article; zbMATH DE number 1962835 (Why is no real title available?)
• scientific article; zbMATH DE number 2044514 (Why is no real title available?)
• scientific article; zbMATH DE number 2044758 (Why is no real title available?)
• scientific article; zbMATH DE number 6963530 (Why is no real title available?)
• Elementary-base cirquent calculus. II: Choice quantifiers
• Cirquent Calculus in a Nutshell
• Circuit complexity and the expressive power of generalized first-order formulas
• scientific article; zbMATH DE number 7155168 (Why is no real title available?)
• scientific article; zbMATH DE number 5263419 (Why is no real title available?)
• Logic for Programming, Artificial Intelligence, and Reasoning
• A propositional cirquent calculus for computability logic.
• Complexity of subclasses of the intuitionistic propositional calculus

This page was built for publication: The computational complexity of propositional cirquent calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5246717)