共查询到20条相似文献,搜索用时 55 毫秒
1.
We introduce a substructural propositional calculus of Sequential Dynamic Logic that subsumes a propositional part of dynamic predicate logic, and is shown to be expressively equivalent to propositional dynamic logic. Completeness of the calculus with respect to the intended relational semantics is established. 相似文献
2.
逻辑系统NMG 的满足性和紧致性 总被引:1,自引:1,他引:0
紧致性是模糊逻辑的一个重要性质.现已经证明?ukasiewicz 命题逻辑、G?del 命题逻辑、乘积命题逻辑和形式系统L*都是紧的.通过刻画逻辑系统NMG 中的极大相容理论和证明NMG 的满足性,进而证明了NMG也是紧的. 相似文献
3.
A foundational development of propositional fuzzy logic programs is presented. Fuzzy logic programs are structured knowledge bases including uncertainties in rules and facts. The precise specifications of uncertainties have a great influence on the performance of the knowledge base. It is shown how fuzzy logic programs can be transformed to neural networks, where adaptations of uncertainties in the knowledge base increase the reliability of the program and are carried out automatically. 相似文献
4.
Extended IF 逻辑是一阶逻辑的扩张,其主要特点是可表达量词间的相互依赖和独立关系,但其命题部分至今没有得到公理化.基于Cirquent 演算方法,给出了一个关于Cirquent 语义(命题水平)可靠完备的形式系统.该系统能够很好地解释和表达命题联结词间的相互依赖和独立关系,从而使Extended IF 逻辑在命题水平得到了真正意义上的公理化. 相似文献
5.
6.
Ciftcibasi T. Altunay D. 《IEEE transactions on systems, man, and cybernetics. Part A, Systems and humans : a publication of the IEEE Systems, Man, and Cybernetics Society》1998,28(5):662-677
Fuzzy propositional logic structure is summarized; different forms of fuzzy propositional expressions and their relations are discussed. Two-sided fuzzy proposition is defined in propositional logic algebra as the counterpart of intuitionistic fuzzy set. The concept of two-sided fuzzy reasoning is discussed and its mathematical structure is developed. Using two-sided fuzzy propositions, human decision-making can be closely simulated by considering his perception of both (somewhat opposite) sides of the subject matter simultaneously. Multiuniverse two-sided fuzzy propositions are presented and multiuniverse operations are defined. Two-sided fuzzy if-then rules are investigated under different interpretations of fuzzy implications, Approximate of these different implications and the inferences in the output universe are investigated, and associated error terms are identified 相似文献
7.
《Information and Computation》2000,156(1-2):320-344
This paper compares the expressive power of first-order monadic logic of order, a fundamental formalism in mathematical logic and the theory of computation, with that of the propositional version of duration calculus (PDC), a formalism for the specification of real-time systems. Our results show that the propositional duration calculus is expressively complete for first-order monadic logic of order. Our semantics for PDC conservatively extends the standard semantics to all positive (including infinite) length intervals. Hence, in view of the expressive completeness, liveness properties can be specified in PDC. This observation refutes a widely believed misconception that the duration calculus cannot specify liveness properties. 相似文献
8.
Beatrice Capitani Michele Loreti Betti Venneri 《Electronic Notes in Theoretical Computer Science》2001,50(2):178-195
We aim at investigating the intersection-type assignment system for lambda calculus, with the Curry-Howard approach. We devise a propositional logic, whose notable characteristic is the presence of the hyperformulae denoting parallel compositions of formulae. As such, this logic formalizes a novel notion of parallel deductions, while forming a simple generalization of the standard natural deduction framework.We prove that the logical calculus is isomorphic to the intersection type system, by mapping logical deductions into typed lambda terms, encoding those deductions, and conversely. In this context the intersection type constructor, which comes out to be a proof-theoretic operator, is now interpreted as a standard propositional connective. 相似文献
9.
Guido Fiorino 《Journal of Automated Reasoning》2001,27(3):297-311
We present a tableau calculus for propositional Dummett logic, also known as LC (Linear Chain), where the depth of the deductions is linearly bounded by the length of the formulas to be proved. We then show that it is possible to decide propositional Dummett logic in O(nlogn)-SPACE. 相似文献
10.
张胜礼 《计算机科学与探索》2014,(4):494-505
对于模糊知识及其否定关系,潘正华指出应该明确地分为矛盾否定关系、对立否定关系和中介否定关系,并建立了一种具有矛盾否定、对立否定和中介否定的模糊集FScom(fuzzy sets with contradictory negation, opposite negation and medium negation),随后建立了一种改进的模糊集IFScom(improved FScom)。为给模糊集FScom及其改进IFScom提供一种逻辑工具,提出了一种带有矛盾否定、对立否定和中介否定的模糊命题逻辑演算系统FPcom,并在给定无穷值语义赋值模型以及可满足性定义下,证明了FPcom具有可靠性和完备性。FPcom在一定意义上可视为对中介命题演算系统的改进。 相似文献
11.
In order to analyze the logical foundation of fuzzy reasoning, this paper first introduces the concept of generalized roots of theories in ?ukasiewicz propositional fuzzy logic ?uk, Gödel propositional fuzzy logic Göd, Product propositional fuzzy logic Π, and nilpotent minimum logic NM (the R0-propositional fuzzy logic L∗). Next, it is proved that all consequences of a theory Γ, named D(Γ), are completely determined by its generalized root whenever Γ has a generalized root. Moreover, it is proved that every finite theory Γ has a generalized root, which can be expressed by a specific formula. Finally, we demonstrate the existence of a non-fuzzy version of Fuzzy Modus Ponens (FMP) in ?uk, Göd, Π and NM (L∗), and we provide its numerical version as a new algorithm for solving FMP. 相似文献
12.
13.
14.
15.
Chad E. Brown 《Journal of Automated Reasoning》2013,51(1):57-77
We describe a complete theorem proving procedure for higher-order logic that uses SAT-solving to do much of the heavy lifting. The theoretical basis for the procedure is a complete, cut-free, ground refutation calculus that incorporates a restriction on instantiations. The refined nature of the calculus makes it conceivable that one can search in the ground calculus itself, obtaining a complete procedure without resorting to meta-variables and a higher-order lifting lemma. Once one commits to searching in a ground calculus, a natural next step is to consider ground formulas as propositional literals and the rules of the calculus as propositional clauses relating the literals. With this view in mind, we describe a theorem proving procedure that primarily generates relevant formulas along with their corresponding propositional clauses. The procedure terminates when the set of propositional clauses is unsatisfiable. We prove soundness and completeness of the procedure. The procedure has been implemented in a new higher-order theorem prover, Satallax, which makes use of the SAT-solver MiniSat. We also describe the implementation and give several examples. Finally, we include experimental results of Satallax on the higher-order part of the TPTP library. 相似文献
16.
基于支持度理论的广义Modus Ponens问题的最优解 总被引:1,自引:0,他引:1
为了将模糊推理纳入逻辑的框架并从语构和语义两个方面为模糊推理奠定严格的逻辑基础,通过将模糊推理形式化的方法移植到经典命题逻辑系统中,把FMP(fuzzy modus ponens)问题转化为GMP(generalized modus ponens)问题,并基于公式的真度概念提出了公式之间的支持度,进一步利用支持度的思想引入了GMP问题以及CGMP(collective generalized modus ponens)问题的一种新型最优求解机制.证明了最优解的存在性,同时指出,在经典命题逻辑系统中存在着与模糊逻辑完全相似的推理机制.该方法是一种程度化的方法,这就使得求解过程从算法上实现成为可能,并对知识的程度化推理有所启示. 相似文献
17.
There has been a long-lasting misunderstanding in the literature of artificial intelligence and uncertainty modeling, regarding the role of fuzzy set theory and many-valued logics. The recurring question is that of the mathematical and pragmatic meaningfulness of a compositional calculus and the validity of the excluded middle law. This confusion pervades the early developments of probabilistic logic, despite early warnings of some philosophers of probability. This paper tries to clarify this situation. It emphasizes three main points. First, it suggests that the root of the controversies lies in the unfortunate confusion between degrees of belief and what logicians call degrees of truth. The latter are usually compositional, while the former cannot be so. This claim is first illustrated by laying bare the non-compositional belief representation embedded in the standard propositional calculus. It turns out to be an all-or-nothing version of possibility theory. This framework is then extended to discuss the case of fuzzy logic versus graded possibility theory. Next, it is demonstrated that any belief representation where compositionality is taken for granted is bound to at worst collapse to a Boolean truth assignment and at best to a poorly expressive tool. Lastly, some claims pertaining to an alleged compositionality of possibility theory are refuted, thus clarifying a pervasive confusion between possibility theory axioms and fuzzy set basic connectives. 相似文献
18.
Luís S. Barbosa Manuel A. Martins Marta Carreteiro 《Journal of Logic, Language and Information》2014,23(1):31-52
This paper introduces an axiomatisation for equational hybrid logic based on previous axiomatizations and natural deduction systems for propositional and first-order hybrid logic. Its soundness and completeness is discussed. This work is part of a broader research project on the development a general proof calculus for hybrid logics. 相似文献
19.
《The Journal of Logic Programming》1992,12(3):281-298
This paper explains new results relating modal propositional logic and rewrite rule systems. More precisely, we give complete term rewriting systems for the modal propositional systems known as K, Q, T, and S5. These systems are presented as extensions of Hsiang's system for classical propositional calculus. We have checked local confluence with the rewrite rule system K.B. (cf. the Knuth-Bendix algorithm) developed by the Formel project at INRIA. We prove that these systems are noetherian, and then infer their confluence from Newman's lemma. Therefore each term rewriting system provides a new automated decision procedure and defines a canonical form for the corresponding logic. We also show how to characterize the canonical forms thus obtained. 相似文献
20.
为了提高直觉模糊命题逻辑的(α,β)-归结效率,将准锁语义归结策略应用于(α,β)-归结原理,得到直觉模糊命题逻辑的(α,β)-准锁语义归结方法,证明方法的可靠性与完备性.给出直觉模糊命题逻辑系统的(α,β)-准锁语义归结和(α,β)-准锁语义归结演绎的概念.讨论直觉模糊命题逻辑系统中的(α,β)-准锁语义归结式和锁子句的合并规则.最后,给出直觉模糊命题逻辑系统的基于(α,β)-准锁语义归结的自动推理算法步骤,并通过实例说明算法的有效性. 相似文献