This page contains a list of departmental technical reports, organized sequentially by year and alphabetically by author within a year. All reports are archived in ACM's CoRR (Computing Research Repository). An archived report can be reached by clicking on its title.
Technical Report Information  including submission guidelines
2012 

Title:  On the system CL12 of computability logic 
Author:  Dr. Giorgi Japaridze 
Abstract:  Abstract: Computability logic (see this http URL) is a longterm 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 firstorder 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 complexityoriented 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 Aamplitude, Sspace and Ttime 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 selfcontained, and targets readers with no prior familiarity with the subject. 
Title:  A PSPACEComplete First Order Fragment of Computability Logic 
Author:  Matthew Bauer 
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, PSPACEcomplete. 
2011 

Title:  A new face of the branching recurrence of computability logic 
Author:  Dr. Giorgi Japaridze 
Abstract:  This letter introduces a new, substantially simplified version of the branching recurrence operation of computability logic (see this http URL), and proves its equivalence to the old, "canonical" version. 
Title:  The taming of recurrences in computability logic through cirquent calculus, Part I 
Author:  Dr. Giorgi Japaridze 
Abstract:  This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic (see this http URL). The logical vocabulary of the system consists of negation, parallel conjunction, parallel disjunction, 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. 
Title:  The taming of recurrences in computability logic through cirquent calculus, Part II 
Author:  Dr. Giorgi Japaridze 
Abstract:  This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic (see this http URL). The logical vocabulary of the system consists of negation, parallel conjunction, parallel disjunction, 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. 
2010 

Title:  Separating the basic logics of the basic recurrences 
Author:  Dr. Giorgi Japaridze 
Abstract:  This paper shows that, even at the most basic level, the parallel, countable branching and uncountable branching recurrences of computability logic validate different principles. 
Title:  Introduction to clarithmetic III 
Author:  Dr. Giorgi Japaridze 
Abstract:  The present paper constructs three new systems of clarithmetic (arithmetic based on computability logic): CLA8, CLA9 and CLA10. System CLA8 is shown to be sound and extensionally complete with respect to PAprovably recursive time computability. This is in the sense that an arithmetical problem A has a ttime solution for some PAprovably recursive function t iff A is represented by some theorem of CLA8. System CLA9 is shown to be sound and intensionally complete with respect to constructively PAprovable computability. This is in the sense that a sentence X is a theorem of CLA9 iff, for some particular machine M, PA proves that M computes (the problem represented by) X. And system CLA10 is shown to be sound and intensionally complete with respect to notnecessarilyconstructively PAprovable computability. This means that a sentence X is a theorem of CLA10 iff PA proves that X is computable, even if PA does not "know" of any particular machine M that computes X. 
Title:  A logical basis for constructive systems 
Author:  Dr. Giorgi Japaridze 
Abstract:  The work is devoted to Computability Logic (CoL)  the philosophical/mathematical platform and longterm project for redeveloping classical logic after replacing truth} by computability in its underlying semantics (see this http URL ). This article elaborates some basic complexity theory for the CoL framework. Then it proves soundness and completeness for the deductive system CL12 with respect to the semantics of CoL, including the version of the latter based on polynomial time computability instead of computabilityinprinciple. CL12 is a sequent calculus system, where the meaning of a sequent intuitively can be characterized as "the succedent is algorithmically reducible to the antecedent", and where formulas are built from predicate letters, function letters, variables, constants, identity, negation, parallel and choice connectives, and blind and choice quantifiers. A case is made that CL12 is an adequate logical basis for constructive applied theories, including complexityoriented ones. 
Title:  Introduction to clarithmetic I 
Author:  Dr. Giorgi Japaridze 
Abstract:  "Clarithmetic" is a generic name for formal number theories similar to Peano arithmetic, but based on computability logic (see this http URL) instead of the more traditional classical or intuitionistic logics. Formulas of clarithmetical theories represent interactive computational problems, and their "truth" is understood as existence of an algorithmic solution. Imposing various complexity constraints on such solutions yields various versions of clarithmetic. The present paper introduces a system of clarithmetic for polynomial time computability, which is shown to be sound and complete. Sound in the sense that every theorem T of the system represents an interactive numbertheoretic computational problem with a polynomial time solution and, furthermore, such a solution can be efficiently extracted from a proof of T. And complete in the sense that every interactive numbertheoretic problem with a polynomial time solution is represented by some theorem T of the system. The paper is written in a semitutorial style and targets readers with no prior familiarity with computability logic. 
Title:  Introduction to clarithmetic II 
Author:  Dr. Giorgi Japaridze 
Abstract:  The earlier paper "Introduction to clarithmetic I" constructed an axiomatic system of arithmetic based on computability logic (see this http URL), and proved its soundness and extensional completeness with respect to polynomial time computability. The present paper elaborates three additional sound and complete systems in the same style and sense: one for polynomial space computability, one for elementary recursive computability, and one for primitive recursive computability. 
2009 

Title:  From formulas to cirquents in computability logic 
Author:  Dr. Giorgi Japaridze 
Abstract:  Computability logic (CL) (see this http URL) is a recently introduced semantical platform and ambitious program for redeveloping logic as a formal theory of computability, as opposed to the formal theory of truth which logic has more traditionally been. Its expressions represent interactive computational tasks seen as games played by a machine against the environment, and "truth" is understood as existence of an algorithmic winning strategy. With logical operators standing for operations on games, the formalism of CL is openended, and has already undergone series of extensions. This article extends the expressive power of CL in a qualitatively new way, generalizing formulas (to which the earlier languages of CL were limited) to circuitstyle structures termed cirquents. The latter, unlike formulas, are able to account for subgame/subtask sharing between different parts of the overall game/task. Among the many advantages offered by this ability is that it allows us to capture, refine and generalize the well known independencefriendly logic which, after the present leap forward, naturally becomes a conservative fragment of CL, just as classical logic had been known to be a conservative fragment of the formulabased version of CL. Technically, this paper is selfcontained, and can be read without any prior familiarity with CL. 
Title:  Toggling operators in computability logic 
Author:  Dr. Giorgi Japaridze 
Abstract:  Computability logic (CL) (see this http URL) is a research program for redeveloping logic as a formal theory of computability, as opposed to the formal theory of truth which it has more traditionally been. Formulas in CL stand for interactive computational problems, seen as games between a machine and its environment; logical operators represent operations on such entities; and "truth" is understood as existence of an effective solution. The formalism of CL is openended, and may undergo series of extensions as the studies of the subject advance. So far three  parallel, sequential and choice  sorts of conjunction and disjunction have been studied. The present paper adds one more natural kind to this collection, termed toggling. The toggling operations can be characterized as lenient versions of choice operations where choices are retractable, being allowed to be reconsidered any finite number of times. This way, they model trialanderror style decision steps in interactive computation. The main technical result of this paper is constructing a sound and complete axiomatization for the propositional fragment of computability logic whose vocabulary, together with negation, includes all four  parallel, toggling, sequential and choice  kinds of conjunction and disjunction. Along with toggling conjunction and disjunction, the paper also introduces the toggling versions of quantifiers and recurrence operations. 
Title:  Ptarithmetic 
Author:  Dr. Giorgi Japaridze 
Abstract:  The present article introduces ptarithmetic (short for "polynomial time arithmetic")  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 an interactive numbertheoretic computational problem with a polynomial time solution and, furthermore, such a solution can be effectively extracted from a proof of T. And complete in the sense that every interactive numbertheoretic problem with a polynomial time solution is represented by some theorem T of the system. The paper is selfcontained, and can be read without any previous familiarity with computability logic. 
2008 

Title:  Towards applied theories based on computability logic 
Author:  Dr. Giorgi Japaridze 
Abstract:  Computability logic (CL) (see this http URL) 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 respect to the semantics of CL. Conservatively extending classical predicate calculus and offering considerable additional expressive and deductive power, CL12 presents a reasonable, computationally meaningful, constructive alternative to classical logic as a basis for applied theories. To obtain a model example of such theories, this paper rebuilds the traditional, classicallogicbased Peano arithmetic into a computabilitylogicbased counterpart. Among the purposes of the present contribution is to provide a starting point for what, as the author wishes to hope, might become a new line of research with a potential of interesting findings  an exploration of the presumably quite unusual metatheory of CLbased arithmetic and other CLbased applied systems. 
2007 

Title:  Sequential operators in computability logic 
Author:  Dr. Giorgi Japaridze 
Abstract:  Computability logic (CL) is a semantical platform and research program for redeveloping logic as a formal theory of computability, as opposed to the formal theory of truth which it has more traditionally been. Formulas in CL stand for (interactive) computational problems, understood as games between a machine and its environment; logical operators represent operations on such entities; and "truth" is understood as existence of an effective solution, i.e., of an algorithmic winning strategy.
The formalism of CL is openended, and may undergo series of extensions as the study of the subject advances. The main groups of operators on which CL has been focused so far are the parallel, choice, branching, and blind operators. The present paper introduces a new important group of operators, called sequential. The latter come in the form of sequential conjunction and disjunction, sequential quantifiers, and sequential recurrences. As the name may suggest, the algorithmic intuitions associated with this group are those of sequential computations, as opposed to the intuitions of parallel computations associated with the parallel group of operations: playing a sequential combination of games means playing its components in a sequential fashion, one after one. The main technical result of the present paper is a sound and complete axiomatization of the propositional fragment of computability logic whose vocabulary, together with negation, includes all three  parallel, choice and sequential  sorts of conjunction and disjunction. An extension of this result to the firstorder level is also outlined. 
Title:  Four concepts and two logics of algorithmic reduction 
Author:  Dr. Giorgi Japaridze 
Abstract:  Within the program of finding axiomatizations for various parts of computability logic, an earlier article proved 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 reduction into the logic of the second sort of reduction takes nothing more than just deleting the contraction rule from its Gentzenstyle axiomatization. The first (Turing) sort of interactive reduction is also shown to come in three natural versions. While those three versions are very different from each other, their logical behaviors (in isolation) turn out to be indistinguishable, with that common behavior being precisely captured by implicative intuitionistic logic. An online source on computability logic can be found here. 
Title:  Cirquent calculus deepened 
Author:  Dr. Giorgi Japaridze 
Abstract:  Cirquent calculus is a new prooftheoretic framework, originally motivited by the needs of computability logic (see here). Its main distinguishing feature is sharing: unlike the more traditional frameworks that manipulate tree or forestlike objects such as formulas, sequents or hypersequents, cirquent calculus deals with circuitstyle structures called cirquents. The present article elaborates a deepinference cirquent calculus system CL8 for classical propositional logic and the corresponding fragment of the resourceconscious computability logic. It also shows the existence of polynomialsize analytic CL8proofs of the pigeonhole principle  the family of tautologies known to have no such proofs in traditional systems. 
2006 

Title:  The logic of interactive Turing reduction 
Author:  Dr. Giorgi Japaridze 
Abstract:  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. See this http URL for a comprehensive online source on computability logic. 
Title:  The intuitionistic fragment of computability logic at the propositional level 
Author:  Dr. Giorgi Japaridze 
Abstract:  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 deterministicchoice combinations of problems (disjunction = machine's choice, conjunction = environment's choice), and "absurd" as a computational problem of universal strength. See this http URL for a comprehensive online source on computability logic. 
Title:  Demanddriven Inlinig in a Regionbased Optimizer for ILP Architectures 
Author:  Dr. Tom Way 
Abstract:  Regionbased compilation repartitions a program into more desirable compilation units using profiling information and procedure inlining to enable region formation analysis. This paper presents an interprocedural compilation technique which performs procedure inlining ondemand, rather than as a separate phase, to improve the ability of a regionbased optimizer to control code growth, compilation time and memory usage while improving performance. Experimental results are presented to evaluate the impact of the algorithm and several inlining heuristics upon a number of traditional and novel compilation characteristics within a regionbased ILP compiler and simulator. 
Title:  Exploring Computer Science Concepts with a Readymade Computer Game Framework 
Author:  Dr. Tom Way 
Abstract:  Leveraging the prevailing interest in computer games among college students, both for entertainment and as a possible career path, is a major reason for the increasing prevalence of computer game design courses in computer science curricula. Because implementing a computer game requires strong programming skills, game design courses are most often restricted to more advanced computer science students. This paper reports on a readymade game design and experimentation framework, implemented in Java, that makes game programming more widely accessible. This framework, called Labyrinth, enables students at all programming skill levels to participate in computer game design. We describe the architecture of the framework, and discuss programming projects suitable for a wide variety of computer science courses, from capstone to nonmajor. 
2005 

Title:  Intuitionistic computability logic I 
Author:  Dr. Giorgi Japaridze 
Abstract:  Computability logic (CL) is a systematic formal theory of computational tasks and resources, which, in a sense, can be seen as a semanticsbased alternative to (the syntactically introduced) linear logic. With its expressive and flexible language, where formulas represent computational problems and "truth" is understood as algorithmic solvability, CL potentially offers a comprehensive logical basis for constructive applied theories and computing systems inherently requiring constructive and computationally meaningful underlying logics. Among the best known constructivistic logics is Heyting's intuitionistic calculus INT, whose language can be seen as a special fragment of that of CL. The constructivistic philosophy of INT, however, has never really found an intuitively convincing and mathematically strict semantical justification. CL has good claims to provide such a justification and hence a materialization of Kolmogorov's known thesis "INT = logic of problems". The present paper contains a soundness proof for INT with respect to the CL semantics. It is expected to constitute part 1 of a twopiece series on the intuitionistic fragment of CL, with part 2 containing an anticipated completeness proof. A comprehensive online source on CL is available this http URL. 
Title:  From truth to computability I 
Author:  Dr. Giorgi Japaridze 
Abstract:  The recently initiated approach called computability logic is a formal theory of interactive computation. See a comprehensive online source on the subject at this http URL . The present paper contains a soundness and completeness proof for the deductive system CL3 which axiomatizes the most basic firstorder fragment of computability logic called the finitedepth, elementarybase fragment. Among the potential application areas for this result are the theory of interactive computation, constructive applied theories, knowledgebase systems, systems for resourcebound planning and action. This paper is selfcontained as it reintroduces all relevant definitions as well as main motivations. 
Title:  From truth to computability II 
Author:  Dr. Giorgi Japaridze 
Abstract:  Computability logic is a formal theory of computational tasks and resources. Formulas in it represent interactive computational problems, and "truth" is understood as algorithmic solvability. Interactive computational problems, in turn, are defined as a certain sort games between a machine and its environment, with logical operators standing for operations on such games. Within the ambitious program of finding axiomatizations for incrementally rich fragments of this semantically introduced logic, the earlier article "From truth to computability I" proved soundness and completeness for system CL3, whose language has the so called parallel connectives (including negation), choice connectives, choice quantifiers, and blind quantifiers. The present paper extends that result to the significantly more expressive system CL4 with the same collection of logical operators. What makes CL4 expressive is the presence of two sorts of atoms in its language: elementary atoms, representing elementary computational problems (i.e. predicates, i.e. problems of zero degree of interactivity), and general atoms, representing arbitrary computational problems. CL4 conservatively extends CL3, with the latter being nothing but the generalatomfree fragment of the former. Removing the blind (classical) group of quantifiers from the language of CL4 is shown to yield a decidable logic despite the fact that the latter is still firstorder. A comprehensive online source on computability logic can be found at this http URL 
Title:  Propositional computability logic II 
Author:  Dr. Giorgi Japaridze 
Abstract:  Computability logic is a formal theory of computational tasks and resources. Its formulas represent interactive computational problems, logical operators stand for operations on computational problems, and validity of a formula is understood as being a scheme of problems that always have algorithmic solutions. A comprehensive online source on the subject is available at this http URL . The earlier article "Propositional computability logic I" proved soundness and completeness for the (in a sense) minimal nontrivial fragment CL1 of computability logic. The present paper extends that result to the significantly more expressive propositional system CL2. What makes CL2 more expressive than CL1 is the presence of two sorts of atoms in its language: elementary atoms, representing elementary computational problems (i.e. predicates), and general atoms, representing arbitrary computational problems. CL2 conservatively extends CL1, with the latter being nothing but the generalatomfree fragment of the former. 
Title:  An O(n log n)Time Algorithm for the Restricted Scaffold Assignment 
Author:  Dr. Mirela Damian 
Abstract:  The assignment problem takes as input two finite point sets S and T and establishes a correspondence between points in S and points in T, such that each point in S maps to exactly one point in T, and each point in T maps to at least one point in S. In this paper we show that this problem has an O(n log n)time solution, provided that the points in S and T are restricted to lie on a line (linear time, if S and T are presorted). 
Title:  In the beginning was game semantics 
Author:  Dr. Giorgi Japaridze 
Abstract:  This paper presents an overview of computability logic  the gamesemantically constructed logic of interactive computational tasks and resources. A comprehensive online source on the subject can be found at this http URL. 
Title:  Introduction to Cirquet Calculus and Abstract Resource Semantics 
Author:  Dr. Giorgi Japaridze 
Abstract:  This paper introduces a refinement of the sequent calculus approach called cirquent calculus. While in Gentzenstyle proof trees sibling (or cousin, etc.) sequents are disjoint sequences of formulas, in cirquent calculus they are permitted to share elements. Explicitly allowing or disallowing shared resources and thus taking to a more subtle level the resourceawareness intuitions underlying substructural logics, cirquent calculus offers much greater flexibility and power than sequent calculus does. A need in substantially new deductive tools came with the birth of computability logic (see this http URL)  the semantically constructed formal theory of computational resources, which has stubbornly resisted any axiomatization attempts within the framework of traditional syntactic approaches. Cirquent calculus breaks the ice. Removing contraction from the full collection of its rules yields a sound and complete system for the basic fragment CL5 of computability logic. Doing the same in sequent calculus, on the other hand, throws out the baby with the bath water, resulting in the strictly weaker affine logic. An implied claim of computability logic is that it is CL5 rather than affine logic that adequately materializes the resource philosophy traditionally associated with the latter. To strengthen this claim, the paper further introduces an abstract resource semantics and shows the soundness and completeness of CL5 with respect to it. 
2004 

Title:  Computability Logic: a formal theory of interaction 
Author:  Dr. Giorgi Japaridze 
Abstract:  Computability logic is a formal theory of (interactive) computability in the same sense as classical logic is a formal theory of truth. This approach was initiated very recently in "Introduction to computability logic" (Annals of Pure and Applied Logic 123 (2003), pp.199). The present paper reintroduces computability logic in a more compact and less technical way. It is written in a semitutorial style with a general computer science, logic or mathematics audience in mind. An Internet source on the subject is available at this http URL, and additional material at this http URL. 
Title:  Propositional computability logic I 
Author:  Dr. Giorgi Japaridze 
Abstract:  In the same sense as classical logic is a formal theory of truth, the recently initiated approach called computability logic is a formal theory of computability. It understands (interactive) computational problems as games played by a machine against the environment, their computability as existence of a machine that always wins the game, logical operators as operations on computational problems, and validity of a logical formula as being a scheme of "always computable" problems. The present contribution gives a detailed exposition of a soundness and completeness proof for an axiomatization of one of the most basic fragments of computability logic. The logical vocabulary of this fragment contains operators for the so called parallel and choice operations, and its atoms represent elementary problems, i.e. predicates in the standard sense. This article is selfcontained as it explains all relevant concepts. While not technically necessary, however, familiarity with the foundational paper "Introduction to computability logic" [Annals of Pure and Applied Logic 123 (2003), pp.199] would greatly help the reader in understanding the philosophy, underlying motivations, potential and utility of computability logic,  the context that determines the value of the present results. Online introduction to the subject is available at this http URL and this http URL. 
2003 

Title:  The Evolution of the Computerized Database 
Author:  Ms. Nancy Bercich 
Advisor:  Dr. Don Goelman 
Abstract:  Databases, collections of related data, are as old as the written word. A database can be anything from a homemaker's metal recipe file to a sophisticated data warehouse. Yet today, when we think of a database we invariably think of computerized data and their DBMSs (database management systems). This paper defines what we mean by a database. It traces the evolution of the database, from its start as a noncomputerized set of related data, to the, now standard, computerized RDBMS (relational database management system). It discusses how these RDBMSs relate to the objectoriented paradigm. It considers future trends in DBMSs. 
2002 

Title:  Complex Systems 
Author:  Dr. Jeffrey Smith 
Advisor:  Dr. Dan Joyce 
Abstract:  The study of Complex Systems is considered by many to be a new scientific field, and is distinguished by being a discipline that has applications within many separate areas of scientific study. The study of Neural Networks, Traffic Patterns, Artificial Intelligence, Social Systems, and many other scientific areas can all be considered to fall within the realm of Complex Systems. This paper provides a general overview of the science of Complex Systems, including terminology, definitions, history, and examples. 