Formal semantics is also called Montague Grammar, model-theoretic semantics, truth-conditional semantics, logical semantics, logical grammar, possible world semantics. (Fang, 2000; Jiang & Pan, 1998; Partee, 2011; Zou, 1995). Formal semantics adopts mathematical logic, including the syntax-semantics interface and the semantics-pragmatics interface, to study the semantics of natural languages. And it aims to help machines understand natural languages.