Unification is originally a technique to make two expressions identical by substituting their variables with other expressions. Unification in an equational theory (E-unification) is a unification where two expressions are made to be equal in that equational theory by a suitable substitution. Here we consider E-unification in modal logics, especially in normal modal logics with weak transitivity axioms. In this talk, we first review some basic notions in E-unification, most general unifier, unification type, and the relation between discriminator and m.g.u. Then we discuss the connection of the classification of unification type and splitting of the lattice of normal modal logics over some weakly transitive logics. This is a part of joint work with Prof. Wojciech Dzik in Katowice last September.
Epsilion calculus is one of the most important proof theoretic concepts but epsilon calculus is usually associated with classical logic. In this lecture we investigate natural extensions to nonclassical logics. These extensions are usually conservative wrt the propositional fragments but allow for the derivability of all classically valid quantifier shift laws. As consequence we show, that finitely valued first order Gödel logics are exactly the intermediary logics validitating the first epsilon theorem. In addition, the second epsilon theorem does also hold.
Associate Professor
School of Computer Science and Engineering
The University of New South Wales
Sydney NSW 2052 Australia
2012-03-15 15:00-17:00
Seminar room of the RCIS, 3. floor
We present a higher-order functional language in which variables define arbitrary-dimensional entities, where any atomic value may be used as a dimension, and a multidimensional runtime context is used to index the variables. We give an intuitive presentation of the language, present the denotational semantics, and demonstrate how function applications over these potentially infinite data structures can be transformed into manipulations of the runtime context. There are two kinds of functional abstraction and application: call-by-value (eager evaluation) is used to pass dimensions and constants, while call-by-name (lazy evaluation) is used for passing multidimensional variables.
The multidimensional space can be used for both programming and implementation purposes. At the programming level, the informal presentation of the language gives many examples showing the utility of describing common computing entities as infinite multidimensional data structures.
At the implementation level, the main technical part of the talk demonstrates that the higher-order functions over infinite data structures - even ones that are currieed - can be statically transformed into equivalent functions directly manipulating the context, thereby avoiding the need for closures over parts of the environment.
