On the system CL12 of computability logic

Abstract

Computability logic (see http://www.csc.villanova.edu/~japaridz/CL/) is a long-term project for redeveloping logic on the basis of a constructive game semantics, with games seen as abstract models of interactive computational problems. Among the fragments of this logic successfully axiomatized so far is CL12 --- a conservative extension of classical first-order logic, whose language augments that of classical logic with the so called choice sorts of quantifiers and connectives. This system has already found fruitful applications as a logical basis for constructive and complexity-oriented versions of Peano arithmetic, such as arithmetics for polynomial time computability, polynomial space computability, and beyond. The present paper introduces a third, indispensable complexity measure for interactive computations termed amplitude complexity, and establishes the adequacy of CL12 with respect to A-amplitude, S-space and T-time computability under certain minimal conditions on the triples (A,S,T) of function classes. This result very substantially broadens the potential application areas of CL12. The paper is self-contained, and targets readers with no prior familiarity with the subject.

arXiv admin note: substantial text overlap with arXiv:1003.0425 and arXiv:1003.4719

References in corpus (22)

• Sequential operators in computability logic
• Introduction to Cirquent Calculus and Abstract Resource Semantics
• Propositional computability logic I
• Cirquent calculus deepened
• Computability Logic: a formal theory of interaction
• From truth to computability I
• The intuitionistic fragment of computability logic at the propositional level
• Propositional Computability Logic II
• Intuitionistic computability logic
• Many concepts and two logics of algorithmic reduction
• From truth to computability II
• The taming of recurrences in computability logic through cirquent calculus, Part I
• Toggling operators in computability logic
• From formulas to cirquents in computability logic
• Introduction to clarithmetic II
• The parallel versus branching recurrences in computability logic
• A new face of the branching recurrence of computability logic
• A logical basis for constructive systems
• Introduction to clarithmetic I
• The taming of recurrences in computability logic through cirquent calculus, Part II
• Separating the basic logics of the basic recurrences
• The Computational Complexity of Propositional Cirquent Calculus

Cited by in corpus (9)

• Elementary-base cirquent calculus I: Parallel and choice connectives
• Build your own clarithmetic I: Setup and completeness
• Build your own clarithmetic II: Soundness
• Towards Distributed Logic Programming based on Computability Logic
• Sequential Operations in LogicWeb
• Implementing program extraction from CL1-proofs
• Agent-Based Proof Design via Lemma Flow Diagram
• Implementing Agent-Based Systems via Computability Logic CL2
• Extending and Automating Basic Probability Theory with Propositional Computability Logic