AI Researcher, Cognitive Technologist Inventor - AI Thinking, Think Chain Innovator - AIOT, XAI, Autonomous Cars, IIOT Founder Fisheyebox Spatial Computing Savant, Transformative Leader, Industry X.0 Practitioner The detection of structures is based on a set of potential invariants that reflect the properties of the environment (space). An invariant is essentially a hypothesis that needs to be tested and confirmed or rejected. For the natural environment, the set of invariants reflects the properties of space-time and does not depend on the purpose of the system. A fixed set of invariants allows detecting previously unknown structures of arbitrary complexity. Detecting a previously unknown structure is essentially the construction of new concepts.

We describe the design and implementation of a reasoning engine that facilitates the gamification of loop-invariant discovery. Our reasoning engine enables students, computational agents and regular software engineers with no formal methods expertise to collaboratively prove interesting theorems about simple programs using browser-based, online games. Within an hour, players are able to specify and verify properties of programs that are beyond the capabilities of fully-automated tools. The hour limit includes the time for setting up the system, completing a short tutorial explaining game play and reasoning about simple imperative programs. Players are never required to understand formal proofs; they only provide insights by proposing invariants. The reasoning engine is responsible for managing and evaluating the proposed invariants, as well as generating actionable feedback.