We give a new construction of free distributive p-algebras. Our construction relies on a detailed description of completely meet-irreducible congruences, so it is purely universal algebraic. It yields a normal form theorem for p-algebra terms, simpler proofs of several existing results. As a by-product, we obtain an isomorphism between the free pseudocomplemented semilattice and the poset of join-irreducibles of the free p-algebra augmented by zero.

Ehrenfeucht-Fraïssé games provide means to characterize elementary equivalence for first-order logic, and by standard translation also for modal logics. We propose a novel generalization of Ehrenfeucht-Fraïssé games to hybrid-dynamic logics which is direct and fully modular: parameterized by the features of the hybrid language we wish to include, for instance, the modal and hybrid language operators as well as first-order existential quantification. We use these games to establish a new modular Fraïssé-Hintikka theorem for hybrid-dynamic propositional logic and its various fragments. We study the relationship between countable game equivalence (determined by countable Ehrenfeucht-Fraïssé games) and bisimulation (determined by countable back-and-forth systems). In general, the former turns out to be weaker than the latter, but under certain conditions on the language, the two coincide. As a corollary we obtain an analogue of the Hennessy-Milner theorem. We also prove that for reachable image-finite Kripke structures elementary equivalence implies isomorphism.

Abstract Lindström’s theorem characterizes first-order logic in terms of its essential model theoretic properties. One cannot gain expressive power extending first-order logic without losing at least one of compactness or downward Löwenheim–Skolem property. We cast this result in an abstract framework of institution theory, which does not assume any internal structure either for sentences or for models, so it is more general than the notion of abstract logic usually used in proofs of Lindström’s theorem; indeed, it can be said that institutional model theory is both syntax and semantics free. Our approach takes advantage of the methods of institutional model theory to provide a structured proof of Lindström’s theorem at a level of abstraction applicable to any logical system that is strong enough to describe its own concept of isomorphism and its own concept of elementary equivalence. We apply our results to some logical systems formalized as institutions and widely used in computer science practice.

Abstract We generalize the characterization of elementary equivalence by Ehrenfeucht–Fraïssé games to arbitrary institutions whose sentences are finitary. These include many-sorted first-order logic, higher-order logic with types, as well as a number of other logics arising in connection to specification languages. The gain for the classical case is that the characterization is proved directly for all signatures, including infinite ones.

Abstract Varieties like groups, rings, or Boolean algebras have the property that, in any of their members, the lattice of congruences is isomorphic to a lattice of more manageable objects, for example normal subgroups of groups, two-sided ideals of rings, filters (or ideals) of Boolean algebras. Abstract algebraic logic can explain these phenomena at a rather satisfactory level of generality: in every memberAof aτ-regular variety the lattice of congruences ofAis isomorphic to the lattice of deductive filters onAof theτ-assertional logic of . Moreover, if has a constant 1 in its type and is 1-subtractive, the deductive filters onA∈ of the 1-assertional logic of coincide with the -ideals ofAin the sense of Gumm and Ursini, for which we have a manageable concept of ideal generation. However, there are isomorphism theorems, for example, in the theories of residuated lattices, pseudointerior algebras and quasi-MV algebras that cannot be subsumed by these general results. The aim of the present paper is to appropriately generalise the concepts of subtractivity andτ-regularity in such a way as to shed some light on the deep reason behind such theorems. The tools and concepts we develop hereby provide a common umbrella for the algebraic investigation of several families of logics, including substructural logics, modal logics, quantum logics, and logics of constructive mathematics.

Constraint networks in qualitative spatial and temporal reasoning are always complete graphs. When one adds an extra element to a given network, previously unknown constraints are derived by intersections and compositions of other constraints, and this may introduce inconsistency to the overall network. Likewise, when combining two consistent networks that share a common part, the combined network may become inconsistent.

In this paper the net verification method of discrete event-driven systems modeled by UML activity diagrams is proposed. Verification is made in a formal way using a suitable procedure called activity diagram to net verifier (in short: ADN-verifier). The ADN verifier operates in two steps: (1) conversion of given activity diagram (AD) into coloured Petri net (CPN), (2) dynamic properties analysis of CPN obtained by conversion. Examination of CPN properties, exploiting Petri net theory methods, enables us to draw conclusions about dynamic properties of the original activity diagram. It was shown, that, during the conversion process, using conversion rules, dynamic properties of the model are preserved. Completeness and independence of the rules were shown as well. The following fundamental properties were shown: (i) simulation of AD by CPN obtained by conversion, and (ii) detection in finite time of any structural incorrectness in AD model by application of ADN verifier. In the case of faulty behavior detection, the method was extended to identify incorrectness in the AD model under consideration. An example of ADN verification is given in the domain of modeling discrete production systems.