## Abstract

Automated theorem provers are often used in other tools as black-boxes for discharging proof obligations. One example where this has enjoyed a lot of success is within interactive theorem proving. A key usability factor in such settings is the time taken for the provers to complete. Automated theorem provers typically run lists of proof strategies sequentially, which can cause proofs to be found more slowly than necessary if the ordering is suboptimal. We show that it is possible to predict which strategies are likely to succeed while they are running using an artificial neural network. We also implement a run-time strategy scheduler in the Vampire prover which utilises a trained neural network to improve average proof search time, and hence increases usability as a black-box prover.

Original language | English |
---|---|

Pages (from-to) | 58-71 |

Number of pages | 14 |

Journal | CEUR Workshop Proceedings |

Volume | 2162 |

Publication status | Published - 1 Jan 2018 |

Event | 6th Workshop on Practical Aspects of Automated Reasoning, PAAR 2018 - Oxford, United Kingdom Duration: 19 Jul 2018 → … |