Part of the "Language, Proof and Logic" suite of instructional software for introductory logic courses. Lets you manipulate a blocks worlds and write sentences in first-order language, and evaluate their truth in the worlds.