Reasoning about Unreliable Actions
This work addresses foundational issues in logic and AI for philosophers and computer scientists, but it appears incremental as it builds on existing frameworks like Reiter's.
The paper tackles the problem of reasoning about unreliable actions by analyzing Davidson's semantics using a strongly typed logic with contexts of partial equations, analogous to Reiter's AI work. It defines a sequent calculus, proves cut elimination, and provides a semantics based on fibrations over partial cartesian categories, including a structure theory for such fibrations.
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.