Search

The motivation for this paper is threefold. First, we study the connectivity properties of the homomorphism order of directed graphs, and more generally for relational structures. As opposed to the homomorphism order of undirected graphs (which has no non-trivial finite maximal antichains), the order of directed graphs has finite maximal antichains of any size. In this paper, we characterise explicitly all maximal antichains in the homomorphism order of directed graphs.Quite surprisingly, these maximal antichains correspond to generalised dualities. The notion of generalised duality is defined here in full generality as an extension of the notion of finitary duality, investigated in [J. Nešetřil, C. Tardif, Duality theorems for finite structures (characterising gaps and good characterisations), J. Combin. Theory Ser. B 80 (1) (2000) 80–97]. Building upon the results of the cited paper, we fully characterise the generalised dualities. It appears that these dualities are determined by forbidding homomorphisms from a finite set of forests (rather than trees).Finally, in the spirit of [A. Atserias, On digraph coloring problems and treewidth duality, in: Proceedings of the 21st IEEE Symposium on Logic in Computer Science, LICS’06, IEEE Computer Society, 2006; B. Larose, C. Loten, C. Tardif, A characterisation of first-order constraint satisfaction problems, in: Proceedings of the 21st IEEE Symposium on Logic in Computer Science, LICS’06, IEEE Computer Society, 2006; V. Dalmau, A. Krokhin, B. Larose, First-order definable retraction problems for posets and reflexive graphs, in: Proceedings of the 19th IEEE Symposium on Logic in Computer Science, LICS’04, IEEE Computer Society, 2004 [5]] we shall characterise “generalised” constraint satisfaction problems (defined also here) that are first-order definable. These are again just generalised dualities corresponding to finite maximal antichains in the homomorphism order.

Grabmayer, Endrullis, Hendriks, Klop, and Moss [C. Grabmayer, J. Endrullis, D. Hendriks, J.W. Klop, and L.S. Moss. Automatic sequences and zipspecifications. In Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science, pages 335–344. IEEE Computer Society, 2012] developed a method for defining automatic sequences in terms of ʼzip specificationsʼ and proved that a sequence is automatic [J.-P. Allouche and J. Shallit. Automatic Sequences. Cambridge University Press, 2003] iff it has a zip specification where all zip terms have the same arity. This paper begins by investigating a similar definitional scheme for the higher-dimensional counterpart of automatic sequences, automatic arrays. In the course of establishing the results required for this machinery, we find an isomorphism–closely related to the z-order curve [G.M. Morton. A computer oriented geodetic data base and a new technique in file sequencing. International Business Machines Company, 1966]–between a final coalgebra for arrays and the standard final coalgebra for sequences. This isomorphism preserves automaticity properties: an array is k,l-automatic iff its corresponding sequence is kl-automatic. The former notion of automaticity (k,l-automatic, note the comma) is defined for arrays as in [J.-P. Allouche and J. Shallit. Automatic Sequences. Cambridge University Press, 2003], and the latter notion is the standard notion of automaticity for sequences. It also provides a convenient way to translate between stream zip specifications and array zip specifications.

We give a direct proof by generic reduction that testing validity of formulas in a decidable rudimentary theory Ω of finite typed sets Henkin, Fundamenta Mathematicae 52 (1963) 323-344) requires space and time exceeding infinitely often exp∞(exp(cn)) = 22...2}height 2cn for some constant c > 0, where n denotes the length of input. This gives the highest currently known lower bound for a decidable logical theory and affirmatively settles Problem 10.13 from (Compton and Henson, Ann. Pure Appl. Logic 48 (1990) 1-79): "Is there a "natural" decidable theory with a lower bound of the form exp∞(f(n)), where f is not linearly bounded?" The highest previously known lower (and upper) bounds for "natural" decidable theories, like WS1S, S2S, are of the form exp∞ (dn), with just linearly growing stacks of twos. Originally, the lower bound (1) for Ω was settled in (12th Annual IEEE Symposium on Logic in Computer Science (LICS'97), 1997, 294-305) using the powerful uniform lower bounds method due to Compton and Henson, and probably would never be discovered otherwise. Although very concise, the original proof has certain gaps, because the method was pushed out of the limits it was originally designed and intended for, and some hidden assumptions were violated. This results in slightly weaker bounds--the stack of twos in (1) grows subexponentially, but superpolynomially, namely, as 2c√n for formulas with fixed quantifier prefix, or as 2cn/log(n) for formulas with varying prefix. The independent direct proof presented in this paper closes the gaps and settles the originally claimed lower bound (1) for the minimally typed, succinct version of Ω.

A continuous stochastic logic with a μ -operator μ CSL is defined, and an interpretation through stochastic relations is proposed. We investigate morphisms for models of μ CSL , showing that the associated congruences can be used for an investigation of bisimilarity. The Hennessy–Milner equivalence for μ CSL is discussed, and it is shown that models are equivalent iff they are bisimilar, using a general criterion for bisimilarity from the theory of stochastic relations.

The procedure of Knuth & Bendix (In: Computational Problems in Abstract Algebras,Pergamon Press, 1970, pp. 263-297) completes a system of equations into a confluent one. It proceeds by adding critical pairs when equations superpose themselves in an ambiguous way. Huet & Hullot (Proc. 21st Symp. Foundations in Computer Science, 1980, pp 96-107) have shown that, for theories with constructors satisfying a so-called principle of definition, the Knuth-Bendix procedure can be used to prove that conjectures are inductive theorems of a given theory (proofs by inductive completion). In this paper, we show that this is the case even when the procedure is restricted in a linear selecting manner: first, critical pairs are generated in a linear manner by superposition of one equation of the initial theory into one equation issued from critical pairs (no superposition between two equations both issued from critical pairs); second, for each critical pair, the occurrence of superposition with theory equations is uniquely determined by a selection function. p Unlike the Knuth-Bendix procedure, our procedure, when terminating with success, does not produce a confluent system in general. However, the generated system is guaranteed to have the ground-confluence property (confluence for terms without variables). This result suffices to guarantee the conjecture validity. Our restricted completion procedure terminates in many cases where the inductive completion procedure loops, generating infinitely many critical pairs. The procedure applies to theories without constructors (Jouannaud & Kounalis, Proc. Symp. on Logic in Computer Science, Cambridge, MA, 1986, pp. 358-366) and extends to conditional theories and conditional conjectures. It can also incorporate various techniques used in classical induction. The procedure then combines the efficiency of classical induction method with the simplicity of inductive completion.

These lecture notes survey some joint work with Samson Abramsky as it was presented by me at Mathematical Foundations of Programming Semantics XXI in Birmingham (2005).2 It concerns a categorical semantics for quantum mechanics introduced in [Abramsky, S. and Coecke, B. (2004) A categorical semantics of quantum protocols. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LiCS'04), IEEE Computer Science Press. An extended & improved version is available at http://arXiv.org/quant-ph/0402130; Abramsky, S. and Coecke, B. (2005) Abstract physical traces. Theory and Applications of Categories 14, 111–124. Available at www.tac.mta.ca/tac/volumes/14/6/14-06abs.html]. We present this semantics with a particular focus on the connection between categorical diagrams and certain pictures involving typed squares, triangles, diamonds and lines. Along the way we unravel the structural components which come with strong compact closure. We provide pointers to related literature. Keywords: Strong compact closure, semantics, quantum mechanics, quantum logic, quantum informatics.

We present domain-theoretic models that support both probabilistic and nondeterministic choice. In [A. McIver and C. Morgan. Partial correctness for probablistic demonic programs. Theoretical Computer Science, 266:513–541, 2001], Morgan and McIver developed an ad hoc semantics for a simple imperative language with both probabilistic and nondeterministic choice operators over a discrete state space, using domain-theoretic tools. We present a model also using domain theory in the sense of D.S. Scott (see e.g. [G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. W. Mislove, and D. S. Scott. Continuous Lattices and Domains, volume 93 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge, 2003]), but built over quite general continuous domains instead of discrete state spaces.Our construction combines the well-known domains modelling nondeterminism – the lower, upper and convex powerdomains, with the probabilistic powerdomain of Jones and Plotkin [C. Jones and G. Plotkin. A probabilistic powerdomain of evaluations. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science, pages 186–195. IEEE Computer Society Press, 1989] modelling probabilistic choice. The results are variants of the upper, lower and convex powerdomains over the probabilistic powerdomain (see Chapter 4). In order to prove the desired universal equational properties of these combined powerdomains, we develop sandwich and separation theorems of Hahn-Banach type for Scott-continuous linear, sub- and superlinear functionals on continuous directed complete partially ordered cones, endowed with their Scott topologies, in analogy to the corresponding theorems for topological vector spaces in functional analysis (see Chapter 3). In the end, we show that our semantic domains work well for the language used by Morgan and McIver.

The procedure of Knuth & Bendix (In: Computational Problems in Abstract Algebras,Pergamon Press, 1970, pp. 263-297) completes a system of equations into a confluent one. It proceeds by adding critical pairs when equations superpose themselves in an ambiguous way. Huet & Hullot (Proc. 21st Symp. Foundations in Computer Science, 1980, pp 96-107) have shown that, for theories with constructors satisfying a so-called principle of definition, the Knuth-Bendix procedure can be used to prove that conjectures are inductive theorems of a given theory (proofs by inductive completion). In this paper, we show that this is the case even when the procedure is restricted in a linear selecting manner: first, critical pairs are generated in a linear manner by superposition of one equation of the initial theory into one equation issued from critical pairs (no superposition between two equations both issued from critical pairs); second, for each critical pair, the occurrence of superposition with theory equations is uniquely determined by a selection function. p Unlike the Knuth-Bendix procedure, our procedure, when terminating with success, does not produce a confluent system in general. However, the generated system is guaranteed to have the ground-confluence property (confluence for terms without variables). This result suffices to guarantee the conjecture validity. Our restricted completion procedure terminates in many cases where the inductive completion procedure loops, generating infinitely many critical pairs. The procedure applies to theories without constructors (Jouannaud & Kounalis, Proc. Symp. on Logic in Computer Science, Cambridge, MA, 1986, pp. 358-366) and extends to conditional theories and conditional conjectures. It can also incorporate various techniques used in classical induction. The procedure then combines the efficiency of classical induction method with the simplicity of inductive completion.

P. Kolaitis and M. Vardi (see Proc. 19th ACM Symp. on Theory of Computing, p.425-35 (1987), and Proc. 3rd Ann. Symp. on Logic in Computer Science, p.2-11 (1988)) proved that the 0-1 law holds for the second-order existential sentences whose first-order parts are formulas of Bernays-Schonfinkel or Ackermann prefix classes. They also provided several examples of second-order formulas for which the 0-1 law does not hold and noticed that the classification of second-order sentences for which the 0-1 law holds resembles the classification of decidable cases of prenex first-order sentences. The only cases they have not settled were the cases of Godel classes with and without equality. The authors confirm the conjecture of Kolaitis and Vardi that the 0-1 law does not hold for the existential second-order sentences whose first-order part is in the godel prenex form with equality. >

We study the cube of type assignment systems, as introduced in Giannini et al. (Fund. Inform. 19 (1993) 87–126), and confront it with Barendregt's typed gl-cube (Barendregt, in: Handbook of Logic in Computer Science, Vol. 2, Clarenden Press, Oxford, 1992). The first is obtained from the latter through applying a natural type erasing function E to derivation rules, that erases type information from terms. In particular, we address the question whether a judgement, derivable in a type assignment system, is always an erasure of a derivable judgement in a corresponding typed system; we show that this property holds only for systems without polymorphism. The type assignment systems we consider satisfy the properties ‘subject reduction’ and ‘strong normalization’. Moreover, we define a new type assignment cube that is isomorphic to the typed one.

Mathematical logic is a discipline used in sciences and humanities with different point of view. Although in tertiary level computer science education it has a solid place, it does not hold also for secondary level education. We present a heterogeneous study both theoretical based and empirically based which points out the key role of logic in computer science, computer science education and knowledge representation. We focus on the key contrast of semantics and syntax, the resolution principle as a leading inference technique (giving also interesting non-clausal generalization of the rule). Further we discuss the possibilities of inclusion the non-classical (many-valued) logics in education together with the original generalization of the non-clausal resolution rule into fuzzy logic. The last part describes partial results of the research concerning the secondary education in the Czech Republic especially in the mathematical logic field. The generalization of the presented ideas entails the article.

Role logic is a notation for describing properties of relational structures in shape analysis, databases and knowledge bases. A natural fragment of role logic corresponds to two-variable logic with counting and is therefore decidable.