Professor Peter Jipsen (Chapman Univeristy, US) will give a seminar on Monday, 11th of January 2016 at 16:00 in the Aula Riunioni of the DipMat.
Title: Poset-product decompositions of ordered algebras and equational decidability.
Abstract: The poset-product of a family of ordered algebras is a common generalization of the ordinal sum and the cartesian product. In this talk we consider the question how to decompose ordered algebras into a poset-product of indecomposable components. For finite generalized basic logic algebras it is well known that every such algebra decomposes into a poset product of finite MV-algebras. We examine how this result extends to some infinite algebras, and how to check that an ordered algebra is poset-product indecomposable. We also discuss the dual notion of poset sum for the Kripke frames of (distributive) lattice-ordered structures.
For the case of basic logic algebras and finite poset-products of the standard MV-algebra, we give an algorithm for deciding if an equation in the language of residuated lattices holds in the algebra or not. The algorithm is implemented by a translation from residuated lattice terms to the language SMT-LIB2. This language is a standard interface for many Satisfiability Modulo Theory (SMT)-solvers, and we give a demo implementation that uses the solver CVC4.
