Variable forgetting is a fundamental reasoning step for intelligent agents. It consists of dropping a proposition p from a theory, leaving everything else as close as possible to the way it was. This amounts to binding p with an existential (propositional) quantifier. In truth-functional logic it is trivial to emulate this effect without adding propositional quantifiers to the language. In certain modal logics, it is non-trivial but can still be done. For logics such as linear logic or relevant logic, which depart more radically from the classical paradigm, it has never been investigated. Let's try it and see what we get.
If variable forgetting can be defined syntactically in substructural logics, show how it is done. If it cannot, prove that it is impossible. Either way, advance the science of knowledge representation and reasoning.
Background in logic and in AI. COMP2620 and COMP3620 would be appropriate.
1. Fangzhen Lin and Ray Reiter, 'Forget it!', in Proceedings of the AAAI Symposium on Relevance, 1994: pp. 154-159. 2. Yan Zhang and Yi Zhu, 'Knowledge forgetting: Properties and applications', in Artificial Intelligence, Vol 173, 2009: pp. 1525-1537.
Knowledge of contemporary work in AI, specifically in KRR. Detailed knowledge of non-classical logic, specifically of substructural systems. Experience of research in formal theory relevant to computer science.