In Church's secret introduction  of his system of pure relevant implication, propositional quantifiers played a key role. (They did not do so in his more accessible .) Anderson, Belnap and Dunn in [3, 4] also invoke such quantifiers to define various logical particles, while the present author has had a go in [5, 6, 7] at similar explorations. What all this (and related) work comes to is that propositional quantifiers are enormously powerful in cooking up some otherwise independent relevant connectives and constants in systems of relevant implication. Here we review some of the more spectacular definitional schemes, dividing them into two classes: (A) Definitions that supply ALL of the expected properties of a relevant connective. (Example: the definition of fusion o using , , which goes back to .) (B) Definitions that require further axioms to get the relevantly expected properties of a particle. (Example: the definition of disjunction using , ,, which delivers the lattice properties of from those of , but which falls short of the distributive lattice properties that  imposes on R. On the other hand, if we are content to stop at the system LR of , the definition of is fully adequate.) We indicate a large supply of candidate definitions of particles under both headings, not only for R but for the related linear logic LL of Girard . And we supply, in addition to a number of particular definitions, two powerful definitional schemes, an intensional (or multiplicative) one useful for defining particles like DeMorgan ; and an extensional (or additive) scheme that produces the corresponding Boolean .
 Church, A., The weak theory of implication, in A. Menne, A. Wilhelmy and H. Angsel, eds., ``Kontrolliertes Denken, Untersuchungen zum Logikkalkül und zur Logik der Einzelwissenschaften'', Munich (Kommissions-Verlag Karl Alber), 1951, pp. 22-37.
 Church, A., The weak positive implicational propositional calculus (abstract), The Journal of Symbolic Logic 16 (1951), p. 238.
 Anderson, A. R., and N. D. Belnap, Jr., Enthymemes, The Journal of Philosophy 58 (1961), pp. 713-723.
 Anderson, A. R., N. D. Belnap, Jr. and J. M. Dunn, ``Entailment: The Logic of Relevance and Necessity, Vol. II,'' Princeton (Princeton University Press), 1992.
 Meyer, R. K., Intuitionism, entailment, negation, in H. Leblanc, ed., ``Truth, Syntax and Modality,'' Proceedings of the Temple University conference on alternative semantics, Amsterdam (North-Holland Publishing Company), 1973, pp. 168-198.
 Meyer, R. K., Definition in relevant propositional theories, unpublished typescript, Canberra, 1978.
 Meyer, R. K., Improved decision procedures for pure relevant logics, in C. A. Anderson and M. Zeleny, eds., "Logic, Meaning and Computation, Essays in Memory of Alonzo Church," 2001 (Kluwer), pp. 191-217.
 Thistlewaite, P. B., M. A. McRobbie and R. K. Meyer, ``Automated Theorem-Proving in Non-Classical Logics,'' Research notes in theoretical computer science, London (Pitman) and New York (John Wiley & Sons), 1988.
 Girard, J-Y., Linear logic, Theoretical Computer Science 50 (1987), pp. 1-102.
The logic BCI is usually defined as a Hilbert system with the following axioms
We call the formula satisfying the conditions of Lemma 1 a split formula. Using these we analyse possible proofs of a sequent for an arbitrary , always arriving at a contradiction. Someone with a taste for paradox might call this a constructive nonexistence proof. Thus, we show
 L. Humberstone, Variations on a theme of Curry, Notre Dame Journal of Formal Logic 47 (2006), 101-131.
 S. Butchard, T. Kowalski, A note on monothetic BCI, Notre Dame Journal of Formal Logic, 47 (2006), 541-544.
This talk will introduce a model of computation called event structures, in which a process is represented by its events, their causal dependency and conflict. It will motivate and outline very recent work on event structures with symmetry, and sketch applications to the semantics of higher order processes, nondeterministic dataflow and the unfolding of Petri nets.
I will compare the expressiveness of several models of concurrency that could be thought of as formalisations of higher dimensional automata: cubical sets, presheaves over a category of bipointed sets, automata with a predicate on hypercube-shaped subgraphs, labelled step transition systems, and higher dimensional transition systems. A series of counterexamples will illustrate the limitations of each of these models. Additionally I recall a few results relating higher dimensional automata to ordinary automata, Petri nets, and various kinds of event structures.
We present a new slant on canonical extensions of distributive-lattice-based algebras by linking them with Boolean topological algebras. This leads to very natural interpretations of the abstract conditions that characterise the canonical extension of a distributive lattice and yields new insights. For example, it allows us to show in a natural way that the variety generated by a finite distributive-lattice-based algebra is closed under forming canonical extensions. We shall illustrate our approach by giving a simple conceptual proof of the fact that the profinite completion and the canonical extension of a distributive lattice coincide.
In this talk I will review the definition of MALL proof net of Dominic Hughes and myself, and compare it with Girard's proof nets. I will discuss a couple of alternatives to deal with cut, and state precisely how proof nets capture proofs modulo inessential rule commutations.
The algebraic properties of the set of all binary relations on a set have been heavily investigated in the context of universal algebra, algebraic logic and their application in theoretical computer science.
In comparison, the study of partial maps is far less developed. This can be at least partly attributed to the failure of the set of partial maps on a set to be closed under many of the basic operations typically considered for binary relations: composition and intersection survive, but (for example) complementation and union do not.
A closer inspection reveals that partial maps are closed under a surprising number of quite expressive operations, and suggests some possible "Master Objects" for the algebraic study of partial maps and their application. We give an introductory survey of some of the existing approaches and present a recent (finite, and equational) characterisation of one of the Master Objects. If time (and expertise!) permit, we will discuss the potential of these approaches to emulate some of the typical applications of algebras of binary relations, and to offer some possible connections between category theory and semigroup theory.
A graph is a set of vertices
together with a binary
relation corresponding to the set of edges. In this language, many
familiar classes of graphs can be described by sets of first-order
sentences, and in particular by quasi-identities and universal
Horn sentences. For example, the class of simple graphs (i.e.
those whose edge relation is anti-reflexive and symmetric) is the
class of graphs satisfying
The unavoidable words problem is concerned with repetition in strings of symbols. There are two main ways to identify a word as unavoidable, one based on generalised pattern matching and one from an algorithm. Both methods are in NP, but do not appear to be in P. We define the simple unavoidable words as a subset of the standard unavoidable words that can be identified by the algorithm in P time. We define depth separating homomorphisms as an easy way to generate a subset of the unavoidable words using the pattern matching method. We then show that the two simpler problems are equivalent to each other.
In this talk, we introduce a simplicial approach to the theory of weak -categories which directly generalises Kan's classical homotopy theory of simplicial sets, Joyal's theory of quasi-categories and the algebraic theory of strict -categories. In keeping with the theme of this workshop, we also examine how this theory of weak complicial sets might be applied to gaining a better understanding of the directed algebraic topology of concurrent processes and re-writing systems.
The coherence problem for an added structure on a category roughly asks "What diagrams commute purely in virtue of the extra structure?". This problem is related to, amongst others, the proof theory of substructural logics and the semantics of concurrent programs. Inspired by work of Kelly on abstract coherence properties, we show how to use term rewriting techniques to efficiently solve several variants of the coherence problem. We then apply this machinery to obtain a new proof of coherence for iterated monoidal categories and interpret this result in terms of compositions of processes in higher dimensional automata.
Clones of -valued logic functions, i.e., composition closed classes of operations on a -element universe that include all projections, form an algebraic and dually algebraic lattice. An element of such lattice is called join- (meet-) irreducible if it cannot be expressed as a join (meet) of other clones, in the usual meaning of these two lattice operations. Such irreducible elements are important since they can serve as generators of the lattice. We present some major results obtained during the past decade or so, which include existence of countable chains of such elements and general criteria for both types of irreducible clones. We also answer some particular questions regarding the irreducible elements located in the `lower part' of the lattice, such as minimal and monoidal clones.