排序方式: 共有190条查询结果,搜索用时 7 毫秒
71.
We generalise the result of [H. Ganzinger, C. Meyer, M. Veanes, The two-variable guarded fragment with transitive relations, in: Proc. 14th IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1999, pp. 24–34] on decidability of the two variable monadic guarded fragment of first order logic with constraints on the guard relations expressible in monadic second order logic. In [H. Ganzinger, C. Meyer, M. Veanes, The two-variable guarded fragment with transitive relations, in: Proc. 14th IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1999, pp. 24–34], such constraints apply to one relation at a time. We modify their proof to obtain decidability for constraints involving several relations. Now we can use this result to prove decidability of multi-modal modal logics where conditions on accessibility relations involve more than one relation. Our main application is intuitionistic modal logic, where the intuitionistic and modal accessibility relations usually interact in a non-trivial way. 相似文献
72.
In the paper we explore the idea of describing Pawlak’s rough sets using three-valued logic, whereby the value t corresponds to the positive region of a set, the value f — to the negative region, and the undefined value u — to the border of the set. Due to the properties of the above regions in rough set theory, the semantics of the logic is
described using a non-deterministic matrix (Nmatrix). With the strong semantics, where only the value t is treated as designated, the above logic is a “common denominator” for Kleene and Łukasiewicz 3-valued logics, which represent
its two different “determinizations”. In turn, the weak semantics—where both t and u are treated as designated—represents such a “common denominator” for two major 3-valued paraconsistent logics.
We give sound and complete, cut-free sequent calculi for both versions of the logic generated by the rough set Nmatrix. Then
we derive from these calculi sequent calculi with the same properties for the various “determinizations” of those two versions
of the logic (including Łukasiewicz 3-valued logic). Finally, we show how to embed the four above-mentioned determinizations
in extensions of the basic rough set logics obtained by adding to those logics a special two-valued “definedness” or “crispness”
operator. 相似文献
73.
Giovanna D’Agostino 《Synthese》2008,164(3):421-435
We discuss the interpolation property on some important families of non classical logics, such as intuitionistic, modal, fuzzy,
and linear logics. A special paragraph is devoted to a generalization of the interpolation property, uniform interpolation.
Supported by PRIN project 2006/2007 ‘Large-scale development of certified mathematical proofs’. 相似文献
74.
Input/output logics are abstract structures designed to represent conditional obligations and goals. In this paper we use them to study conditional permission. This perspective provides a clear separation of the familiar notion of negative permission from the more elusive one of positive permission. Moreover, it reveals that there are at least two kinds of positive permission. Although indistinguishable in the unconditional case, they are quite different in conditional contexts. One of them, which we call static positive permission, guides the citizen and law enforcement authorities in the assessment of specific actions under current norms, and it behaves like a weakened obligation. Another, which we call dynamic positive permission, guides the legislator. It describes the limits on the prohibitions that may be introduced into a code, and under suitable conditions behaves like a strengthened negative permission. 相似文献
75.
It is known that a number of inference principles can be used to trivialise the axioms of naïve comprehension – the axioms underlying the naïve theory of sets. In this paper we systematise and extend these known results, to provide a number of general classes of axioms responsible for trivialising naïve comprehension. 相似文献
76.
In [7], 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 [1], 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 {0, 1}* is computable in polynomial time if and only if it is provably total in
LAST. 相似文献
77.
In this paper we improve the results of [2] by proving the product f.m.p. for the product of minimal n-modal and minimal n-temporal logic. For this case we modify the finite depth method introduced in [1]. The main result is applied to identify new fragments of classical first-order logic and of the equational theory of relation algebras, that are decidable and have the finite model property. 相似文献
78.
Completeness of Certain Bimodal Logics for Subset Spaces 总被引:1,自引:0,他引:1
Subset Spaces were introduced by L. Moss and R. Parikh in [8]. These spaces model the reasoning about knowledge of changing states.In [2] a kind of subset space called intersection space was considered and the question about the existence of a set of axioms that is complete for the logic of intersection spaces was addressed. In [9] the first author introduced the class of directed spaces and proved that any set of axioms for directed frames also characterizes intersection spaces.We give here a complete axiomatization for directed spaces. We also show that it is not possible to reduce this set of axioms to a finite set. 相似文献
79.
Dorota Leszczyńska-Jasion 《Journal of Philosophical Logic》2009,38(2):151-177
The aim of this paper is to present a loop-free decision procedure for modal propositional logics K4, S4 and S5. We prove that the procedure terminates and that it is sound and complete. The procedure is based on the method of Socratic
proofs for modal logics, which is grounded in the logic of questions IEL. 相似文献
80.
Josep Maria Font 《Studia Logica》2009,91(3):383-406
This is a contribution to the discussion on the role of truth degrees in manyvalued logics from the perspective of abstract
algebraic logic. It starts with some thoughts on the so-called Suszko’s Thesis (that every logic is two-valued) and on the
conception of semantics that underlies it, which includes the truth-preserving notion of consequence. The alternative usage
of truth values in order to define logics that preserve degrees of truth is presented and discussed. Some recent works studying
these in the particular cases of Łukasiewicz’s many-valued logics and of logics associated with varieties of residuated lattices
are also presented. Finally the extension of this paradigm to other, more general situations is discussed, highlighting the
need for philosophical or applied motivations in the selection of the truth degrees, due both to the interpretation of the
idea of truth degree and to some mathematical difficulties. 相似文献