Reasoning about Unreliable Actions
Logic
2012-05-04 v2 Artificial Intelligence
Category Theory
Abstract
We analyse the philosopher Davidson's semantics of actions, using a strongly typed logic with contexts given by sets of partial equations between the outcomes of actions. This provides a perspicuous and elegant treatment of reasoning about action, analogous to Reiter's work on artificial intelligence. We define a sequent calculus for this logic, prove cut elimination, and give a semantics based on fibrations over partial cartesian categories: we give a structure theory for such fibrations. The existence of lax comma objects is necessary for the proof of cut elimination, and we give conditions on the domain fibration of a partial cartesian category for such comma objects to exist.
Keywords
Cite
@article{arxiv.1202.0255,
title = {Reasoning about Unreliable Actions},
author = {Graham White},
journal= {arXiv preprint arXiv:1202.0255},
year = {2012}
}