共查询到20条相似文献,搜索用时 515 毫秒
1.
Maciej Kandulski 《Mathematical Logic Quarterly》1993,39(1):103-114
We show that derivations in the nonassociative and commutative Lambek calculus with product can be transformed to a normal form as it is the case with derivations in noncommutative calculi. As an application we obtain that the class of languages generated by categorial grammars based on the nonassociative and commutative Lambek calculus with product is included in the class of CF-languages. MSC: 68Q50, 03D15, 03B65. 相似文献
2.
Ryo Kashima 《Mathematical Logic Quarterly》2003,49(4):401-414
The semilattice relevant logics ∪ R , ∪ T , ∪ RW , and ∪ TW (slightly different from the orthodox relevant logics R , T , RW , and TW ) are defined by semilattice models in which conjunction and disjunction are interpreted in a natural way. For each of them, there is a cut‐free labelled sequent calculus with plural succedents (like LK ). We prove that these systems are equivalent, with respect to provable formulas, to the restricted systems with single succedents (like LJ ). Moreover, using this equivalence, we give a new Hilbert‐style axiomatizations for ∪ R and ∪ T and prove equivalence between two semantics (commutative monoid and distributive semilattice) for the contractionless logics ∪ RW and ∪ TW . 相似文献
3.
Wojciech Buszkowski 《Mathematical Logic Quarterly》2002,48(1):63-72
We give a proof of the finite model property (fmp) of some fragments of commutative and noncommutative linear logic: the Lambek calculus, BCI, BCK and their enrichments, MALL and Cyclic MALL. We essentially simplify the method used in [4] for proving fmp of BCI and the Lambek ca culus and in [5] for proving fmp of MALL. Our construction of finite models also differs from that used in Lafont [8] in his proof of fmp of MALL (we do not use cut elimination). 相似文献
4.
Kosta Doen 《Mathematical Logic Quarterly》1992,38(1):179-187
Models for the Lambek calculus of syntactic categories surveyed here are based on frames that are in principle of the same type as Kripke frames for intuitionistic logic. These models are extracted from the literature on models for relevant logics, in particular the ternary relationed models introduced in the early seventies. The purpose of this brief survey is to locate some open completeness problems for variants of the Lambek calculus in the context of completeness results based on various types of ternary relational models. 相似文献
5.
We present a new axiomatization of the non-associative Lambek calculus. We prove that it takes polynomial time to reduce any non-associative Lambek categorial grammar to an equivalent context-free grammar. Since it is possible to recognize a sentence generated by a context-free grammar in polynomial time, this proves that a sentence generated by any non-associative Lambek categorial grammar can be recognized in polynomial time. 相似文献
6.
The paper deals with the loop-rule problem in the first-order intuitionistic temporal logic sequent calculus LBJ. The calculus LBJT is intended for the specialization of the antecedent implication rule. The invertibility of some of the LBJT rules and the syntactic admissibility of the structural rules and the cut rule in LBJT, as well as the equivalence of LBJ and LBJT, are proved. The calculus LBJT2 is intended for the specialization of the antecedent universal quantifier and antecedent box rules. The decidability of LBJT2 is proved. 相似文献
7.
K. Čulík 《Periodica Mathematica Hungarica》1980,11(2):105-116
The graph of a set grammar is introduced in such a way that each set rule of the grammar is represented by a cartesian subgraph of it. The correspondence between cartesian subgraphs and transitions of Petri nets (which satisfy the axiom of extensionality) is established. The set grammars with input (initial) and output (terminal) elements are studied in an analogy to Chomsky's string grammars and their strong equivalence. Permit rules and parallel permit rules are introduced in such a way that parallel permit grammars are more general tools than Petri nets themselves, because the equivalence between homogeneous parallel permit grammars and set grammars (and Petri nets) is proved. 相似文献
8.
S. D. Kuznetsov 《Moscow University Mathematics Bulletin》2011,66(4):173-175
In this paper we present a substitution that reduces the derivability in the Lambek calculus with a unit and one division
to the derivability in the Lambek calculus with one division permitting empty antecedents. Using this substitution, we establish
the existence of an algorithm checking the derivability in the Lambek calculus with a unit and one division in polynomial
time. 相似文献
9.
Norihiro Kamide 《Mathematical Logic Quarterly》2005,51(6):579-585
The logic just corresponding to (non‐commutative) involutive quantales, which was introduced by Wendy MacCaull, is reconsidered in order to obtain a cut‐free sequent calculus formulation, and the completeness theorem (with respect to the involutive quantale model ) for this logic is proved using a new admissible rule. (© 2005 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim) 相似文献
10.
A. N. Safiullin 《Moscow University Mathematics Bulletin》2007,62(4):168-171
A method for proving the fact that any admissible in the basic Lambek calculus L rule with a premise consisting of a finite number of simple (i.e., not containing connectives) sequents is derivable is described in the paper. 相似文献
11.
S. L. Kuznetsov 《Moscow University Mathematics Bulletin》2009,64(2):76-79
The following assertion is proved: an inference rule given by a scheme is admissible in the Lambek calculus with one division L*(\) permitting empty antecedents if and only if it is admissible in the fragment of L*(\) with one primitive type L*(\; p 1). To do that, a type substitution is used which reduces the derivability in L*(\) to the derivability in L*(\; p 1). 相似文献
12.
In this paper we obtain a finite Hilbert-style axiomatization of the implicationless fragment of the intuitionistic propositional calculus. As a consequence we obtain finite axiomatizations of all structural closure operators on the algebra of {–}-formulas containing this fragment. Mathematics Subject Classification: 03B20, 03B22, 06D15. 相似文献
13.
Hassan Allouba 《随机分析与应用》2013,31(2):367-380
Abstract A peculiar feature of Itô's calculus is that it is an integral calculus that gives no explicit derivative with a systematic differentiation theory counterpart, as in elementary calculus. So, can we define a pathwise stochastic derivative of semimartingales with respect to Brownian motion that leads to a differentiation theory counterpart to Itô's integral calculus? From Itô's definition of his integral, such a derivative must be based on the quadratic variation process. We give such a derivative in this note and we show that it leads to a fundamental theorem of stochastic calculus, a generalized stochastic chain rule that includes the case of convex functions acting on continuous semimartingales, and the stochastic mean value and Rolle's theorems. In addition, it interacts with basic algebraic operations on semimartingales similarly to the way the deterministic derivative does on deterministic functions, making it natural for computations. Such a differentiation theory leads to many interesting applications, some of which we address in an upcoming article. 相似文献
14.
The Distributional Compositional Categorical (DisCoCat) model is a mathematical framework that provides compositional semantics for meanings of natural language sentences. It consists of a computational procedure for constructing meanings of sentences, given their grammatical structure in terms of compositional type-logic, and given the empirically derived meanings of their words. For the particular case that the meaning of words is modelled within a distributional vector space model, its experimental predictions, derived from real large scale data, have outperformed other empirically validated methods that could build vectors for a full sentence. This success can be attributed to a conceptually motivated mathematical underpinning, something which the other methods lack, by integrating qualitative compositional type-logic and quantitative modelling of meaning within a category-theoretic mathematical framework. The type-logic used in the DisCoCat model is Lambek?s pregroup grammar. Pregroup types form a posetal compact closed category, which can be passed, in a functorial manner, on to the compact closed structure of vector spaces, linear maps and tensor product. The diagrammatic versions of the equational reasoning in compact closed categories can be interpreted as the flow of word meanings within sentences. Pregroups simplify Lambek?s previous type-logic, the Lambek calculus. The latter and its extensions have been extensively used to formalise and reason about various linguistic phenomena. Hence, the apparent reliance of the DisCoCat on pregroups has been seen as a shortcoming. This paper addresses this concern, by pointing out that one may as well realise a functorial passage from the original type-logic of Lambek, a monoidal bi-closed category, to vector spaces, or to any other model of meaning organised within a monoidal bi-closed category. The corresponding string diagram calculus, due to Baez and Stay, now depicts the flow of word meanings, and also reflects the structure of the parse trees of the Lambek calculus. 相似文献
15.
Miroslawa Kolowska-Gawiejnowicz 《Mathematical Logic Quarterly》1999,45(1):51-58
We present a labelled version of Lambek Calculus without unit, and we use it to prove a completeness theorem for Lambek Calculus with respect to some relational semantics. 相似文献
16.
Francesco Catoni Roberto Cannata Enrico Nichelatti Paolo Zampetti 《Advances in Applied Clifford Algebras》2005,15(2):183-212
Systems of hypercomplex numbers, which had been studied and developed at the end of the 19th century, are nowadays quite unknown to the scientific community. It is believed that study of their applications ended just
before one of the fundamental discoveries of the 20th century, Einstein’s equivalence between space and time. Owing to this equivalence, not-defined quadratic forms have got concrete
physical meaning and have been recently recognized to be in strong relationship with a system of bidimensional hypercomplex
numbers. These numbers (called hyperbolic) can be considered as the most suitable mathematic language for describing the bidimensional space-time, in spite of some
unfamiliar algebraic properties common to all the commutative hypercomplex systems with more than two dimensions: they are
decomposable systems and there are non-zero numbers whose product is zero. With respect to the famous Hamilton quaternions,
one can introduce the differential calculus for the hyperbolic numbers and for all the commutative hypercomplex systems; moreover,
one can even introduce functions of hypercomplex variable.
The aim of this work is to study the systems of commutative hypercomplex numbers and the functions of hypercomplex variable
by describing them in terms of a familiar mathematical tool, i.e. matrix algebra. 相似文献
17.
Algebra and Logic - The Lambek calculus with the unit can be defined as the atomic theory (algebraic logic) of the class of residuated monoids. This calculus, being a theory of a broader class of... 相似文献
18.
We introduce a Gentzen-style sequent calculus axiomatization for Basic Predicate Calculus. Our new axiomatization is an improvement
of the previous axiomatizations, in the sense that it has the subformula property. In this system the cut rule is eliminated.
Received: 18 April 2000 / Published online: 2 September 2002
Mathematics Subject Classification (2000): Primary 03F05; Secondary 03F99, 03B60
Key words or phrases: Basic predicate calculus – Cut elimination – Sequent 相似文献
19.
Yu. V. Savateev 《Moscow University Mathematics Bulletin》2009,64(2):73-75
A polynomial algorithm for determination of derivability in the Lambek calculus with one division is described in the paper. 相似文献
20.
J. Sakalauskaitė 《Lithuanian Mathematical Journal》2006,46(3):347-355
We consider logic of knowledge and past time. This logic involves the discrete-time linear temporal operators next, until, weak yesterday, and since. In addition, it contains an indexed set of unary modal operators agent i knows.We consider the semantic constraint of the unique initial states for this logic. For the logic, we present a sequent calculus
with a restricted cut rule. We prove the soundness and completeness of the sequent calculus presented. We prove the decidability
of provability in the considered calculus as well. So, this calculus can be used as a basis for automated theorem proving.
The proof method for the completeness can be used to construct complete sequent calculi with a restricted cut rule for this
logic with other semantical constraints as well.
Published in Lietuvos Matematikos Rinkinys, Vol. 46, No. 3, pp. 427–437, July–September, 2006. 相似文献