16 found
Order:
  1.  19
    Introduction to Computability Logic.Giorgi Japaridze - 2003 - Annals of Pure and Applied Logic 123 (1-3):1-99.
    This work is an attempt to lay foundations for a theory of interactive computation and bring logic and theory of computing closer together. It semantically introduces a logic of computability and sets a program for studying various aspects of that logic. The intuitive notion of computational problems is formalized as a certain new, procedural-rule-free sort of games between the machine and the environment, and computability is understood as existence of an interactive Turing machine that wins the game against any possible (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   21 citations  
  2.  13
    In the Beginning Was Game Semantics?Giorgi Japaridze - 2009 - In Ondrej Majer, Ahti-Veikko Pietarinen & Tero Tulenheimo (eds.), Games: Unifying Logic, Language, and Philosophy. Springer Verlag. pp. 249--350.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   12 citations  
  3.  21
    The Logic of Interactive Turing Reduction.Giorgi Japaridze - 2007 - Journal of Symbolic Logic 72 (1):243 - 276.
    The paper gives a soundness and completeness proof for the implicative fragment of intuitionistic calculus with respect to the semantics of computability logic, which understands intuitionistic implication as interactive algorithmic reduction. This concept — more precisely, the associated concept of reducibility — is a generalization of Turing reducibility from the traditional, input/output sorts of problems to computational tasks of arbitrary degrees of interactivity.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  4.  21
    Many Concepts and Two Logics of Algorithmic Reduction.Giorgi Japaridze - 2009 - Studia Logica 91 (1):1-24.
    Within the program of finding axiomatizations for various parts of computability logic, it was proven earlier that the logic of interactive Turing reduction is exactly the implicative fragment of Heyting’s intuitionistic calculus. That sort of reduction permits unlimited reusage of the computational resource represented by the antecedent. An at least equally basic and natural sort of algorithmic reduction, however, is the one that does not allow such reusage. The present article shows that turning the logic of the first sort of (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  5.  11
    Towards Applied Theories Based on Computability Logic.Giorgi Japaridze - 2010 - Journal of Symbolic Logic 75 (2):565-601.
    Computability logic (CL) is a recently launched program for redeveloping logic as a formal theory of computability, as opposed to the formal theory of truth that logic has more traditionally been. Formulas in it represent computational problems, "truth" means existence of an algorithmic solution, and proofs encode such solutions. Within the line of research devoted to finding axiomatizations for ever more expressive fragments of CL, the present paper introduces a new deductive system CL12 and proves its soundness and completeness with (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  6.  14
    The Intuitionistic Fragment of Computability Logic at the Propositional Level.Giorgi Japaridze - 2007 - Annals of Pure and Applied Logic 147 (3):187-227.
    This paper presents a soundness and completeness proof for propositional intuitionistic calculus with respect to the semantics of computability logic. The latter interprets formulas as interactive computational problems, formalized as games between a machine and its environment. Intuitionistic implication is understood as algorithmic reduction in the weakest possible — and hence most natural — sense, disjunction and conjunction as deterministic-choice combinations of problems , and “absurd” as a computational problem of universal strength.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  7.  16
    A Constructive Game Semantics for the Language of Linear Logic.Giorgi Japaridze - 1997 - Annals of Pure and Applied Logic 85 (2):87-156.
    I present a semantics for the language of first-order additive-multiplicative linear logic, i.e. the language of classical first-order logic with two sorts of disjunction and conjunction. The semantics allows us to capture intuitions often associated with linear logic or constructivism such as sentences = games, SENTENCES = resources or sentences = problems, where “truth” means existence of an effective winning strategy.The paper introduces a decidable first-order logic ET in the above language and gives a proof of its soundness and completeness (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  8.  17
    The Taming of Recurrences in Computability Logic Through Cirquent Calculus, Part I.Giorgi Japaridze - 2013 - Archive for Mathematical Logic 52 (1-2):173-212.
    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 ${\neg}$ , parallel conjunction ${\wedge}$ , parallel disjunction ${\vee}$ , branching recurrence ⫰, and branching corecurrence ⫯. The article is published in two parts, with (the present) Part I containing preliminaries and a soundness proof, and (the forthcoming) Part II containing a completeness proof.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  9.  20
    Separating the Basic Logics of the Basic Recurrences.Giorgi Japaridze - 2012 - Annals of Pure and Applied Logic 163 (3):377-389.
  10.  46
    The Taming of Recurrences in Computability Logic Through Cirquent Calculus, Part II.Giorgi Japaridze - 2013 - Archive for Mathematical Logic 52 (1-2):213-259.
    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 ${{\neg}}$ , parallel conjunction ${{\wedge}}$ , parallel disjunction ${{\vee}}$ , branching recurrence ⫰, and branching corecurrence ⫯. 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.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  11.  22
    A Simple Proof of Arithmetical Completeness for $\pi_1$ -Conservativity Logic.Giorgi Japaridze - 1994 - Notre Dame Journal of Formal Logic 35 (3):346-354.
    Hájek and Montagna proved that the modal propositional logic ILM is the logic of -conservativity over sound theories containing I (PA with induction restricted to formulas). I give a simpler proof of the same fact.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  12.  6
    The Logic of Tasks.Giorgi Japaridze - 2002 - Annals of Pure and Applied Logic 117 (1-3):261-293.
    The paper introduces a semantics for the language of classical first order logic supplemented with the additional operators and . This semantics understands formulas as tasks. An agent , working as a slave for its master , can carry out the task αβ if it can carry out any one of the two tasks α, β, depending on which of them was requested by the master; similarly, it can carry out xα if it can carry out α for any particular (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  13.  14
    Ptarithmetic.Giorgi Japaridze - 2013 - The Baltic International Yearbook of Cognition, Logic and Communication 8 (1).
    The present article introduces ptarithmetic — a formal number theory similar to the well known Peano arithmetic, but based on the recently born computability logic instead of classical logic. The formulas of ptarithmetic represent interactive computational problems rather than just true/false statements, and their “truth” is understood as existence of a polynomial time solution. The system of ptarithmetic elaborated in this article is shown to be sound and complete. Sound in the sense that every theorem T of the system represents (...)
    No categories
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  14.  21
    The Propositional Logic of Elementary Tasks.Giorgi Japaridze - 2000 - Notre Dame Journal of Formal Logic 41 (2):171-183.
    The paper introduces a semantics for the language of propositional additive-multiplicative linear logic. It understands formulas as tasks that are to be accomplished by an agent (machine, robot) working as a slave for its master (user, environment). This semantics can claim to be a formalization of the resource philosophy associated with linear logic when resources are understood as agents accomplishing tasks. I axiomatically define a decidable logic TSKp and prove its soundness and completeness with respect to the task semantics in (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  15.  6
    Introduction to Clarithmetic III.Giorgi Japaridze - 2014 - Annals of Pure and Applied Logic 165 (1):241-252.
    The present paper constructs three new systems of clarithmetic : CLA8, CLA9 and CLA10. System CLA8 is shown to be sound and extensionally complete with respect to PA-provably recursive time computability. This is in the sense that an arithmetical problem A has a τ-time solution for some PA-provably recursive function τ iff A is represented by some theorem of CLA8. System CLA9 is shown to be sound and intensionally complete with respect to constructively PA-provable computability. This is in the sense (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  16.  2
    Elementary-Base Cirquent Calculus II: Choice Quantifiers.Giorgi Japaridze - forthcoming - Logic Journal of the IGPL.
    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 $\textbf{CL16}$ of a propositional fragment of computability logic. The atoms of the language of $\textbf{CL16}$ 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 $\textbf{CL17}$ of $\textbf{CL16}$, also enjoying soundness and completeness. The language of (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark