|
The project lies at the interface of algebra (ordered algebraic structures), logic and computer science, drawing on these fields symbiotically to develop mathematical tools for the design, comparison and evaluation of logic-based models of computation and information. As computer systems become ever more complex, it is essential to have tools to ensure that computer programs perform their intended tasks. Mathematical models based on logics play an important part in program specification and verification, and in analysing how computer systems operate. Explicitly, we might wish, e.g., to reason about statements true or false in given states of a computational system, and to make deductions about the system according to prescribed rules.In full generality, logic is the science of reasoning. A logic is simply a formal language endowed with axioms and/or rules for making deductions from given premisses. In classical propositional logic, we reason about statements which may be assigned values `true' or `false' and can be combined according to the everyday rules for `and', `or', and `not'. Alternatively, different logical rules may be postulated, additional truth values (such as `unknown') may be considered, and modal operators (`it is possible that', `it is necessary that', ...) may be introduced. Particular modal logics, such as epistemic logics (modelling state-of-knowledge), description logics (providing a formalism for knowledge representation), and temporal logics, have attracted much attention and so too have substructural logics, e.g. linear logics (which take into account resource limitations), and relevance logics (debarring deductions from irrelevant premisses).Logics can be studied either syntactically or semantically; for well-behaved ones the approaches are connected by soundness and completeness theorems. This project takes a semantic approach, whereby mathematical structures are used to model a given logic, and so to obtain snapshots of its properties. We propose to consider relational semantics, linking these to algebraic and coalgebraic semantics. With relational semantics, a logic is interpreted within the theory of relational structures. Such semantics are immensely useful in modal logic, where they yield a mathematically powerful language exactly formalising our intuitions about the possibility and necessity operators. In this restricted setting relational semantics have led to an understanding of the relative strengths of various axioms and to important results about decidability, complexity, and expressivity. One would like to have similar semantic models for a much wider range of logics, including substructural ones. We plan to exploit recently available methods based on canonical extensions to devise such semantics for certain logics which are algebraically modelled by lattices with additional operations. The central idea is to embed a given abstract algebra into a concrete algebra, of the same type but with stronger properties. Coalgebraic semantics have been intensively studied in recent years. Coalgebras generalise transition systems, a key notion in a state-based view of computation: each state of the system represents a computation at a given time instant, and relationships between states model the way the computation can proceed.To use these different semantics to full effect one must be able to move backwards and forwards between them. The project seeks to facilitate and to exploit such translations. A key mathematical strategy underpins this endeavour: the use of categorical equivalences and dual equivalences, which allow structures of one type to be analysed in terms of structures of another type. Examples of dual equivalences are that of Stone (for Boolean algebras) and of Priestley (for distributive lattices). Our algebraic and relational models, and algebraic and coalgebraic ones, are linked by dualities sitting on top of, or related to, these basic ones.
|