Navarro-Pérez, JA;
Voronkov, A;
(2013)
Planning with effectively propositional logic.
In:
Programming Logics Essays in Memory of Harald Ganzinger.
(pp. 302 - 316).
Springer Berlin Heidelberg
![[thumbnail of Navarro_Perez_mhg13.pdf]](https://discovery.ucl.ac.uk/style/images/fileicons/application_pdf.png) Preview |
PDF
Navarro_Perez_mhg13.pdf Download (185kB) |
Abstract
We present a fragment of predicate logic which allows the use of equality and quantification but whose models are limited to finite Herbrand interpretations. Formulae in this logic can be thought as syntactic sugar on top of the Bernays-Schönfinkel fragment and can, therefore, still be effectively grounded into a propositional representation. We motivate the study of this logic by showing that practical problems from the area of planning can be naturally and succinctly represented using the added syntactic features. Moreover, from a theoretical point of view, we show that this logic allows, when compared to the propositional approach, not only more compact encodings but also exponentially shorter refutation proofs. © Springer-Verlag Berlin Heidelberg 2013.
| Type: | Proceedings paper |
|---|---|
| Title: | Planning with effectively propositional logic |
| ISBN: | 978-3-642-37650-4 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-642-37651-1_13 |
| Publisher version: | http://dx.doi.org/10.1007/978-3-642-37651-1_13 |
| Additional information: | This is the authors' accepted version of this published chapter. |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/1418747 |
Archive Staff Only
 |
View Item |
