August 30, 2012
In a seminal paper in 1997 Lin and Reiter introduced the notion of progression for basic action theories in the situation calculus. The idea is to replace the initial knowledge base by a new set of sentences which reflect the changes due to an action. Their definition has the intended properties with respect to reasoning about action but comes with a strong negative result, namely that for certain kinds of action theories first-order logic is not expressive enough to correctly characterize this form of progression, and second-order axioms are necessary. However, Lin and Reiter also considered an alternative definition for progression which is always first-order definable. They conjectured that this alternative definition is incorrect in the sense that the progressed theory is too weak and may sometimes lose information. This conjecture, and the status of first-order definable progression, has remained open since then. In this talk I will present four major results. The first result justifies that second-order logic is necessary by providing a proof for Lin and Reiter’s conjecture. The other three results show that under practical conditions first-order logic is strong enough to characterize progression. Finally, for the last part of the talk I will focus on the practical aspect of these results and discuss a possible application in video games.
Talk slides in pdf [~0,9MB]http://www.iit.demokritos.gr/docs/seminars/iptseminars-2010-06-vassos.pdf