A PSPACE-complete first-order fragment of computability logic

DOI10.1145/2559949MaRDI QIDQ5410328zbMATH OpenOpenAlexWikidataFDO

Authors Matthew S. Bauer

Publication date 16 April 2014

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

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

zbMATH Keywords

computability logiccomputational complexitygame semanticsinteractive computation

Mathematics Subject Classification ID

Logic in computer science (03B70) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Abstract: In a recently launched research program for developing logic as a formal theory of (interactive) computability, several very interesting logics have been introduced and axiomatized. These fragments of the larger Computability Logic aim not only to describe "what" can be computed, but also provide a mechanism for extracting computational algorithms from proofs. Among the most expressive and fundamental of these is CL4, known to be (constructively) sound and complete with respect to the underlying computational semantics. Furthermore, the fragment of CL4 not containing blind quantifiers was shown to be decidable in polynomial space. The present work extends this result and proves that this fragment is, in fact, PSPACE-complete.

Recommendations

• A PSPACE-complete fragment of second-order linear logic
• Completeness and decidability of general first-order logic (with a detour through the guarded fragment)
• First-order satisfiability in Gödel logics: an NP-complete fragment
• Some Turing-complete extensions of first-order logic
• The intuitionistic fragment of computability logic at the propositional level
• Computations in fragments of intuitionistic propositional logic
• Completeness theorem for a first order linear-time logic
• Completeness for a first-order abstract separation logic
• Parameterized complexity of some prefix-vocabulary fragments of first-order logic
• Lindstrom theorems for fragments of first-order logic

Cites work

• A game semantics for linear logic
• First-order linear logic without modalities is NEXPTIME-hard
• From truth to computability. I.
• From truth to computability. II.
• scientific article; zbMATH DE number 5595162 (Why is no real title available?)
• scientific article; zbMATH DE number 972408 (Why is no real title available?)
• In the beginning was game semantics
• Introduction to Cirquent Calculus and Abstract Resource Semantics
• Introduction to clarithmetic. I
• Introduction to clarithmetic. II
• Introduction to clarithmetic. III
• Introduction to computability logic
• Propositional computability logic I
• Propositional computability logic II
• Soundness and completeness of the cirquent calculus system CL6 for computability logic

Cited in

(6)

• A constant-space sequential model of computation for first-order logic
• On the toggling-branching recurrence of computability logic
• Build your own clarithmetic. I: Setup and completeness
• scientific article; zbMATH DE number 3900148 (Why is no real title available?)
• A propositional cirquent calculus for computability logic.
• Thoughts on sub-Turing interactive computability

This page was built for publication: A PSPACE-complete first-order fragment of computability logic

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