[CGT12] |
Agata Ciabattoni, Nikolaos Galatos, and Kazushige Terui.
Algebraic proof theory for substructural logics: Cut-elimination and
completions.
Ann. Pure Appl. Logic, Vol. 163, No. 3, pp. 266-290, 2012.[ bib | http | .pdf ] We carry out a unified investigation of two prominent topics in proof theory and order algebra: cut-elimination and completion, in the setting of substructural logics and residuated lattices. |

[Ter12] |
Kazushige Terui.
Semantic evaluation, intersection types and complexity of simply
typed lambda calculus, 2012.
Submitted. [ bib | .pdf ] Consider the following problem: given a simply typed lambda term of Boolean type and of order r, does it normalize to ``true''? A related problem is: given a term M of word type and of order r together with a finite automaton D, does D ``accepts'' the normal form of M? We prove that these problems are n-EXPTIME complete for r= 2n +2, and n-EXPSPACE complete for r = 2n + 3. |

[Ter11] |
Kazushige Terui.
Computational ludics.
Theor. Comput. Sci., Vol. 412, No. 20, pp. 2048-2071, 2011.[ bib | http | .pdf ] We reformulate the theory of ludics introduced by J.-Y. Girard from a computational point of view. We introduce a handy term syntax for designs, the main objects of ludics. Our syntax also incorporates explicit cuts for attaining computational expressivity. In addition, we consider design generators that allow for finite representation of some infinite designs. A normalization procedure in the style of Krivine's abstract machine directly works on generators, giving rise to an effective means of computation over infinite designs. The acceptance relation between machines and words, a basic concept in computability theory, is well expressed in ludics by the orthogonality relation between designs. Fundamental properties of ludics are then discussed in this concrete context. We prove three characterization results that clarify the computational powers of three classes of designs. (i) Arbitrary designs may capture arbitrary sets of finite data. (ii) When restricted to finitely generated ones, designs exactly capture the recursively enumerable languages. (iii) When further restricted to cut-free ones as in Girard's original definition, designs exactly capture the regular languages. We finally describe a way of defining data sets by means of logical connectives, where the internal completeness theorem plays an essential role. |

[HT11] |
Rostislav Horcík and Kazushige Terui.
Disjunction property and complexity of substructural logics.
Theor. Comput. Sci., Vol. 412, No. 31, pp. 3992-4006, 2011.[ bib | http | .pdf ] We systematically identify a large class of substructural logics that satisfy the disjunction property (DP), and show that every consistent substructural logic with the DP is PSPACE-hard. Our results are obtained by using algebraic techniques. PSPACE-completeness for many of these logics is furthermore established by proof theoretic arguments. |

[CGT11] |
Agata Ciabattoni, Nikolaos Galatos, and Kazushige Terui.
Macneille completions of fl-algebras.
Algebra Universalis, Vol. 66, No. 4, pp. 405-420, 2011.[ bib | http | .pdf ] We show that a large number of equations are preserved by Dedekind-MacNeille completions when applied to subdirectly irreducible FL-algebras/residuated lattices. These equations are identified in a systematic way, based on proof-theoretic ideas and techniques in substructural logics. It follows that many varieties of Heyting algebras and FL-algebras admit completions. |

[BT10c] |
Aloïs Brunel and Kazushige Terui.
Church => scott = ptime: an application of resource sensitive
realizability.
In DICE, pp. 31-46, 2010.[ bib | http | http ] We introduce a variant of linear logic with second order quantifiers and type fixpoints, both restricted to purely linear formulas. The Church encodings of binary words are typed by a standard non-linear type `Church,' while the Scott encodings (purely linear representations of words) are by a linear type `Scott.' We give a characterization of polynomial time functions, which is derived from (Leivant and Marion 93): a function is computable in polynomial time if and only if it can be represented by a term of type Church => Scott. |

[BT10a] |
Michele Basaldella and Kazushige Terui.
Infinitary completeness in ludics.
In LICS, pp. 294-303, 2010.[ bib | http | .pdf ] Traditional Gödel completeness holds between finite proofs and infinite models over formulas of finite depth, where proofs and models are heterogeneous. Our purpose is to provide an interactive form of completeness between infinite proofs and infinite models over formulas of infinite depth (that include recursive types), where proofs and models are homogenous. |

[BT10b] |
Michele Basaldella and Kazushige Terui.
On the meaning of logical completeness.
Logical Methods in Computer Science, Vol. 6, No. 4, 2010.[ bib | http | http ] Gödel's completeness theorem is concerned with provability, while Girard's theorem in ludics (as well as full completeness theorems in game semantics) are concerned with proofs. Our purpose is to look for a connection between these two disciplines. Following a previous work [3], we consider an extension of the original ludics with contraction and universal nondeterminism, which play dual roles, in order to capture a polarized fragment of linear logic and thus a constructive variant of classical propositional logic. We then prove a completeness theorem for proofs in this extended setting: for any behaviour (formula) A and any design (proof attempt) P, either P is a proof of A or there is a model M of the orthogonal of A which defeats P. Compared with proofs of full completeness in game semantics, ours exhibits a striking similarity with proofs of Goedel's completeness, in that it explicitly constructs a countermodel essentially using Koenig's lemma, proceeds by induction on formulas, and implies an analogue of Loewenheim-Skolem theorem. |

[ACT09] |
Agata Ciabattoni, Lutz Straßburger and Kazushige Terui.
Expanding the realm of systematic proof theory, 2009.
CSL. [ bib | .pdf ] This paper is part of a general project of developing a systematic and algebraic proof theory for nonclassical logics. Generalizing our previous work on intuitionistic-substructural axioms and single-conclusion (hyper)sequent calculi, we define a hierarchy on Hilbert axioms in the language of classical linear logic without exponentials. We then give a systematic procedure to transform axioms up to the level P3' of the hierarchy into inference rules in multiple-conclusion (hyper)sequent calculi, which enjoy cut-elimination under a certain condition. This allows a systematic treatment of logics which could not be dealt with in the previous approach. Our method also works as a heuristic principle for finding appropriate rules for axioms located at levels higher than P3'. The case study of Abelian and Lukasiewicz logic is outlined. |

[BT09b] |
Michele Basaldella and Kazushige Terui.
On the meaning of logical completeness.
In TLCA, pp. 50-64, 2009.[ bib | http | .pdf ] Gödel's completeness theorem is concerned with provability, while Girard's theorem in ludics (as well as full completeness theorems in game semantics) is concerned with proofs. Our purpose is to look for a connection between these two disciplines. Following a previous work (Faggian, Basaldella 09), we consider an extension of the original ludics with contraction and universal nondeterminism, which play dual roles, in order to capture a polarized fragment of linear logic and thus a constructive variant of classical propositional logic. |

[BT09a] |
Patrick Baillot and Kazushige Terui.
Light types for polynomial time computation in lambda calculus.
Information and Computation, Vol. 207, No. 1, pp. 41-62, 2009.[ bib | .pdf ] We present a polymorphic type system for lambda calculus ensuring that well-typed programs can be executed in polynomial time: dual light affine logic (DLAL). DLAL has a simple type language with a linear and an intuitionistic type arrow, and one modality. It corresponds to a fragment of light affine logic (LAL). We show that contrarily to LAL, DLAL ensures good properties on lambda-terms (and not only on proof-nets): subject reduction is satisfied and a well-typed term admits a polynomial bound on the length of any of its beta reduction sequences. We also give a translation of LAL into DLAL and deduce from it that all polynomial time functions can be represented in DLAL. |

[CGT08a] |
Agata Ciabattoni, Nikolaos Galatos, and Kazushige Terui.
Algebraic proof theory for substructural logics: Cut-elimination and
completions, 2008.
Submitted. [ bib | .pdf ] We carry out a unified investigation of two prominent topics in proof theory and algebra: cut-elimination and completion, in the setting of substructural logics and residuated lattices. |

[Ter08] |
Kazushige Terui.
Computational ludics, 2008.
To appear in Theoretical Computer Science. [ bib | .pdf ] We reformulate the theory of ludics introduced by J.-Y. Girard from a computational point of view. We introduce a handy term syntax for designs, the main objects of ludics. Our syntax also incorporates explicit cuts for attaining computational expressivity. We also consider design generators that allow for finite representation of some infinite designs. A normalization procedure in the style of Krivine's abstract machine directly works on generators, giving rise to an effective means of computation over infinite designs. |

[CGT08] |
Agata Ciabattoni, Nikolaos Galatos, and Kazushige Terui.
From axioms to analytic rules in nonclassical logics.
In Proceedings of LICS'08, pp. 229-240, 2008.[ bib | http | .pdf ] We introduce a systematic procedure to transform large classes of (Hilbert) axioms into equivalent inference rules in sequent and hypersequent calculi. This allows for the automated generation of analytic calculi for a wide range of propositional nonclassical logics including intermediate, fuzzy and substructural logics. Our work encompasses many existing results, allows for the definition of new calculi and contains a uniform semantic proof of cut-elimination for hypersequent calculi. |

[ABT07] |
Vincent Atassi, Patrick Baillot, and Kazushige Terui.
Verification of ptime reducibility for system f terms: Type
inference in dual light affine logic.
Logical Methods in Computer Science, Vol. 3, No. 4, 2007.[ bib | http ] In a previous work Baillot and Terui introduced Dual light affine logic (DLAL) as a variant of Light linear logic suitable for guaranteeing complexity properties on lambda calculus terms: all typable terms can be evaluated in polynomial time by beta reduction and all Ptime functions can be represented. In the present work we address the problem of typing lambda-terms in second-order DLAL. For that we give a procedure which, starting with a term typed in system F, determines whether it is typable in DLAL and outputs a concrete typing if there exists any. We show that our procedure can be run in time polynomial in the size of the original Church typed system F term. |

[Ter07a] |
Kazushige Terui.
Light affine lambda calculus and polynomial time strong
normalization.
Archive for Mathematical Logic, Vol. 46, No. 3-4, pp. 253-280,
2007.[ bib | http | .pdf ] Light Linear Logic (LLL) and Intuitionistic Light Affine Logic (ILAL) are logics that capture polynomial time computation. It is known that every polynomial time function can be represented by a proof of these logics via the proofs-as-programs correspondence. Furthermore, there is a reduction strategy which normalizes a given proof in polynomial time. Given the latter polynomial time |

[Ter07b] |
Kazushige Terui.
Which structural rules admit cut elimination? an algebraic
criterion.
Journal of Symbolic Logic, Vol. 72, No. 3, pp. 738-754, 2007.[ bib | http | .pdf ] Consider a general class of structural inference rules such as exchange, weakening, contraction and their generalizations. Among them, some are harmless but others do harm to cut elimination. Hence it is natural to ask under which condition cut elimination is preserved when a set of structural rules is added to a structure-free logic. The aim of this work is to give such a condition by using algebraic semantics. |

[CT06b] |
Agata Ciabattoni and Kazushige Terui.
Towards a semantic characterization of cut-elimination.
Studia Logica, Vol. 82, No. 1, pp. 95-119, 2006.
Corrigenda:
http://www.kurims.kyoto-u.ac.jp/~terui/corrigendaSL.pdf.[ bib | http | .pdf ] We introduce necessary and sufficient conditions for a (single-conclusion) sequent calculus to admit (reductive) cut-elimination. Our conditions are formulated both syntactically and semantically. |

[CT06a] |
Agata Ciabattoni and Kazushige Terui.
Modular cut-elimination: Finding proofs or counterexamples.
In Proceedings of LPAR'06, pp. 135-149. LNAI 4246, 2006.[ bib | http | .pdf ] Modular cut-elimination is a particular notion of |

[ABT06] |
Vincent Atassi, Patrick Baillot, and Kazushige Terui.
Verification of ptime reducibility for system F terms via dual
light affine logic.
In Proceedings of CSL'06, pp. 150-166, 2006.
See [ABT07] for the journal version.[ bib | http ] In a previous work we introduced Dual Light Affine Logic (DLAL) as a variant of Light Linear Logic suitable for guaranteeing complexity properties on lambda-calculus terms: all typable terms can be evaluated in polynomial time and all Ptime functions can be represented. In the present work we address the problem of typing lambda-terms in second-order DLAL. For that we give a procedure which, starting with a term typed in system F, finds all possible ways to decorate it into a DLAL typed term. We show that our procedure can be run in time polynomial in the size of the original Church typed system F term. |

[KOT06] |
Max I. Kanovich, Mitsuhiro Okada, and Kazushige Terui.
Intuitionistic phase semantics is almost classical.
Mathematical Structures in Computer Science, Vol. 16, pp.
1-20, 2006.[ bib | http | .pdf ] We study the relationship between classical phase semantics for classical linear logic (LL) and intuitionistic phase semantics for intuitionistic linear logic (ILL). We prove that (i) every intuitionistic phase space is a subspace of a classical phase space, and (ii) every intuitionistic phase space is phase isomorphic to an |

[BT05] |
Patrick Baillot and Kazushige Terui.
A feasible algorithm for typing in elementary affine logic.
In Proceedings of TLCA'05, pp. 55-70. LNCS 3461, 2005.[ bib | http | .pdf ] We give a new type inference algorithm for typing lambda-terms in Elementary Affine Logic (EAL), which is motivated by applications to complexity and optimal reduction. Following previous references on this topic, the variant of EAL type system we consider (denoted EAL*) is a variant where sharing is restricted to variables and without polymorphism. Our algorithm improves over the ones already known in that it offers a better complexity bound: if a simple type derivation for the term is given our algorithm performs EAL* type inference in polynomial time in the size of the derivation. |

[Ter04a] |
Kazushige Terui.
Light affine set theory: A naive set theory of polynomial time.
Studia Logica, Vol. 77, No. 1, pp. 9-40, 2004.[ bib | http | .pdf ] In (Girard 1998), a naive set theory is introduced based on a polynomial time logical system, Light Linear Logic (LLL). Although it is reasonably claimed that the set theory inherits the intrinsically polytime character from the underlying logic LLL, the discussion there is largely informal, and a formal justification of the claim is not provided sufficiently. Moreover, the syntax is quite complicated in that it is based on a non-traditional hybrid sequent calculus which is required for formulating LLL. |

[BT04] |
Patrick Baillot and Kazushige Terui.
Light types for polynomial time computation in lambda-calculus.
In Proceedings of LICS'04, pp. 266-275, 2004.
See [BT08] for the journal version.[ bib | http ] We propose a new type system for lambda-calculus ensuring that well-typed programs can be executed in polynomial time: Dual light affine logic (DLAL). DLAL has a simple type language with a linear and an intuitionistic type arrow, and one modality. It corresponds to a fragment of Light affine logic (LAL). We show that contrarily to LAL, DLAL ensures good properties on lambda-terms: subject reduction is satisfied and a well-typed term admits a polynomial bound on the reduction by any strategy. Finally we establish that as LAL, DLAL allows to represent all polytime functions. |

[Ter04b] |
Kazushige Terui.
Proof nets and boolean circuits.
In Proceedings of LICS'04, pp. 182-191, 2004.[ bib | http | .pdf ] We study the relationship between proof nets for mutiplicative linear logic (with unbounded fan-in logical connectives) and Boolean circuits. We give simulations of each other in the style of the proofs-as-programs correspondence; proof nets correspond to Boolean circuits and cut-elimination corresponds to evaluation. The depth of a proof net is defined to be the maximum logical depth of cut formulas in it, and it is shown that every unbounded fan-in Boolean circuit of depth n, possibly with stCONN2 gates, is polynomially simulated by a proof net of depth O(n) and vice versa. here, stCONN2 stands for st-connectivity gates for undirected graphs of degree 2. Let APNi be the class of languages for which there is a polynomial size, log i-depth family of proof nets. We then have APNi = ACi(stCONN2). |

[MT03] |
Harry G. Mairson and Kazushige Terui.
On the computational complexity of cut-elimination in linear logic.
In Proceedings of ICTCS'03, pp. 23-36. LNCS 2841, 2003.[ bib | .pdf ] Given two proofs in a logical system with a confluent cut-elimination procedure, the cut-elimination problem (CEP) is to decide whether these proofs reduce to the same normal form. This decision problem has been shown to be PTIME-complete for Multiplicative Linear Logic (Mairson 2003). The latter result depends upon a restricted simulation of weakening and contraction for boolean values in MLL; in this paper, we analyze how and when this technique can be generalized to other MLL formulas, and then consider CEP for other subsystems of Linear Logic. We also show that while additives play the role of nondeterminism in cut-elimination, they are not needed to express deterministic PTIME computation. As a consequence, affine features are irrelevant to expressing PTIME computation. In particular, Multiplicative Light Linear Logic (MLLL) and Multiplicative Soft Linear Logic (MSLL) capture PTIME even without additives nor unrestricted weakening. We establish hierarchical results on the cut-elimination problem for MLL (PTIME-complete), MALL (coNP-complete), MSLL (EXPTIME-complete), and for MLLL (2EXPTIME-complete). |

[Ter02] |
Kazushige Terui.
Light Logic and Polynomial Time Computation.
PhD thesis, Keio University, March 2002.[ bib | .pdf ] |

[Ter01] |
Kazushige Terui.
Light affine lambda calculus and polytime strong normalization.
In Proceedings of LICS'01, 2001.
See [Ter07a] for the journal version.[ bib ] Light linear logic (LLL) and its variant, intuitionistic light affine logic (ILAL), are logics of polytime computation. All polynomial-time functions are representable by proofs of these logics (via the proofs-as-programs correspondence), and, conversely, that there is a specific reduction (cut-elimination) strategy which normalizes a given proof in polynomial time (the latter may well be called the polytime |

[OT99] |
Mitsuhiro Okada and Kazushige Terui.
The finite model property for various fragments of intuitionistic
linear logic.
Journal of Symbolic Logic, Vol. 64, No. 2, pp. 790-802, 1999.[ bib | http ] Recently (Lafont 1997) showed the finite model property for the multiplicative additive fragment of linear logic (MALL) and for affine logic (LLW), i.e., linear logic with weakening. In this paper, we shall prove the finite model property for intuitionistic versions of those, i.e. intuitionistic MALL (which we call IMALL), and intuitionistic LLW (which we call ILLW). In addition, we shall show the finite model property for contractive linear logic (LLC), i.e., linear logic with contraction, and for its intuitionistic version (ILLC). The finite model property for related substructural logics also follow by our method. In particular, we shall show that the property holds for all of FL and GL-systems except FLc and GLc of (Ono 1994), that will settle the open problems stated in (Ono 1996). |

[Ter99] |
Kazushige Terui.
Labelled tableau calculi generating simple models for substructural
logics, 1999.
ILLC Research Report PP-1999-04, University of Amsterdam. [ bib | .pdf ] In this paper we apply the methodology of Labelled Deductive Systems to the tableau method in order to obtain a deductive framework for substructural logics which incorporates the facility of model generation. For this special purpose, we propose new labelled tableau calculi TL and TLe for two substructural logics L (essentially the Lambek calculus) and Le (the multiplicative fragment of intuitionistic linear logic). The use of labels makes it possible to generate countermodels in terms of a certain very simple semantics based on monoids, which we call the simple semantics. We show that, given a formula C as input, every nonredundant tableau construction procedure for TL and TLe terminates in finitely many steps, yielding either a tableau proof of C or a finite countermodel of C in terms of the simple semantics. It shows the finite model property for L and Le with respect to the simple semantics. |

[OT98] |
Mitsuhiro Okada and Kazushige Terui.
Completeness proofs for linear logic based on the proof search
method (preliminary report).
In J. Garrigue, editor, RIMS Koukyuroku: Type theory and its
applications to computer systems, pp. 57-75. Research Institute for
Mathematical Sciences, Kyoto University, 1998.[ bib | .pdf ] We investigate a method of completeness proofs based on the labelled proof search in Linear Logic framework. This method is obtained from the usual proof search methods in classical and intuitionistic logic by considering the resource-sensitivity and concurrency of the Linear Logic. By using this method, we prove that some computationally meaningful fragments of Linear Logic are complete with respect to naive phase semantics, which is a simplification of phase semantics (the standard Tarskian-style semantics of Linear Logic). |

[Ter98] |
Kazushige Terui.
Anaphoric linking at run time: A type-logical account of discourse
representation, 1998.
ILLC Research Report LP-1998-17, University of Amsterdam. [ bib | .pdf ] A number of attempts have been made to combine Discourse Representation Theory with type-logical grammar in order to obtain a compositional (bottom-up) framework for discourse representation (e.g., Muskens 1994, van Eijck and Kamp 1997). In those attempts, however, it is usually assumed that anaphoric links are given in advance of the construction of discourse representation structures (DRSs). This assumption causes a difficulty, typically dealing with plural anaphora, because generally suitable referents of plural pronouns are not present before the construction, but should be created through the construction of DRSs. |

[OT97] |
Mitsuhiro Okada and Kazushige Terui.
Semantic characterizations for reachability and trace equivalence
in a linear logic-based process calculus.
In T. Arai, editor, RIMS Koukyuroku: Symposium on Proof Theory
and Ordinals, pp. 146-168. Research Institute for Mathematical Sciences,
Kyoto University, 1997.[ bib | .pdf ] We give semantic characterizations for reachability and trace equivalence in a version of asynchronous process calculus based on linear logic. |

*This file has been generated by
bibtex2html 1.79*