Output details
11 - Computer Science and Informatics
Newcastle University
Revising basic theorem proving algorithms to cope with the logic of partial functions
<10> The Logic of Partial Functions (LPF) is a long-standing framework for reasoning about partial functions. Despite intense academic interest, LPF has had limited industrial take up due to the lack of automated reasoning tools. This paper provides a unique investigation into extending fundamental theorem proving techniques to LPF. An important range of novel new insights and results for automating LPF are presented. Crucially, the work has provided the basis for ongoing work on developing the effective automated tool support for LPF and has initiated a range of further work. The paper was invited to a special SCP issue.