Technical Reports

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 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.
Title: A PSPACE-Complete 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, PSPACE-complete.

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 PA-provably recursive time computability. This is in the sense that an arithmetical problem A has a t-time solution for some PA-provably 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 PA-provable 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 not-necessarily-constructively PA-provable 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 long-term 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 computability-in-principle. 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 complexity-oriented 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 number-theoretic 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 number-theoretic 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 open-ended, 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 circuit-style 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 independence-friendly 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 formula-based version of CL. Technically, this paper is self-contained, 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 open-ended, 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 trial-and-error 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 number-theoretic 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 number-theoretic problem with a polynomial time solution is represented by some theorem T of the system. The paper is self-contained, 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, classical-logic-based Peano arithmetic into a computability-logic-based 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 CL-based arithmetic and other CL-based 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 open-ended, 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 first-order 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 Gentzen-style 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 proof-theoretic 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 forest-like objects such as formulas, sequents or hypersequents, cirquent calculus deals with circuit-style structures called cirquents. The present article elaborates a deep-inference cirquent calculus system CL8 for classical propositional logic and the corresponding fragment of the resource-conscious computability logic. It also shows the existence of polynomial-size analytic CL8-proofs 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 deterministic-choice 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: Demand-driven Inlinig in a Region-based Optimizer for ILP Architectures
Author: Dr. Tom Way
Abstract: Region-based 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 on-demand, rather than as a separate phase, to improve the ability of a region-based 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 region-based ILP compiler and simulator.
Title: Exploring Computer Science Concepts with a Ready-made 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 ready-made 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 non-major.

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 semantics-based 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 two-piece 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 first-order fragment of computability logic called the finite-depth, elementary-base fragment. Among the potential application areas for this result are the theory of interactive computation, constructive applied theories, knowledgebase systems, systems for resource-bound planning and action. This paper is self-contained 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 general-atom-free 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 first-order. 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 general-atom-free 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 game-semantically 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 Gentzen-style 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 resource-awareness 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.1-99). 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 self-contained 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.1-99] 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 non-computerized set of related data, to the, now standard, computerized RDBMS (relational database management system). It discusses how these RDBMSs relate to the object-oriented 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.