Abstract
It is a common approach when faced with a reasoning problem to translate that problem into first-order logic and utilise a first-order automated theorem prover (ATP). One of the reasons for this is that first-order ATPs have reached a good level of maturity after decades of development. However, not all translations are equal and in many cases the same problem can be translated in ways that either help or hinder the ATP. This paper looks at this activity from the perspective of a first-order ATP (mostly Vampire).
| Original language | English |
|---|---|
| Pages (from-to) | 11-25 |
| Number of pages | 15 |
| Journal | CEUR Workshop Proceedings |
| Volume | 2095 |
| Publication status | Published - 1 Jan 2018 |
| Event | 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics, ARQNL 2018 - Oxford, United Kingdom Duration: 18 Jul 2018 → … |