Cirquent calculus is a proof system with inherent ability to account for sharing subcomponents in logical expressions. Within its framework, this article constructs an axiomatization CL18\documentclass[12pt]{minimal} ...
详细信息
Cirquent calculus is a proof system with inherent ability to account for sharing subcomponents in logical expressions. Within its framework, this article constructs an axiomatization CL18\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\text{ CL18 }$$\end{document} of the basic propositional fragment of computability logic-the game-semantically conceived logic of computational resources and tasks. The nonlogical atoms of this fragment represent arbitrary so called static games, and the connectives of its logical vocabulary are negation and the parallel and choice versions of conjunction and disjunction. The main technical result of the article is a proof of the soundness and completeness of CL18\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\text{ CL18 }$$\end{document} with respect to the semantics of computability logic.
computability logic (CoL) 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 C...
详细信息
computability logic (CoL) 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 CoL 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 ("constructive") sorts of quantifiers and connectives. This system has already found fruitful applications as a logical basis for constructive and complexity-bound versions of Peano arithmetic, such as arithmetics for polynomial tune 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 (soundness/completeness) of CL12 and the associated logical Catisequetice mechanism with respect to (simultatieously) A amplitude, S space and T time computability under certain minimal conditions on the triples (A, 5, T) of function classes. This result very substantially broadens the potential application areas of CL12, even when time and/or space complexity is the only concern. It would be sufficient to point out that, for instance, now CL12 can be reliably used as a logical basis of systems for logarithmic space or exponential time computabilities - something that the earlier-known crude adequacy results for CL12 were too weak to allow us to do. This paper is self-contained, and targets readers with no prior familiarity with the subject.
This paper proposes a new approach to defining and expressing algorithms: the notion of task logical algorithms. This notion allows the user to define an algorithm for a task T as a set of agents who can collectively ...
详细信息
This paper proposes a new approach to defining and expressing algorithms: the notion of task logical algorithms. This notion allows the user to define an algorithm for a task T as a set of agents who can collectively perform T. This notion considerably simplifies the algorithm development process and can be seen as an integration of the sequential pseudocode and logical algorithms. This observation requires some changes to algorithm development process. We propose a two-step approach: the first step is to define an algorithm for a task T via a set of agents that can collectively perform T. The second step is to translate these agents into (higher-order) computability logic.
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 Compu...
详细信息
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 for all, there exists-free fragment of CL4 was shown to be decidable in polynomial space. The present work extends this result and proves that this fragment is, in fact, PSPACE-complete.
We introduce a new, substantially simplified version of the toggling-branching recurrence operation of com- putability logic, prove its equivalence to Japaridze＇s old, ＂canonical＂ version, and also prove that both ...
详细信息
We introduce a new, substantially simplified version of the toggling-branching recurrence operation of com- putability logic, prove its equivalence to Japaridze＇s old, ＂canonical＂ version, and also prove that both versions preserve the static property of their arguments.
Cirquent calculus is a novel proof theory permitting component-sharing between logical expressions. Using it, the predecessor article 'Elementary-base cirquent calculus I: Parallel and choice connectives' buil...
详细信息
Cirquent calculus is a novel proof theory permitting component-sharing between logical expressions. Using it, the predecessor article 'Elementary-base cirquent calculus I: Parallel and choice connectives' built the sound and complete axiomatization of a propositional fragment of computability logic. The atoms of the language of represent elementary, i.e. moveless, games and the logical vocabulary consists of negation, parallel connectives and choice connectives. The present paper constructs the first-order version of , also enjoying soundness and completeness. The language of augments that of by including choice quantifiers. Unlike classical predicate calculus, turns out to be decidable.
This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic. The logical vocabulary of the system consists of negation (sic), paralle...
详细信息
This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic. The logical vocabulary of the system consists of negation (sic), parallel conjunction boolean AND, parallel disjunction boolean OR, branching recurrence (sic), and branching corecurrence (sic). The article is published in two parts, with (the previous) Part I containing preliminaries and a soundness proof, and (the present) Part II containing a completeness proof.
This paper shows that the basic logic induced by the parallel recurrence (sic) of computability logic (i.e., the one in the signature {(sic), boolean AND, boolean OR, (sic), gamma}) is a proper superset of the basic l...
详细信息
This paper shows that the basic logic induced by the parallel recurrence (sic) of computability logic (i.e., the one in the signature {(sic), boolean AND, boolean OR, (sic), gamma}) is a proper superset of the basic logic induced by the branching recurrence (sic) (i.e., the one in the signature {(sic), boolean AND, boolean OR, (sic), (sic)}). The latter is known to be precisely captured by the cirquent calculus system CL15, conjectured by Japaridze to remain sound-but not complete-with (sic) instead of (sic). The present result is obtained by positively verifying that conjecture. A secondary result of the paper is showing that (sic) is strictly weaker than (sic) in the sense that, while (sic) F logically implies (sic)F, the reverse does not hold.
This letter introduces a new, substantially simplified version of the branching recurrence operation of computability logic, and proves its equivalence to the old, "canonical" version. (C) 2011 Elsevier Ltd....
详细信息
This letter introduces a new, substantially simplified version of the branching recurrence operation of computability logic, and proves its equivalence to the old, "canonical" version. (C) 2011 Elsevier Ltd. All rights reserved.
computability logic is a formal theory of computability. The earlier article 'Introduction to cirquent calculus and abstract resource semantics' by Japaridze proved soundness and completeness for the basic fra...
详细信息
computability logic is a formal theory of computability. The earlier article 'Introduction to cirquent calculus and abstract resource semantics' by Japaridze proved soundness and completeness for the basic fragment CL5 of computability logic. The present article extends that result to the more expressive cirquent calculus system CL6, which is a conservative extension of both CL5 and classical propositional logic.
暂无评论