---
title: "On Progression and Query Evaluation in First-Order Knowledge Bases with Function Symbols"
authors:
  - "Vaishak Belle"
  - "Gerhard Lakemeyer"
doi: "10.5591/978-1-57735-516-8/IJCAI11-131"
url: "https://ijcai.org/proceedings/2011/131"
pdf: "https://ijcai.org/proceedings/2011/0131.pdf"
venue: "Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence"
year: 2011
pages: "744-748"
track: ""
keywords:
---

# On Progression and Query Evaluation in First-Order Knowledge Bases with Function Symbols

Vaishak Belle, Gerhard Lakemeyer

*Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence*, pages 744-748. DOI: [10.5591/978-1-57735-516-8/IJCAI11-131](https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-131)

## Abstract

In a seminal paper, Lin and Reiter introduced the notion of progression of basic action theories. Unfortunately, progression is second-order in general. Recently, Liu and Lakemeyer improve on earlier results and show that for the local-effect and normal actions case, progression is computable but may lead to an exponential blow-up. Nevertheless, they show that for certain kinds of expressive first-order knowledge bases with disjunctive information, called proper+, it is efficient. However, answering queries about the resulting state is still undecidable. In this paper, we continue this line of research and extend proper+ to include functions. We prove that their progression wrt local-effect, normal actions, and range-restricted theories, is first-order definable and efficiently computable. We then provide a new logically sound and complete decision procedure for certain kinds of queries.