It is possible (using formal semantics) to translate natural language sentences into lambda expressions. So, is it possible to translate those lambda expressions into some logic, e.g. into first-order logic or into modal logic?
I am aware of the Curry-Howard correspondence, but I have not found actual translation, it is more conceptual one. I am aware of translation of lambda expressions into Answer Set Programming http://costantini.di.univaq.it/pubbls/aspopc10-Costantini.pdf and I have heard about translations into combinatory logic.
But are there translations into first order or modal logic?
Such translation would be big step into natural language processing.