Axiomatisation and decidability ofF andP in cyclical time

We present a Hilert style axiomatisation for the set of formulas in the temporal language withF andP which are valid over non-transitive cyclical flows of time.We also give a simpler axiomatisation using the slightly controversial irreflexivity rule and go on to prove the decidability of any temporal logic over cyclical time provided it uses only connectives with first-order tables.     

On Modal Logics Characterized by Models with Relative Accessibility Relations: Part I

This work is divided in two papers (Part I and Part II). In Part I, we study a class of polymodal logics (herein called the class of "Rare-logics") for which the set of terms indexing the modal operators are hierarchized in two levels: the set of Boolean terms and the set of terms built upon the set of Boolean terms. By investigating different algebraic properties satisfied by the models of the Rare-logics, reductions for decidability are established by faithfully translating the Rare-logics into more standard modal logics. The main idea of the translation consists in eliminating the Boolean terms by taking advantage of the components construction and in using various properties of the classes of semilattices involved in the semantics. The novelty of our approach allows us to prove new decidability results (presented in Part II), in particular for information logics derived from rough set theory and we open new perspectives to define proof systems for such logics (presented also in Part II).     

A general method for proving decidability of intuitionistic modal logics

We generalise the result of [H. Ganzinger, C. Meyer, M. Veanes, The two-variable guarded fragment with transitive relations, in: Proc. 14th IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1999, pp. 24–34] on decidability of the two variable monadic guarded fragment of first order logic with constraints on the guard relations expressible in monadic second order logic. In [H. Ganzinger, C. Meyer, M. Veanes, The two-variable guarded fragment with transitive relations, in: Proc. 14th IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1999, pp. 24–34], such constraints apply to one relation at a time. We modify their proof to obtain decidability for constraints involving several relations. Now we can use this result to prove decidability of multi-modal modal logics where conditions on accessibility relations involve more than one relation. Our main application is intuitionistic modal logic, where the intuitionistic and modal accessibility relations usually interact in a non-trivial way.     

The complexity of satisfiability for fragments of hybrid logic—Part I

The satisfiability problem of hybrid logics with the downarrow binder is known to be undecidable. This initiated a research program on decidable and tractable fragments.In this paper, we investigate the effect of restricting the propositional part of the language on decidability and on the complexity of the satisfiability problem over arbitrary, transitive, total frames, and frames based on equivalence relations. We also consider different sets of modal and hybrid operators. We trace the border of decidability and give the precise complexity of most fragments, in particular for all fragments including negation. For the monotone fragments, we are able to distinguish the easy from the hard cases, depending on the allowed set of operators.     

FINITE MODELS CONSTRUCTED FROM CANONICAL FORMULAS

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:229–237, 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. 113–118, 1981). The point is to develop a general model-construction method based on this definition. We do this and thereby obtain the completeness of most of the standard modal systems, and in addition apply the method to some other systems of interest. None of the results use filtration, but in our final section we explore the connection.     

Decidability by filtrations for graded normal logics (graded modalities V)

We prove decidability for all of the main graded normal logics, by a notion of filtration suitably conceived for this environment.Presented byJan Zygmunt     

Information dynamics and uniform substitution

The picture of information acquisition as the elimination of possibilities has proven fruitful in many domains, serving as a foundation for formal models in philosophy, linguistics, computer science, and economics. While the picture appears simple, its formalization in dynamic epistemic logic reveals subtleties: given a valid principle of information dynamics in the language of dynamic epistemic logic, substituting complex epistemic sentences for its atomic sentences may result in an invalid principle. In this article, we explore such failures of uniform substitution. First, we give epistemic examples inspired by Moore, Fitch, and Williamson. Second, we answer affirmatively a question posed by van Benthem: can we effectively decide when every substitution instance of a given dynamic epistemic principle is valid? In technical terms, we prove the decidability of this schematic validity problem for public announcement logic (PAL and PAL-RC) over models for finitely many fully introspective agents, as well as models for infinitely many arbitrary agents. The proof of this result illuminates the reasons for the failure of uniform substitution.     

On Modal Logics Characterized by Models with Relative Accessibility Relations: Part II

This work is divided in two papers (Part I and Part II). In Part I, we introduced the class of Rare-logics for which the set of terms indexing the modal operators are hierarchized in two levels: the set of Boolean terms and the set of terms built upon the set of Boolean terms. By investigating different algebraic properties satisfied by the models of the Rare-logics, reductions for decidability were established by faithfully translating the Rare-logics into more standard modal logics (some of them contain the universal modal operator).In Part II, we push forward the results from Part I. For Rare-logics with nominals (present at the level of formulae and at the level of modal expressions), we show that the constructions from Part I can be extended although it is technically more involved. We also characterize a class of standard modal logics for which the universal modal operator can be eliminated as far as satifiability is concerned. Although the previous results have a semantic flavour, we are also able to define proof systems for Rare-logics from existing proof systems for the corresponding standard modal logics. Last, but not least, decidability results for Rare-logics are established uniformly, in particular for information logics derived from rough set theory.Since this paper is the continuation of Part I, we do not recall here the definitions of Part I although we refer to them.     

Extended Quantum Logic

The concept of quantum logic is extended so that it covers a more general set of propositions that involve non-trivial probabilities. This structure is shown to be embedded into a multi-modal framework, which has desirable logical properties such as an axiomatization, the finite model property and decidability.     

Axiomatising first-order temporal logic: Until and since over linear time

We present an axiomatisation for the first-order temporal logic with connectives Until and Since over the class of all linear flows of time. Completeness of the axiom system is proved.We also add a few axioms to find a sound and complete axiomatisation for the first order temporal logic of Until and Since over rational numbers time.The author would like to thank Dov Gabbay and Ian Hodkinson for helpful discussions on this material. The work was supported by the U.K. Science and Engineering Research Council under the Metatem project (GR/F/28526).Presented by Dov Gabbay     

Progression and Verification of Situation Calculus Agents with Bounded Beliefs

We investigate agents that have incomplete information and make decisions based on their beliefs expressed as situation calculus bounded action theories. Such theories have an infinite object domain, but the number of objects that belong to fluents at each time point is bounded by a given constant. Recently, it has been shown that verifying temporal properties over such theories is decidable. We take a first-person view and use the theory to capture what the agent believes about the domain of interest and the actions affecting it. In this paper, we study verification of temporal properties over online executions. These are executions resulting from agents performing only actions that are feasible according to their beliefs. To do so, we first examine progression, which captures belief state update resulting from actions in the situation calculus. We show that, for bounded action theories, progression, and hence belief states, can always be represented as a bounded first-order logic theory. Then, based on this result, we prove decidability of temporal verification over online executions for bounded action theories.     

Products of modal logics and tensor products of modal algebras

One of natural combinations of Kripke complete modal logics is the product, an operation that has been extensively investigated over the last 15 years. In this paper we consider its analogue for arbitrary modal logics: to this end, we use product-like constructions on general frames and modal algebras. This operation was first introduced by Y. Hasimoto in 2000; however, his paper remained unnoticed until recently. In the present paper we quote some important Hasimoto's results, and reconstruct the product operation in an algebraic setting: the Boolean part of the resulting modal algebra is exactly the tensor product of original algebras (regarded as Boolean rings). Also, we propose a filtration technique for Kripke models based on tensor products and obtain some decidability results.     

Definability and decidability of binary predicates for time granularity

In this paper we study the definability and decidability of binary predicates for time granularity in monadic languages interpreted over finitely and infinitely layered structures. We focus our attention on the equi-level (respectively equi-column) predicate constraining two time points to belong to the same layer (respectively column) and on the horizontal (respectively vertical) successor predicate relating a time point to its successor within a given layer (respectively column). We give a number of positive and negative results by reduction to/from a wide spectrum of decidable/undecidable problems.     

Normal Modal Substructural Logics with Strong Negation

We introduce modal propositional substructural logics with strong negation, and prove the completeness theorems (with respect to Kripke models) for these logics.     

Bunched sequential information

It is known that the logic BI of bunched implications is a logic of resources. Many studies have reported on the applications of BI to computer science. In this paper, an extension BIS of BI by adding a sequence modal operator is introduced and studied in order to formalize more fine-grained resource-sensitive reasoning. By the sequence modal operator of BIS, we can appropriately express “sequential information” in resource-sensitive reasoning. A Gentzen-type sequent calculus SBIS for BIS is introduced, and the cut-elimination and decidability theorems for SBIS are proved. An extension of the Grothendieck topological semantics for BI is introduced for BIS, and the completeness theorem with respect to this semantics is proved. The cut-elimination, decidability and completeness theorems for SBIS and BIS are proved using some theorems for embedding BIS into BI.     

On the Complexity of Nonassociative Lambek Calculus with Unit

Nonassociative Lambek Calculus (NL) is a syntactic calculus of types introduced by Lambek [8]. The polynomial time decidability of NL was established by de Groote and Lamarche [4]. Buszkowski [3] showed that systems of NL with finitely many assumptions are decidable in polynomial time and generate context-free languages; actually the P-TIME complexity is established for the consequence relation of NL. Adapting the method of Buszkowski [3] we prove an analogous result for Nonassociative Lambek Calculus with unit (NL1). Moreover, we show that any Lambek grammar based on NL1 (with assumptions) can be transformed into an equivalent context-free grammar in polynomial time.     

DFC-algorithms for Suszko logic and one-to-one Gentzen type formalizations

We use here the notions and results from algebraic theory of programs in order to give a new proof of the decidability theorem for Suszko logic SCI (Theorem 3).We generalize the method used in the proof of that theorem in order to prove a more general fact that any prepositional logic which admits a cut-free Gentzen type formalization is decidable (Theorem 6).We establish also the relationship between the Suszko Logic SCI, one-to-one Gentzen type formalizations and deterministic and algorithmic regular languages (Remark 2 and Theorem 7, respectively).     

A Two Dimensional Tense-modal Sortal Logic

We consider a formal language whose logical syntax involves both modal and tense propositional operators, as well as sortal quantifiers, sortal identities and (second order) quantifiers over sortals. We construct an intensional semantics for the language and characterize a formal logical system which we prove to be sound and complete with respect to the semantics. Conceptualism is the philosophical background of the semantic system.     

Δ-core Fuzzy Logics with Propositional Quantifiers, Quantifier Elimination and Uniform Craig Interpolation

In this paper we investigate the connections between quantifier elimination, decidability and Uniform Craig Interpolation in Δ-core fuzzy logics added with propositional quantifiers. As a consequence, we are able to prove that several propositional fuzzy logics have a conservative extension which is a Δ-core fuzzy logic and has Uniform Craig Interpolation.     

On Modal Logics of Partial Recursive Functions

The classical propositional logic is known to be sound and complete with respect to the set semantics that interprets connectives as set operations. The paper extends propositional language by a new binary modality that corresponds to partial recursive function type constructor under the above interpretation. The cases of deterministic and non-deterministic functions are considered and for both of them semantically complete modal logics are described and decidability of these logics is established. Presented by Melvin Fitting