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.     

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.     

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.     

Deterministic propositional dynamic logic: Finite models,complexity, and completeness

Let p be a formula in deterministic propositional dynamic logic. A decision procedure for the satisfiability of p is given along with a construction of a finite model for every satisfiable p. The decision procedure runs in deterministic time 2^cn and the size of the model is bounded by n² · 4ⁿ, where n is the length of p. Finally, a complete axiomatization for deterministic propositional dynamic logic is given, based on the Segerberg axoms for propositional dynamic logic.     

Serializable histories in quantified propositional temporal logic

The model of concurrent uninterpreted transactions [Papadimitriou, C. H. (1979). The serializability of concurrent database updates. J. ACM, 26, 631–653.] is extended to histories with infinitely many occurrences of the transactions. Such histories are viewed as models of linear temporal logic formulae with propositions representing read and write steps of transactions. A necessary and sufficient condition for histories to be serializable is encoded into temporal logic by the use of propositional quantification. The encoding differs from work on commutativity-based serializability and partial-order temporal logics in using linear temporal logic and defining serializability in terms of uninterpreted histories without reference to the state of variables. An application is the specification of a weaker form of serializability where commutativity of steps is not determined by past history.     

Computations in fragments of intuitionistic propositional logic

This article is a report on research in progress into the structure of finite diagrams of intuitionistic propositional logic with the aid of automated reasoning systems for larger calculations. Afragment of a propositional logic is the set of formulae built up from a finite number of propositional variables by means of a number of connectives of the logic, among which possibly non-standard ones like ¬¬ or which are studied here. Thediagram of that fragment is the set of equivalence classes of its formulae partially ordered by the derivability relation. N.G. de Bruijn's concept of exact model has been used to construct subdiagrams of the [p, q, , , ¬]-fragment.     

n值命题逻辑中公式的随机真度

给出了Lukasiewicz n值命题逻辑中公式的随机真度的概念,研究了其性质,利用随机真度定义了公式间的随机相似度,进而导出全体公式集上的一种伪距离。     

二值命题逻辑中逻辑理论的计量化及应用

在二值命题逻辑系统中,利用势为2的均匀概率测度空间的无穷乘积,通过计算理论[Γ]的全体模型占整个赋值空间的测度定义了理论[Γ]的真度,进而利用理论的真度简化了理论的发散度和相容度的计算公式,给出了由推理的前提集的真度估计其逻辑结论真度的表达式。     

An essay in combinatory dynamic logic

We propose a refinement of Kripke modal logic, and in particular of PDL.     

Branch-and-cut solution of inference problems in propositional logic

We describe and test computationally a branch-and-cut algorithm for solving inference problems in propositional logic. The problem is written as an integer program whose variables correspond to atomic propositions. We generate cuts for the integer program using a separation algorithm based on the resolution method for theorem proving. We find that the algorithm substantially reduces the size of the search tree when it is large. It is faster than Jeroslow and Wang's method on hard problems and slower on easy problems.Supported in part by the US Air Force Office of Scientific Research, grant AFOSR-87-0292.     

Redundancy in logic I: CNF propositional formulae

A knowledge base is redundant if it contains parts that can be inferred from the rest of it. We study some problems related to the redundancy of a CNF formula. In particular, any CNF formula can be made irredundant by deleting some of its clauses: what results is an irredundant equivalent subset. We study the complexity of problems related to irredundant equivalent subsets: verification, checking existence of an irredundant equivalent subset with a given size, checking necessary and possible presence of clauses in irredundant equivalent subsets, and uniqueness. We also consider the problem of redundancy with different definitions of equivalence.     

Social choice rules driven by propositional logic

Several rules for social choice are examined from a unifying point of view that looks at them as procedures for revising a system of degrees of belief in accordance with certain specified logical constraints. Belief is here a social attribute, its degrees being measured by the fraction of people who share a given opinion. Different known rules and some new ones are obtained depending on which particular constraints are assumed. These constraints allow to model different notions of choiceness. In particular, we give a new method to deal with approval-disapproval-preferential voting.     

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.