共查询到20条相似文献,搜索用时 19 毫秒
1.
There is a correspondence between classical logic and programming language calculi with first-class continuations. With the
addition of control delimiters, the continuations become composable and the calculi become more expressive. We present a fine-grained
analysis of control delimiters and formalise that their addition corresponds to the addition of a single dynamically-scoped
variable modelling the special top-level continuation. From a type perspective, the dynamically-scoped variable requires effect
annotations. In the presence of control, the dynamically-scoped variable can be interpreted in a purely functional way by
applying a store-passing style. At the type level, the effect annotations are mapped within standard classical logic extended
with the dual of implication, namely subtraction. A continuation-passing-style transformation of lambda-calculus with control
and subtraction is defined. Combining the translations provides a decomposition of standard CPS transformations for delimited
continuations. Incidentally, we also give a direct normalisation proof of the simply-typed lambda-calculus with control and
subtraction. 相似文献
2.
A focused proof system provides a normal form to cut-free proofs in which the application of invertible and non-invertible inference rules is structured. Within linear logic, the focused proof system of Andreoli provides an elegant and comprehensive normal form for cut-free proofs. Within intuitionistic and classical logics, there are various different proof systems in the literature that exhibit focusing behavior. These focused proof systems have been applied to both the proof search and the proof normalization approaches to computation. We present a new, focused proof system for intuitionistic logic, called LJF, and show how other intuitionistic proof systems can be mapped into the new system by inserting logical connectives that prematurely stop focusing. We also use LJF to design a focused proof system LKF for classical logic. Our approach to the design and analysis of these systems is based on the completeness of focusing in linear logic and on the notion of polarity that appears in Girard’s LC and LU proof systems. 相似文献
3.
直觉模糊集时态逻辑算子及扩展运算性质 总被引:5,自引:0,他引:5
首先在考察Atanassov直觉模糊集的基本运算的基础上.引入两个典型的作用于直觉模糊集的时态逻辑算子“□(always)”和“◇(sometimes)”,重点研究了直觉模糊集在直觉模糊时态逻辑算子作用下的若干扩展运算及其性质。最后,将这些运算性质归结为一组定理,并给出详细的证明过程。 相似文献
4.
Torben Braüner 《Information and Computation》2011,209(12):1437-1446
Intuitionistic hybrid logic is hybrid modal logic over an intuitionistic logic basis instead of a classical logical basis. In this short paper we introduce intuitionistic hybrid logic and we give a survey of work in the area. 相似文献
5.
In this paper, we show the equivalence between the provability of a proof system of basic hybrid logic and that of translated
formulas of the classical predicate logic with equality and explicit substitution by a purely proof–theoretic method. Then
we show the equivalence of two groups of proof systems of hybrid logic: the group of labelled deduction systems and the group
of modal logic-based systems. 相似文献
6.
Failure mode and effects analysis (FMEA) is one of the most powerful methods in the field of risk management and has been widely used for improving process reliability in manufacturing and service sector. High applicability of FMEA has contributed to its applications in many research domains and practical fields pertaining risk assessment and system safety enhancement. However, the method has also been criticized by experts due to several weaknesses and limitations. The current study proposed a novel model for failure mode and effects analysis based on intuitionistic fuzzy approach. This approach offers some advantages over earlier models as it accounts for degrees of uncertainty in relationships among various criteria or options, specifically when relations cannot be expressed in definite numbers. The proposed model provides a tool to evaluate the failure modes, while dealing with vague concepts and insufficient data. The proposed model was tested in a case study examining the failure modes for quality of internet banking services. 相似文献
7.
直觉模糊粗糙推理的规则库完备性研究 总被引:1,自引:0,他引:1
针对规则库检验问题,提出了直觉模糊粗糙规则库的完备性检验方法.首先,引入直觉模糊粗糙集的概念,给出了直觉模糊粗糙规则库的完备性定义;其次,针对直觉模糊粗糙规则库的完备性,提出了完备性检验算法,指出如何设计规则库才能满足完备性要求;最后,通过实例验证了算法的合理性和有效性. 相似文献
8.
A logical foundation for the semantic Web 总被引:8,自引:0,他引:8
SHI Zhongzhi DONG Mingkai JIANG Yuncheng & ZHANG Haijun Key Laboratory of Intelligent Information Processing Institute of Computing Technology Chinese Acad- emy of Sciences Beijing China 《中国科学F辑(英文版)》2005,48(2):161-178
World Wide Web (WWW) has been one of important channels from which people acquire information and services, but most web pages are only used by humans at pre-sent, and these pages cannot be processed and understood automatically by computers. The semantic Web is an essential reformation of Web. The main objective of the seman-tic Web is to enrich Web with semantics and make Web be understood by computers, in order to communicate and cooperate between people and computer. The key of the se-… 相似文献
9.
An analysis of refinement in an abortive paradigm 总被引:1,自引:1,他引:0
This paper presents a new strand of investigation which complements our previous investigation of refinement for specifications whose semantics is given by partial relations (using Z as a linguistic vehicle for this semantics). It revolves around extending our mathematical apparatus so as to continue our quest for examining mathematically the essence of the lifted-totalisation semantics (which underlies the de facto standard notion of refinement in Z) and the role of the semantic elements in model-theoretic refinement, but this time in the abortive paradigm. The analysis is given in two salient parts. In the first part, we consider the simpler framework of operation-refinement: we examine the (de facto) standard account of operation-refinement in this regime by introducing a simpler, normative theory which captures the notion of firing-conditions refinement directly in the language and in terms of the natural properties of preconditions and postconditions. In the second part, we generalise our analysis to a more intricate investigation of simulation-based
data-refinement. The proof-theoretic approach we undertake in the formal analysis provides us with a mathematical apparatus which enables us to examine precisely the relationships amongst the various theories of refinement. This enables us to examine the general mathematical role that the values play in model-theoretic refinement in the abortive paradigm, as well as the significance of the unique interaction of these values with the notions of lifting (of data simulations) and lifted-totalisation (of operations) in this regime. Furthermore, we generalise this mathematical analysis to a more conceptual one which also involves extreme specifications. 相似文献
10.
首先给出直觉模糊S-粗集的基本概念,在直觉模糊S-粗集基本运算的基础上,引入两个典型的作用于直觉模糊S-粗集的时态逻辑算子"□(always)"和"◇(sometimes)",重点研究了直觉模糊S-粗集在时态逻辑算子作用下的若干扩展运算及其性质.最后将这些性质归结为定理,并给出详细的证明过程. 相似文献
11.
Yasuhito Suzuki Frank Wolter Michael Zakharyaschev 《Journal of Logic, Language and Information》1998,7(3):317-339
This paper is a comparative study of the propositional intuitionistic (non-modal) and classical modal languages interpreted in the standard way on transitive frames. It shows that, when talking about these frames rather than conventional quasi-orders, the intuitionistic language displays some unusual features: its expressive power becomes weaker than that of the modal language, the induced consequence relation does not have a deduction theorem and is not protoalgebraic. Nevertheless, the paper develops a manageable model theory for this consequence and its extensions which also reveals some unexpected phenomena. The balance between the intuitionistic and modal languages is restored by adding to the former one more implication. 相似文献
12.
The inverse method is a generalization of resolution that can be applied to non-classical logics. We have recently shown how
Andreoli’s focusing strategy can be adapted for the inverse method in linear logic. In this paper we introduce the notion
of focusing bias for atoms and show that it gives rise to forward and backward chaining, generalizing both hyperresolution
(forward) and SLD resolution (backward) on the Horn fragment. A key feature of our characterization is the structural, rather
than purely operational, explanation for forward and backward chaining. A search procedure like the inverse method is thus
able to perform both operations as appropriate, even simultaneously. We also present experimental results and an evaluation
of the practical benefits of biased atoms for a number of examples from different problem domains.
This work has been partially supported by the Office of Naval Research (ONR) under grant MURI N00014-04-1-0724 and by the
National Science Foundation (NSF) under grant CCR-0306313. The first author was partially supported by a post-doctoral fellowship
from INRIA-Futurs/école Polytechnique. 相似文献
13.
This paper presents some techniques which bound the proof search space in propositional intuitionistic logic. These techniques are justified by Kripke semantics and are the backbone of a tableau based theorem prover (PITP) implemented in C++. PITP and some known theorem provers are compared using the formulas of ILTP benchmark library. It turns out that PITP is, at the moment, the propositional prover that solves most formulas of the library. 相似文献
14.
基于IFTPN的不确定时间知识描述和推理方法 总被引:1,自引:0,他引:1
针对现有时序逻辑在对复杂不确定时间信息描述和推理方面的局限性,构造了直觉模糊时间Petri网模型(IFTPN)及其推理方法.该Petri网模型利用直觉模糊集合对模糊时延、模糊时间片进行描述,可以表达定义在离散论域或连续论域的各种不确定时间信息,并基于直觉模糊逻辑定义了模糊时间运算法则;同时,基于线性逻辑对该模型进行描述,定义了变迁之间的各种触发规则,并给出了推理方法.将该方法应用于C4ISR系统进行决策时延分析,表明了该模型及其推理方法是比较优越的. 相似文献
15.
16.
An intuitionistic fuzzy system for time series analysis in plant monitoring and diagnosis 总被引:1,自引:0,他引:1
We describe in this paper a proposed new approach for fuzzy inference in intuitionistic fuzzy systems. The new approach combines the outputs of two traditional fuzzy systems to obtain the final conclusion of the intuitionistic fuzzy system. The new method provides an efficient way of calculating the output of an intuitionistic fuzzy system, and as consequence can be applied to real-world problems in many areas of application. We illustrate the new approach with a simple example to motivate the ideas behind this work. We also illustrate the new approach for fuzzy inference with a more complicated example of monitoring a non-linear dynamic plant. 相似文献
17.
18.
Torben Braüner 《Journal of Logic, Language and Information》2006,15(3):179-194
In this paper we give axiom systems for classical and intuitionistic hybrid logic. Our axiom systems can be extended with additional rules corresponding to conditions on the accessibility relation expressed by so-called geometric theories. In the classical case other axiomatisations than ours can be found in the literature but in the intuitionistic case no axiomatisations have been published. We consider plain intuitionistic hybrid logic as well as a hybridized version of the constructive and paraconsistent logic N4. 相似文献
19.
The discoveries of continuations 总被引:4,自引:0,他引:4
John C. Reynolds 《LISP and Symbolic Computation》1993,6(3-4):233-247
We give a brief account of the discoveries of continuations and related concepts by A. van Wijngaarden, A. W. Mazurkiewicz, F. L. Morris, C. P. Wadsworth, J. H. Morris, M. J. Fischer, and S. K. Abdali. 相似文献
20.