@ARTICLE{DBLP:journals/jsyml/OkadaT99, AUTHOR = {Mitsuhiro Okada and Kazushige Terui}, TITLE = {{The} Finite Model Property for Various Fragments of Intuitionistic Linear Logic}, JOURNAL = {Journal of Symbolic Logic}, VOLUME = {64}, NUMBER = {2}, YEAR = {1999}, PAGES = {790-802}, BIBSOURCE = {DBLP, http://dblp.uni-trier.de}, URL = {http://www.jstor.org/sici?sici=0022-4812%28199906%2964%3A2%3C790%3ATFMPFV%3E2%2E0%2ECO%3B2-L&origin=euclid&cookieSet=1}, ABSTRACT = {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). } }

@INPROCEEDINGS{DBLP:conf/lics/Terui01, AUTHOR = {Kazushige Terui}, TITLE = {{Light} Affine Lambda Calculus and Polytime Strong Normalization}, BOOKTITLE = {Proceedings of LICS'01}, YEAR = {2001}, BIBSOURCE = {DBLP, http://dblp.uni-trier.de}, NOTE = {See [Ter07a] for the journal version.}, ABSTRACT = { 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 "weak" normalization theorem). In this paper, we introduce an untyped term calculus, called the light affine lambda calculus (lambda-LA), generalizing the essential ideas of light logics into an untyped framework. It is a simple modification of the lambda-calculus, and has ILAL as a type assignment system. Then, in this generalized setting, we prove the polytime "strong" normalization theorem: any reduction strategy normalizes a given lambda-LA term (of fixed depth) in a polynomial number of reduction steps, and indeed in polynomial time} }

@INPROCEEDINGS{DBLP:conf/ictcs/MairsonT03, AUTHOR = {Harry G. Mairson and Kazushige Terui}, TITLE = {{On} the Computational Complexity of Cut-Elimination in Linear Logic}, BOOKTITLE = {Proceedings of ICTCS'03}, PUBLISHER = {LNCS 2841}, YEAR = {2003}, PAGES = {23-36}, BIBSOURCE = {DBLP, http://dblp.uni-trier.de}, PDF = {http://www.kurims.kyoto-u.ac.jp/~terui/cep.pdf}, ABSTRACT = {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).} }

@ARTICLE{DBLP:journals/sLogica/Terui04, AUTHOR = {Kazushige Terui}, TITLE = {{Light} Affine Set Theory: A Naive Set Theory of Polynomial Time}, JOURNAL = {Studia Logica}, VOLUME = {77}, NUMBER = {1}, YEAR = {2004}, PAGES = {9-40}, URL = {http://www.springerlink.com/index/10.1023/B:STUD.0000034183.33333.6f}, BIBSOURCE = {DBLP, http://dblp.uni-trier.de}, PDF = {http://www.kurims.kyoto-u.ac.jp/~terui/lastfin.pdf}, ABSTRACT = {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. In this paper, we consider a naive set theory based on Intuitionistic Light Affine Logic (ILAL), a simplification of LLL introduced by (Asperti 1998), and call it Light Affine Set Theory (LAST). The simplicity of LAST allows us to rigorously verify its polytime character. In particular, we prove that a function over words is computable in polynomial time if and only if it is provably total in LAST.} }

@INPROCEEDINGS{DBLP:conf/lics/BaillotT04, AUTHOR = {Patrick Baillot and Kazushige Terui}, TITLE = {{Light} Types for Polynomial Time Computation in Lambda-Calculus}, BOOKTITLE = {Proceedings of LICS'04}, YEAR = {2004}, PAGES = {266-275}, URL = {http://csdl.computer.org/comp/proceedings/lics/2004/2192/00/21920266abs.htm}, BIBSOURCE = {DBLP, http://dblp.uni-trier.de}, NOTE = {See [BT08] for the journal version.}, ABSTRACT = {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. } }

@INPROCEEDINGS{DBLP:conf/lics/Terui04, AUTHOR = {Kazushige Terui}, TITLE = {{Proof} Nets and Boolean Circuits}, BOOKTITLE = {Proceedings of LICS'04}, YEAR = {2004}, PAGES = {182-191}, URL = {http://csdl.computer.org/comp/proceedings/lics/2004/2192/00/21920182abs.htm}, BIBSOURCE = {DBLP, http://dblp.uni-trier.de}, PDF = {http://www.kurims.kyoto-u.ac.jp/~terui/pn.pdf}, ABSTRACT = {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). } }

@INPROCEEDINGS{DBLP:conf/tlca/BaillotT05, AUTHOR = {Patrick Baillot and Kazushige Terui}, TITLE = {{A} Feasible Algorithm for Typing in Elementary Affine Logic}, BOOKTITLE = {Proceedings of TLCA'05}, PUBLISHER = {LNCS 3461}, YEAR = {2005}, PAGES = {55-70}, URL = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3461{\&}spage=55}, BIBSOURCE = {DBLP, http://dblp.uni-trier.de}, PDF = {http://www.kurims.kyoto-u.ac.jp/~terui/inferEALfinal.pdf}, ABSTRACT = { 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.} }

@ARTICLE{DBLP:journals/sLogica/CiabattoniT06, AUTHOR = {Agata Ciabattoni and Kazushige Terui}, TITLE = {{Towards} a Semantic Characterization of Cut-Elimination}, JOURNAL = {Studia Logica}, VOLUME = {82}, NUMBER = {1}, YEAR = {2006}, PAGES = {95-119}, URL = {http://dx.doi.org/10.1007/s11225-006-6607-2}, PDF = {http://www.kurims.kyoto-u.ac.jp/~terui/ciabteruiSLfinal.pdf}, BIBSOURCE = {DBLP, http://dblp.uni-trier.de}, NOTE = {Corrigenda: \url{http://www.kurims.kyoto-u.ac.jp/~terui/corrigendaSL.pdf}}, ABSTRACT = {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.} }

@INPROCEEDINGS{DBLP:conf/lpar/CiabattoniT06, AUTHOR = {Agata Ciabattoni and Kazushige Terui}, TITLE = {{Modular} Cut-Elimination: Finding Proofs or Counterexamples}, BOOKTITLE = {Proceedings of LPAR'06}, PUBLISHER = {LNAI 4246}, YEAR = {2006}, PAGES = {135-149}, URL = {http://dx.doi.org/10.1007/11916277_10}, PDF = {http://www.kurims.kyoto-u.ac.jp/~terui/lpar2006.pdf}, BIBSOURCE = {DBLP, http://dblp.uni-trier.de}, ABSTRACT = {Modular cut-elimination is a particular notion of "cut-elimination in the presence of non-logical axioms" that is preserved under the addition of suitable rules. We introduce syntactic necessary and sufficient conditions for modular cut-elimination for standard calculi, a wide class of (possibly) multiple-conclusion sequent calculi with generalized quantifiers. We provide a "universal" modular cut-elimination procedure that works uniformly for any standard calculus satisfying our conditions. The failure of these conditions generates counterexamples for modular cut-elimination and, in certain cases, for cut-elimination.} }

@INPROCEEDINGS{DBLP:conf/csl/AtassiBT06, AUTHOR = {Vincent Atassi and Patrick Baillot and Kazushige Terui}, TITLE = {{Verification} of Ptime Reducibility for System {F} Terms Via Dual Light Affine Logic}, BOOKTITLE = {Proceedings of CSL'06}, YEAR = {2006}, PAGES = {150-166}, URL = {http://dx.doi.org/10.1007/11874683_10}, BIBSOURCE = {DBLP, http://dblp.uni-trier.de}, NOTE = {See [ABT07] for the journal version.}, ABSTRACT = {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. } }

@ARTICLE{DBLP:journals/lmcs/AtassiBT07, AUTHOR = {Vincent Atassi and Patrick Baillot and Kazushige Terui}, TITLE = {{Verification} of Ptime Reducibility for system {F} Terms: Type Inference in Dual Light Affine Logic}, JOURNAL = {Logical Methods in Computer Science}, VOLUME = {3}, NUMBER = {4}, YEAR = {2007}, URL = {http://dx.doi.org/10.2168/LMCS-3(4:10)2007}, BIBSOURCE = {DBLP, http://dblp.uni-trier.de}, ABSTRACT = {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. } }

@ARTICLE{DBLP:journals/aml/Terui07, AUTHOR = {Kazushige Terui}, TITLE = {{Light} affine lambda calculus and polynomial time strong normalization}, JOURNAL = {Archive for Mathematical Logic}, VOLUME = {46}, NUMBER = {3-4}, YEAR = {2007}, PAGES = {253-280}, URL = {http://dx.doi.org/10.1007/s00153-007-0042-6}, BIBSOURCE = {DBLP, http://dblp.uni-trier.de}, PDF = {http://www.kurims.kyoto-u.ac.jp/~terui/lalcjournal.pdf}, ABSTRACT = {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 "weak" normalization theorem, it is natural to ask whether a "strong" form of polynomial time normalization theorem holds or not. In this paper, we introduce an untyped term calculus, called Light Affine Lambda Calculus (lambda-LA), which corresponds to ILAL. Lambda-LA is a bi-modal lambda-calculus with certain constraints, endowed with very simple reduction rules. The main property of lambda-LA is the polynomial time strong normalization: any reduction strategy normalizes a given lambda-LA term in a polynomial number of reduction steps, and indeed in polynomial time. Since proofs of ILAL are structurally representable by terms of lambda-LA, we conclude that the same holds for ILAL.} }

@INPROCEEDINGS{Terui97, AUTHOR = {Mitsuhiro Okada and Kazushige Terui}, TITLE = {{Semantic} Characterizations for Reachability and Trace Equivalence in a Linear Logic-Based Process Calculus}, BOOKTITLE = {RIMS Koukyuroku 976: Symposium on Proof Theory and Ordinals}, PAGES = {146--168}, EDITOR = {T. Arai}, YEAR = {1997}, PUBLISHER = {Research Institute for Mathematical Sciences, Kyoto University}, PDF = {http://www.kurims.kyoto-u.ac.jp/~terui/process.pdf}, URL = {http://www.kurims.kyoto-u.ac.jp/~kyodo/kokyuroku/contents/976.html}, ABSTRACT = { We give semantic characterizations for reachability and trace equivalence in a version of asynchronous process calculus based on linear logic. Usually the reachability relation in linear logic-based process calculi is characterized by the logical notion of provability, which is in turn characterized by model-theoretic semantics such as phase semantics. We introduce considerably simplified phase models, which we call naive phase models, and show that reachability is also characterized by the completeness with respect to the naive phase models. On the other hand, logical provability does not provide any satisfactory notion of equivalence on processes. We consider the trace equivalence (Hoare 1980) on our process calculus and introduce certain algebraic models, which we call trace models. Then the trace equivalence is characterized by the completeness with respect to the trace models.} }

@INPROCEEDINGS{Terui98, AUTHOR = {Mitsuhiro Okada and Kazushige Terui}, TITLE = {{Completeness} proofs for linear logic based on the proof search method (preliminary report)}, BOOKTITLE = {RIMS Koukyuroku 1023: Type theory and its applications to computer systems}, PAGES = {57--75}, EDITOR = {J. Garrigue}, YEAR = {1998}, PUBLISHER = {Research Institute for Mathematical Sciences, Kyoto University}, PDF = {http://www.kurims.kyoto-u.ac.jp/~terui/proofsearch.pdf}, URL = {http://www.kurims.kyoto-u.ac.jp/~kyodo/kokyuroku/contents/1023.html}, ABSTRACT = {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). Under the proofs-as-processes correspondence, Linear Logic proof search can be identified with a theory of asyncronous concurrent process calculus. Based on this paradigm, we apply our technique to construct a denotational semantics for the concurrent process calculus.} }

@PHDTHESIS{Terui2002phd, AUTHOR = {Kazushige Terui}, TITLE = {{Light} Logic and Polynomial Time Computation}, SCHOOL = {Keio University}, YEAR = {2002}, MONTH = {March}, PDF = {http://www.kurims.kyoto-u.ac.jp/~terui/phd.pdf} }

@ARTICLE{Terui07, AUTHOR = {Kazushige Terui}, TITLE = {{Which} Structural Rules Admit Cut Elimination? an Algebraic Criterion}, JOURNAL = {Journal of Symbolic Logic}, VOLUME = {72}, NUMBER = {3}, YEAR = {2007}, PAGES = {738-754}, URL = {http://projecteuclid.org/DPubS?service=UI&version=1.0&verb=Display&handle=euclid.jsl/1191333839}, PDF = {http://www.kurims.kyoto-u.ac.jp/~terui/cutfinal.pdf}, ABSTRACT = {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. We consider full Lambek calculus (FL), i.e., intuitionistic logic without any structural rules, as our basic framework. Residuated lattices are the algebraic structures corresponding to FL. In this setting, we introduce a criterion, called the propagation property, that can be stated both in syntactic and algebraic terminologies. We then show that, for any set R of structural rules, the cut elimination theorem holds for FL enriched with R if and only if R satisfies the propagation property. As an application, we show that any set R of structural rules can be "completed" into another set R*, so that the cut elimination theorem holds for FL enriched with R*, while the provability remains the same.} }

@ARTICLE{KOT06, AUTHOR = {Max I. Kanovich and Mitsuhiro Okada and Kazushige Terui}, TITLE = {{Intuitionistic} Phase Semantics is Almost Classical}, JOURNAL = {Mathematical Structures in Computer Science}, VOLUME = {16}, YEAR = {2006}, PAGES = {1-20}, URL = {http://portal.acm.org/citation.cfm?id=1127700&dl=&coll=&CFID=15151515&CFTOKEN=6184618}, PDF = {http://www.kurims.kyoto-u.ac.jp/~terui/iphasemscsfinal.pdf}, ABSTRACT = {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 "almost classical" phase space. Here, by an `"almost classical" phase space we mean a phase space having a double-negation-like closure operator. Based on these semantic considerations, we give a syntactic embedding of propositional ILL into LL.} }

@ARTICLE{BT08, AUTHOR = {Patrick Baillot and Kazushige Terui}, TITLE = {{Light} Types for Polynomial Time Computation in Lambda Calculus}, JOURNAL = {Information and Computation}, VOLUME = {207}, NUMBER = {1}, PAGES = {41-62}, YEAR = {2009}, PDF = {http://www.kurims.kyoto-u.ac.jp/~terui/DlalLongFinal.pdf}, ABSTRACT = { 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.} }

@MISC{Terui08, AUTHOR = {Kazushige Terui}, TITLE = {{Computational} Ludics}, NOTE = {To appear in Theoretical Computer Science}, YEAR = {2008}, PDF = {http://www.kurims.kyoto-u.ac.jp/~terui/ludicslatest.pdf}, ABSTRACT = {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. 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.} }

@INPROCEEDINGS{DBLP:conf/lics/CiabattoniGT08, AUTHOR = {Agata Ciabattoni and Nikolaos Galatos and Kazushige Terui}, TITLE = {{From} Axioms to Analytic Rules in Nonclassical Logics}, BOOKTITLE = {Proceedings of LICS'08}, YEAR = {2008}, PAGES = {229-240}, URL = {http://doi.ieeecomputersociety.org/10.1109/LICS.2008.39}, PDF = {http://www.kurims.kyoto-u.ac.jp/~terui/lics08.pdf}, BIBSOURCE = {DBLP, http://dblp.uni-trier.de}, ABSTRACT = {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.} }

@MISC{Terui99, AUTHOR = {Kazushige Terui}, TITLE = {{Labelled} Tableau Calculi Generating Simple Models for Substructural Logics}, NOTE = {ILLC Research Report PP-1999-04, University of Amsterdam}, YEAR = {1999}, PDF = {http://www.kurims.kyoto-u.ac.jp/~terui/lintab.pdf}, ABSTRACT = {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.} }

@MISC{Terui98b, AUTHOR = {Kazushige Terui}, TITLE = {{Anaphoric} Linking at Run Time: A Type-Logical Account of Discourse Representation}, NOTE = {ILLC Research Report LP-1998-17, University of Amsterdam}, YEAR = {1998}, PDF = {http://www.kurims.kyoto-u.ac.jp/~terui/drt.pdf}, ABSTRACT = {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. To settle this difficulty, we shall propose a new type-logical framework of DRT in which anaphoric linking takes place during the construction of DRSs (Run Time Anaphoric Linking). The construction is bottom-up in the sense that it is based on the sequent calculus proof search of Lambek calculus. We exploit quantifier types to represent the run time anaphoric linking mechanism. We shall briefly illustrate how plural anaphora are treated in our framework. In particular, we shall show that Summation and Abstraction, which are used to create suitable antecedent discourse referents for plural pronouns in (Kamp and Reyle 1993), are available in our type-logical setting using the linear logic modality.} }

@MISC{AGT08, AUTHOR = {Agata Ciabattoni and Nikolaos Galatos and Kazushige Terui}, TITLE = {Algebraic Proof Theory for Substructural Logics: Cut-Elimination and Completions}, NOTE = {Submitted}, YEAR = {2008}, PDF = {http://www.kurims.kyoto-u.ac.jp/~terui/apt.pdf}, ABSTRACT = {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. We introduce the substructural hierarchy -- a new classification of logical axioms (algebraic equations) over full Lambek calculus FL, and show that cut-elimination for extensions of FL and the MacNeille completion for subvarieties of pointed residuated lattices coincide up to the level N2 in the hierarchy. Negative results, which indicate limitations of cut-elimination and the MacNeille completion, as well as of the expressive power of structural sequent rules, are also provided. Our arguments interweave proof theory and algebra, leading to an integrated discipline which we call algebraic proof theory.} }

@MISC{BT09, AUTHOR = {Michele Basaldella and Kazushige Terui}, TITLE = {On the meaning of logical completeness}, NOTE = {A revised version of a submitted paper}, YEAR = {2009}, PDF = {http://www.kurims.kyoto-u.ac.jp/~terui/meaning.pdf}, ABSTRACT = {G\"odel's completeness theorem is concerned with provability. We look for its analogue for proofs in the monistic framework of Girard's Ludics. Following a previous work, we consider an extension of the original Ludics with duplication and (universal) nondeterminism in order to capture a polarized fragment of linear logic and thus a constructive variant of propositional classical logic. We then prove a completeness theorem for proofs in this extended setting: for any formula A and any design P, either P is a proof of A or there is a model M in the negation of A which beats P. Compared with proofs of full completeness in Game Semantics, ours exhibits a striking similarity with proofs of G\"odelian completeness, in that it explicitly constructs a countermodel essentially using K\"onig's lemma, proceeds by induction on formulas, and implies an analogue of L\"owenheim-Skolem theorem.} }

*This file has been generated by
bibtex2html 1.79*