Formalizing and Compiling Background Knowledge and Its Applications to Knowledge Representation and Question Answering