UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Planning with effectively propositional logic

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 Green open access

[thumbnail of Navarro_Perez_mhg13.pdf]
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
Downloads since deposit
179Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item