In [14], we studied the computational behaviour of various first-order and modal languages interpreted in metric or weaker distance spaces. [13] gave an axiomatisation of an expressive and decidable metric logic. The main result of this paper is in showing that the technique of representing metric spaces by means of Kripke frames can be extended to cover the modal (hybrid) language that is expressively complete over metric spaces for the (undecidable) two-variable fragment of first-order logic with binary pred-icates interpreting the (...) metric. The frame conditions needed correspond rather directly with a Boolean modal logic that is, again, of the same expressivity as the two-variable fragment. We use this representation to derive an axiomatisation of the modal hybrid variant of the two-variable fragment, discuss the compactness property in distance logics, and derive some results on (the failure of) interpolation in distance logics of various expressive power. (shrink)

We investigate the major mathematical theories of space from a modal standpoint: topology, affine geometry, metric geometry, and vector algebra. This allows us to see new fine-structure in spatial patterns which suggests analogies across these mathematical theories in terms of modal, temporal, and conditional logics. Throughout the modal walk through space, expressive power is analyzed in terms of language design, bisimulations, and correspondence phenomena. The result is both unification across the areas visited, and the uncovering of interesting new questions.

This paper is devoted to the completeness issue of RMLCI — the relative modal logic with composition and intersection— a restriction of the propositional dynamic logic with intersection. The trouble with RMLCI is that the operation of intersection is not modally definable. Using the notion of mosaics, we give a new proof of a theorem considered in a previous paper “Complete axiomatization of a relative modal logic with composition and intersection”. The theorem asserts that the proof theory of RMLCI is (...) complete for the standard Kripke semantics of RMLCI. (shrink)

We introduce and study a variety of modal logics of parallelism, orthogonality, and affine geometries, for which we establish several completeness, decidability and complexity results and state a number of related open, and apparently difficult problems. We also demonstrate that lack of the finite model property of modal logics for sufficiently rich affine or projective geometries (incl. the real affine and projective planes) is a rather common phenomenon.

We survey main developments, results, and open problems on interval temporal logics and duration calculi. We present various formal systems studied in the literature and discuss their distinctive features, emphasizing on expressiveness, axiomatic systems, and (un)decidability results.

This paper is devoted to the complete axiomatization of dynamic extensions of arrow logic based on a restriction of propositional dynamic logic with intersection. Our deductive systems contain an unorthodox inference rule: the inference rule of intersection. The proof of the completeness of our deductive systems uses the technique of the canonical model.

ABSTRACT George Gargov was an active pioneer in the ‘Sofia School’ of modal logicians. Starting in the 1970s, he and his colleagues expanded the scope of the subject by introducing new modal expressive power, of various innovative kinds. The aim of this paper is to show some general patterns behind such extensions, and review some very general results that we know by now, 20 years later. We concentrate on simulation invariance, decidability, and correspondence. What seems clear is that ‘modal logic’ (...) as a genre of logical systems has a much wider scope than originally conceived, and that we have not reached its limits yet. (shrink)

Logic is not just about single-agent notions like reasoning, or zero-agent notions like truth, but also about communication between two or more people. What we tell and ask each other can be just as 'logical' as what we infer in Olympic solitude. We show how such interactive phenomena can be studied systematically by merging epistemic and dynamic logic.

The aim of this paper is to give new kinds of modal logics suitable for reasoning about regions in discrete spaces. We call them dynamic logics of the region-based theory of discrete spaces. These modal logics are linguistic restrictions of propositional dynamic logic with the global diamond E. Their formulas are equivalent to Boolean combinations of modal formulas like E(A ∧ ⟨α⟩ B) where A and B are Boolean terms and α is a relational term. Examining what we can say (...) about dynamic models when we use formulas to describe them, we successively address the axiomatization/completeness issue and the decidability/complexity issue of our dynamic logics of the region-based theory of discrete spaces. (shrink)

Spatio-temporal logic is a variant of branching temporal logic where one of the so-called causal relations on spacetime plays the role of a time flow. Allowing only rational numbers as space and time co-ordinates, we prove that a first-order spatio-temporal theory over this flow is recursively enumerable if and only if the dimension of spacetime does not exceed 2. The situation is somewhat different compared to the case of real co-ordinates, because we establish that even dimension 2 does not permit (...) recursive enumerability in this case. The proof of the result on rational spacetime involves a more deeper portion of spacetime geometry than the corresponding, more evident result for the real co-ordinates. (shrink)

Proc. of the 8th International Conference on Advances in Modal Logic, (AiML'2010).

We consider the problem of axiomatizing various natural "successor" logics for 2-dimensional integral spacetime. We provide axiomatizations in monomodal and multimodal languages, and prove completeness theorems. We also establish that the irreflexive successor logic in the "standard" modal language (i.e. the language containing □ and ◊) is not finitely axiomatizable.

In this paper we show that the class of fork squares has a complete orthodox axiomatization in fork arrow logic (FAL). This result may be seen as an orthodox counterpart of Venema's non-orthodox axiomatization for the class of squares in arrow logic. FAL is the modal logic of fork algebras (FAs) just as arrow logic is the modal logic of relation algebras (RAs). FAs extend RAs by a binary fork operator and are axiomatized by adding three equations to RAs equational (...) axiomatization. A proper FA is an algebra of relations where the fork is induced by an injective operation coding pair formation. In contrast to RAs, FAs are representable by proper ones and their equational theory has the expressive power of full first-order logic. A square semantics (the set of arrows is U×U for some set U) for arrow logic was defined by Y. Venema. Due to the negative results about the finite axiomatizability of representable RAs, Venema provided a non-orthodox finite axiomatization for arrow logic by adding a new rule governing the applications of a difference operator. We address here the question of extending the type of relational structures to define orthodox axiomatizations for the class of squares. Given the connections between this problem and the finitization problem addressed by I. Németi, we suspect that this cannot be done by using only logical operations. The modal version of the FA equations provides an orthodox axiomatization for FAL which is complete in view of the representability of FAs. Here we review this result and carry it further to prove that this orthodox axiomatization for FAL also axiomatizes the class of fork squares. (shrink)

ABSTRACT George Gargov was an active pioneer in the ‘Sofia School’ of modal logicians. Starting in the 1970s, he and his colleagues expanded the scope of the subject by introducing new modal expressive power, of various innovative kinds. The aim of this paper is to show some general patterns behind such extensions, and review some very general results that we know by now, 20 years later. We concentrate on simulation invariance, decidability, and correspondence. What seems clear is that ‘modal logic’ (...) as a genre of logical systems has a much wider scope than originally conceived, and that we have not reached its limits yet. (shrink)

The paper introduces a first-order theory in the language of predicate tense logic which contains a single simple axiom. It is shewn that this theory enables times to be referred to and sentences involving ‘now’ and ‘then’ to be formalised. The paper then compares this way of increasing the expressive capacity of predicate tense logic with other mechanisms, and indicates how to generalise the results to other modal and tense systems.

In epistemic logic, some axioms dealing with the notion of knowledge are rather convoluted and difficult to interpret intuitively, even though some of them, such as the axioms.2 and.3, are considered to be key axioms by some epistemic logicians. We show that they can be characterized in terms of understandable interaction axioms relating knowledge and belief or knowledge and conditional belief. In order to show it, we first sketch a theory dealing with the characterization of axioms in terms of interaction (...) axioms in modal logic. We then apply the main results and methods of this theory to obtain specific results related to epistemic and doxastic logics. (shrink)

This paper addresses questions of universality related to ontological engineering, namely aims at substantiating (negative) answers to the following three basic questions: (i) Is there a ‘universal ontology’?, (ii) Is there a ‘universal formal ontology language’?, and (iii) Is there a universally applicable ‘mode of reasoning’ for formal ontologies? To support our answers in a principled way, we present a general framework for the design of formal ontologies resting on two main principles: firstly, we endorse Rudolf Carnap’s principle of logical (...) tolerance by giving central stage to the concept of logical heterogeneity, i.e. the use of a plurality of logical languages within one ontology design. Secondly, to structure and combine heterogeneous ontologies in a semantically well-founded way, we base our work on abstract model theory in the form of institutional semantics, as forcefully put forward by Joseph Goguen and Rod Burstall. In particular, we employ the structuring mechanisms of the heterogeneous algebraic specification language HetCasl for defining a general concept of heterogeneous, distributed, highly modular and structured ontologies, called hyperontologies. Moreover, we distinguish, on a structural and semantic level, several different kinds of combining and aligning heterogeneous ontologies, namely integration, connection, and refinement. We show how the notion of heterogeneous refinement can be used to provide both a general notion of sub-ontology as well as a notion of heterogeneous equivalence of ontologies, and finally sketch how different modes of reasoning over ontologies are related to these different structuring aspects. (shrink)

In a number of publications A.N. Prior considered the use of what he called ‘metric tense logic’. This is a tense logic in which the past and future operators P and F have an index representing a temporal distance, so that Pnα means that α was true n -much ago, and Fn α means that α will be true n -much hence. The paper investigates the use of metric predicate tense logic in formalising phenomena ormally treated by such devices as (...) multiple indexing or quantification over times. (shrink)

Providing a compositional interpretation procedure for discourses in which descriptions of complex dependencies between interrelated objects are incrementally built is a key challenge for formal theories of natural language interpretation. This paper examines several quantificational phenomena and argues that to account for these phenomena, we need richly structured contexts of interpretation that are passed on between different parts of the same sentence and also across sentential boundaries. The main contribution of the paper is showing how we can add structure to (...) contexts in an incremental way, starting with the basic notion of context in classical first-order logic, i.e., interpretation contexts formalized as single total variable assignments. (shrink)

Some initial motivations for the Guarded Fragment still seem of interest in carrying its program further. First, we stress the equivalence between two perspectives: (a) satisfiability on standard models for guarded first-order formulas, and (b) satisfiability on general assignment models for arbitrary first-order formulas. In particular, we give a new straightforward reduction from the former notion to the latter. We also show how a perspective shift to general assignment models provides a new look at the fixed-point extension LFP(FO) of first-order (...) logic, making it decidable. Next, we relate guarded syntax to earlier quantifier restriction strategies for achieving effective axiomatizability in second-order logic – pointing at analogies with ‘persistent’ formulas, which are essentially in the Bounded Fragment of many-sorted first-order logic. Finally, we look at some further unexplored directions, including the systematic use of ‘quasi-models’ as a semantics by itself. (shrink)

One of the important extensions of PDL is PDL with intersection of programs. We devote this paper to its complete axiomatization.