next up previous
Next: TRAVELING AND COMMERCE Up: APPENDIX Previous: APPENDIX

BLOCKSWORLD

Our blocks world has 4 sorts, situations s, blocks b, locations l and actions a. These are all disjoint.

We have a situation constant S0, other situation constant Sn and Sn' for various n's, a set of block constants tex2html_wrap_inline1170 , where tex2html_wrap_inline1172 and one block location constant Table. We also have constants tex2html_wrap_inline1176 , tex2html_wrap_inline1178 and tex2html_wrap_inline1180 .

All blocks are unique, but we do not postulate domain closure.

displaymath1138

We have block locationsgif, which are the Top of a block, or are the Table.

displaymath1139

All distinct block location terms denote distinct locations.

displaymath1140

displaymath1141

We have a function from actions and situations to situations, tex2html_wrap_inline695 , and a function from blocks and locations to actions, tex2html_wrap_inline1190 , which gives the action where block b is moved to location l.

All distinct action terms are distinct.

displaymath1142

We have the foundational axioms for situation calculus we considered earlier.

We have fluents, tex2html_wrap_inline1196 which states that b is on location l in situation s, and tex2html_wrap_inline1204 . tex2html_wrap_inline1204 is fully defined in terms of On.

displaymath1143

We now add the obvious definition of Changes for Move(b,l) actions. That is, there is a change in On(b,l') and On(b,l) when tex2html_wrap_inline1218 contains On(b,l') for an l' not equal to l, and tex2html_wrap_inline1226 , and tex2html_wrap_inline1228 contains Clear(l) and Clear(top(b)).

displaymath1144

This concludes the axiomatization of blocksworld, we could add domain constraints, but this is not necessary for the reasoning we do in this paper. We now present an axiomatization of traveling, followed by an axiomatization of buying selling and sending and receiving.



John McCarthy
Thu Jul 8 18:10:07 PDT 1999