Wolfgang Pauli Institute (WPI) Vienna

Home WPI in a nutshell Practical Information Events People WPI Projects
Login Thematic Programs Pauli Fellows Talks Research Groups

Kick-off Meeting for Project TICAMORE (external website )

Location: WPI, OMP 1, Seminar Room 08.135 Tue, 14. Mar - Thu, 16. Mar 17
Topics:
Translating and Discovering Calculi for Modal and Related Logics
Organiser(s)
Agata Ciabattoni (WPI c/o TU Wien)

Talks in the framework of this event


Brotherston James (University College London) WPI, OMP 1, Seminar Room 08.135 Tue, 14. Mar 17, 10:00
Biabduction (and Related Problems) in Array Separation Logic
I describe array separation logic (ASL), a variant of separation logic in which the data structures are either pointers or arrays. This logic can be used, e.g., to give memory safety proofs of imperative array programs. The key to automatically inferring specifications is the so-called "biabduction" problem, given formulas A and B, find formulas X and Y such that A + X |= B + Y (and such that A + X is also satisfiable), where + is the well-known "separating conjunction" of separation logic. We give an NP decision procedure for this problem that produces solutions of reasonable quality, and we also show that the problem of finding a consistent solution is NP-hard. Along the way, we study satisfiability and entailment in our logic, giving decision procedures and complexity bounds for both problems. This is joint work with Nikos Gorogiannis (Middlesex) and Max Kanovich (UCL).
  • Event: Kick-off Meeting for Project TICAMORE (2017)

Buszkowski Wojciech (Adam Mickiewicz University) WPI, OMP 1, Seminar Room 08.135 Wed, 15. Mar 17, 10:00
Some open problems in substructural logics
I will focus on several substructural logics, mainly conservative extensions of the Lambek calculus (associative and nonassociative, with and without constants) and point out some basic open problems. Examples: the lower bound of the complexity of the full nonassociative Lambek calculus, the decidability of Pratt's action logic, the decidability of the consequence relation for the nonassociative Lambek calculus with involutive negations, the decidability of the equational theory of lattice-ordered pregroups. I will briefly discuss what is known in these areas.
  • Event: Kick-off Meeting for Project TICAMORE (2017)

Impressum webmaster [Printable version]