A Resolution Calculus for Dynamic Semantics
Christof Monz, Maarten de Rijke

Abstract:
This paper applies resolution theorem proving to natural language 
semantics.  The aim is to circumvent the computational complexity 
triggered by natural language ambiguities like pronoun binding, by 
interleaving pronoun binding with resolution deduction.  To this end, 
disambiguation is only applied to expressions that actually occur 
during derivations.  Given a set of premises and a conclusion, our 
resolution method only delivers pronoun bindings that are needed to 
derive the conclusion.