Citations of:
An algebraic theory of normal forms
Annals of Pure and Applied Logic 71 (3):189245 (1995)
Add citations
You must login to add citations.


In a previous work we introduced the algorithm \SQEMA\ for computing firstorder equivalents and proving canonicity of modal formulae, and thus established a very general correspondence and canonical completeness result. \SQEMA\ is based on transformation rules, the most important of which employs a modal version of a result by Ackermann that enables elimination of an existentially quantified predicate variable in a formula, provided a certain negative polarity condition on that variable is satisfied. In this paper we develop several extensions of (...) 

This paper provides several examples of how modal logic can be used in studying the XML document navigation language XPath. More specifically, we derive complete axiomatizations, computational complexity and expressive power results for XPath fragments from known results for corresponding logics. A secondary aim of the paper is to introduce XPath in a way that makes it accessible to an audience of modal logicians. 

The role played by continuous morphisms in propositional modal logic is investigated: it turns out that they are strictly related to filtrations and to suitable variants of the notion of a free algebra. We also employ continuous morphisms in incremental constructions of finitely generated free. 

This paper obtains the weak completeness and decidability results for standard systems of modal logic using models built from formulas themselves. This line of work began with Fine (Notre Dame J. Form. Log. 16:229237, 1975). There are two ways in which our work advances on that paper: First, the definition of our models is mainly based on the relation Kozen and Parikh used in their proof of the completeness of PDL, see (Theor. Comp. Sci. 113118, 1981). The point is to (...) 

We show that (contrary to the parallel case of intuitionistic logic, see [7], [4]) there does not exist a translation fromS42 (the propositional modal systemS4 enriched with propositional quantifiers) intoS4 that preserves provability and reduces to identity for Boolean connectives and. 

In this article, we tell a story about incompleteness in modal logic. The story weaves together an article of van Benthem, “Syntactic aspects of modal incompleteness theorems,” and a longstanding open question: whether every normal modal logic can be characterized by a class of completely additive modal algebras, or as we call them, ${\cal V}$baos. Using a firstorder reformulation of the property of complete additivity, we prove that the modal logic that starred in van Benthem’s article resolves the open question (...) 



A. M. Pitts in [Pi] proved that HA op fp is a biHeyting category satisfying the Lawrence condition. We show that the embedding $\Phi: HA^\mathrm{op}_\mathrm{fp} \longrightarrow Sh(\mathbf{P_0,J_0})$ into the topos of sheaves, (P 0 is the category of finite rooted posets and open maps, J 0 the canonical topology on P 0 ) given by $H \longmapsto HA(H,\mathscr{D}()): \mathbf{P_0} \longrightarrow \text{Set}$ preserves the structure mentioned above, finite coproducts, and subobject classifier, it is also conservative. This whole structure on HA op (...) 

Here, we provide a detailed description of the mutual relation of formulas with finite propositional variables p1, …, pm in modal logic S4. Our description contains more information on S4 than those given in Shehtman (1978) and Moss (2007); however, Shehtman (1978) also treated Grzegorczyk logic and Moss (2007) treated many other normal modal logics. Specifically, we construct normal forms, which behave like the principal conjunctive normal forms in the classical propositional logic. The results include finite and effective methods to (...) 



Inspired by the recent work on approximations of classical logic, we present a method that approximates several modal logics in a modular way. Our starting point is the limitation of the ndegree of introspection that is allowed, thus generating modalnlogics. The semantics for nlogics is presented, in which formulas are evaluated with respect to paths, and not possible worlds. A tableaubased proof system is presented, nSST, and soundness and completeness is shown for the approximation of modal logics image and image. 

