The Great Computational Intelligence (GCI) project, funded by the Air Force Office of Scientific Research, aims to develop powerful computational systems and demonstrate their capability to solve complex problems in a wide variety of domains. Thus far in the project, this has included the development of the Deontic Cognitive Event Calculus (DCEC*), several automated theorem provers including ShadowProver, and Analogico-Deductive Reasoning. These tools and techniques have been used to create models of Nuclear Deterrence, produce a computer-generated, complete, and verifiably correct proof of Gödel’s first incompleteness theorem from first principles, and model the reasoning done by children on Piagetian tasks.

Current research goals of the project include producing computer-generated proofs of the Gödel-Rosser Theorem and Gödel’s speed-up theorem, as well as further developing our tools and techniques in order to accomplish these tasks.