2012/02/01 by Graham White, White, Graham
Computer Science · #18C50 #Advanced Algebra and Logic #Artificial Intelligence (cs.AI) #Category Theory (math.CT) #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1202.0255
openalex publication_date 2012/02/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.