格值模态命题逻辑及其完备性

文中以满足第一及第二无限分配律的完备格为工具,建立了格值模态命题逻辑的语义理论,并指出这种语义是经典模态命题逻辑语义理论及[0,1]值模态命题逻辑语义理论的共同推广.给出了QMR0代数的定义,并分别以Boole代数及QMR0代数为背景构建了Boole型格值模态命题逻辑系统B及QMR0型格值模态命题逻辑系统QML*,并证明了系统B及系统QML*的完备性.     

A new modal logic for reasoning about space: spatial propositional neighborhood logic

It is widely accepted that spatial reasoning plays a central role in artificial intelligence, for it has a wide variety of potential applications, e.g., in robotics, geographical information systems, and medical analysis and diagnosis. While spatial reasoning has been extensively studied at the algebraic level, modal logics for spatial reasoning have received less attention in the literature. In this paper we propose a new modal logic, called spatial propositional neighborhood logic (SpPNL for short) for spatial reasoning through directional relations. We study the expressive power of SpPNL, we show that it is able to express meaningful spatial statements, we prove a representation theorem for abstract spatial frames, and we devise a (non-terminating) sound and complete tableaux-based deduction system for it. Finally, we compare SpPNL with the well-known algebraic spatial reasoning system called rectangle algebra.      

On combinations of propositional dynamic logic and doxastic modal logics

We prove completeness and decidability results for a family of combinations of propositional dynamic logic and unimodal doxastic logics in which the modalities may interact. The kind of interactions we consider include three forms of commuting axioms, namely, axioms similar to the axiom of perfect recall and the axiom of no learning from temporal logic, and a Church–Rosser axiom. We investigate the influence of the substitution rule on the properties of these logics and propose a new semantics for the test operator to avoid unwanted side effects caused by the interaction of the classic test operator with the extra interaction axioms. This paper is a revised and extended version of Schmidt and Tishkovsky (2003).     

Transforming equality logic to propositional logic

We investigate and compare various ways of transforming equality formulas to propositional formulas, in order to be able to solve satisfiability in equality logic by means of satisfiability in propositional logic. We propose equality substitution as a new approach combining desirable properties of earlier methods, we prove its correctness and show its applicability by experiments.     

Some properties of fuzzy reasoning in propositional fuzzy logic systems

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 R₀-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.     

Dempster-shafer approach in propositional logic

A general framework of uncertainty reasoning based on Dempster-Shafer's theory is proposed in the context of logic calculus. Under this framework, any inference can be conducted without much computational complexity. Furthermore, it avoids the problems of considering conflicting information and common universe when two pieces of evidence are combined. © 1993 John Wiley & Sons, Inc.     

Monotonic and nonmonotonic gentzen deduction systems for L3-valued propositional logic

A sequent is a pair (Γ, Δ), which is true under an assignment if either some formula in Γ is false, or some formula in Δ is true. In L₃-valued propositional logic, a multisequent is a triple Δ|Θ|Γ, which is true under an assignment if either some formula in Δ has truth-value t, or some formula in Θ has truth-value m, or some formula in Γ has truth-value f. Correspondingly there is a sound and complete Gentzen deduction system G for multisequents which is monotonic. Dually, a comultisequent is a triple Δ : Θ : Γ, which is valid if there is an assignment v in which each formula in Δ has truth-value≠t, each formula in Θ has truth-value≠m, and each formula in Γ has truth-value≠f. Correspondingly there is a sound and complete Gentzen deduction system G⁻ for co-multisequents which is nonmonotonic.     

Sequential method in propositional dynamic logic

Summary Recently prepositional modal logic of programs, called prepositional dynamic logic, has been developed by many authors, following the ideas of Fisher and Ladner [1] and Pratt [12]. The main purpose of this paper is to present a Gentzen-type sequential formulation of this logic and to establish its semantical completeness with due regard to sequential formulation as such. In a sense our sequential formulation might be regarded as a powerful tool to establish the completeness theorem of already familiar axiomatizations of prepositional dynamic logic such as seen in Harel [4], Parikh [11] or Segerberg [15]. Indeed our method is powerful enough in completeness proof to yield a desired structure directly without making a detour through such intermediate constructs as a pseudomodel or a nonstandard structure, which can be seen in Parikh [11]. We also show that our sequential system of prepositional dynamic logic does not enjoy the so-called cut-elimination theorem.     

命题逻辑中广义MP问题的合理解

在经典命题逻辑中基于公式的真度概念提出了公式之间的支持度,利用支持度的思想引入了广义MP问题的一种新型合理求解机制,并证明了合理解的存在性。     

Phase semantics for a pure noncommutative linear propositional logic

We use a many-sorted language to remove commutativity from phase semantics of linear logic an show that pure noncommutative intuitionistic linear propositional logic plus two classical rules enjoys the soundness and completeness with respect to completely noncommutative phase semantics.     

启发式方法生成命题逻辑可读证明

探讨了自动生成命题逻辑系统R的可读证明.采用试探法和自然推理法分别从前推和后推模拟人类思维求证,试探法根据推理规则将待证公式反向分解,自然推理法从假设出发根据推理规则生成新的公式.两种方法都实现了相干命题逻辑系统R的可读证明,并结合实现了混合证明.试探法和自然推理法是生成可读证明的有效方法,前推和后推两种思维方法也适用于其他逻辑系统的自动证明.     

Optimization techniques for propositional intuitionistic logic and their implementation

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.     

Belief revision within fragments of propositional logic

Belief revision has been extensively studied in the framework of propositional logic, but just recently revision within fragments of propositional logic has gained attention. Hereby it is not only the belief set and the revision formula which are given within a certain language fragment, but also the result of the revision has to be located in the same fragment. So far, research in this direction has been mainly devoted to the Horn fragment of classical logic. Here we present a general approach to define new revision operators derived from known operators, such that the result of the revision remains in the fragment under consideration. Our approach is not limited to the Horn case but applicable to any fragment of propositional logic where the models of the formulas are closed under a Boolean function. Thus we are able to uniformly treat cases as dual Horn, Krom and affine formulas, as well.     

An arithmetical hierarchy in propositional dynamic logic

We prove that any alternation of modalities in PDL adds to its expressive power. The proof uses Turing machine models where PDL formulas define the arithmetical hierarchy of sets. As a by-product, we obtain a theorem of Berman and Paterson.     

Symbolic backward reachability with effectively propositional logic

We describe a symbolic procedure for solving the reachability problem of transition systems that use formulae of Effectively Propositional Logic to represent sets of backward reachable states. We discuss the key ideas for the mechanization of the procedure where fix-point checks are reduced to SMT problems. We also show the termination of the procedure on a sub-class of transition systems. Then, we discuss how reachability problems for this sub-class can be used to encode analysis problems of administrative policies in the Role-Based Access Control (RBAC) model that is one of the most widely adopted access control paradigms. An implementation of a refinement of the backward reachability procedure, called asasp, shows better flexibility and scalability than a state-of-the-art tool on a significant set of security problems.