@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