The Stanford Formal Reasoning Group wants to do basic technical work and is therefore unsuited to be a full challenger in the sense of the BAA. Moreover, we don't have enough people.
However, we have ideas about the requirements an HPKB should meet, if it is to support viable planning, and would like to develop them further and make our present ideas and the new ones available to those formulating official challenges.
Some previous experience is relevant. We consider some large knowledge engineering projects, and detail problems that arose in these projects. Representing large amounts of knowledge in logical form is difficult. The examples given here focus on certain problems that arise, both of rigidity of representation, and of mis-placed emphasis. The talents that the Formal Reasoning Group brings to this endeavor are its familiarity with the nature of these problems, and its ability to quickly find incipient errors in the building of large knowledge based systems.