Abductive reasoning is a form of logical inference which seeks to uncover all possible causes of an observation. We show how abduction has a computational counterpart, like many other proof-theoretic concepts: namely the identification and modification of certain constants in a term. Abductive computation can be used to improve the behaviour of a term in some programmer-defined sense, like a typical workflow of optimisation problems including some machine-learning tasks. The emphasis of this progress report is a type system for abductive computation. It is intended to guarantee observably deterministic behaviour of programs, even though abduction may introduce a degree of computational nondeterminism.
Thu 7 Sep
|14:00 - 14:25|
|14:25 - 14:50|
|14:50 - 15:15|
Koko MuroyaUniversity of Birmingham, UK