The Edinburgh Laboratory for Integrated Artificial Intelligence (ELIAI) will fund a new project on integrating theorem proving and neural learning led by Jacques Fleuriot in collaboration with Ram Ramamoorthy. The 2-year project will involve the development of theorem-proving framework that allows for formal representation and proofs, and then faithful code-generation, of user-specified, spatio-temporal constraints that can then be used for learning in scenarios involving human-robot interaction