Output details
11 - Computer Science and Informatics
Queen Mary University of London
Algebra, Proof Theory and Applications for an Intuitionistic Logic of
Propositions, Actions and Adjoint Modal Operators
<11>A two-sorted modal logic and a sound, complete, cut-free proof system are developed, implemented in Haskell, and applied to reason about belief update, e.g. in robot navigation. This is the first cut-free proof system for such a family of logics. It led to the EPSRC project EP/J012564/1, worth £636,718, awarded on June 2012, with 3 postdocs and BAE-Systems (Clive.Downes@baesystems.com) as main industrial sponsor. The logic will be used to develop decision procedures to automatically verify the operating systems of Unmanned Aerial Vehicles. A group in Naval Research Laboratory (Washington, ramesh@itd.nrl.navy.mil) is working on the implementation of the logic.
