On the system CL12 of computability logic

DOI10.2168/LMCS-11(3:1)2015MaRDI QIDQ2941766zbMATH OpenFDO

Authors Giorgi Japaridze

Publication date 25 August 2015

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

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

zbMATH Keywords

computability logicconstructive logicsefficiency logicsgame semanticsimplicit computational complexityinteractive computation

Mathematics Subject Classification ID

Complexity of computation (including implicit computational complexity) (03D15) Recursive functions and relations, subrecursive hierarchies (03D20) Abstract and axiomatic computability and recursion theory (03D75) Metamathematics of constructive systems (03F50) Analysis of algorithms and problem complexity (68Q25)

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.

Recommendations

• Soundness and completeness of the cirquent calculus system CL6 for computability logic
• On computability by logic programs
• On the Logical System L₁
• scientific article; zbMATH DE number 4125400
• An application of clasp in the study of logics
• Computability logic: a formal theory of interaction
• Introduction to computability logic
• Towards applied theories based on computability logic
• scientific article; zbMATH DE number 1163938
• scientific article; zbMATH DE number 1341468

Cited in

(4)

• A logical basis for constructive systems
• Build your own clarithmetic. I: Setup and completeness
• Arithmetics base on computability logic
• A propositional cirquent calculus for computability logic.

This page was built for publication: On the system CL12 of computability logic

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