Theory Construction in Computational Logic