The discipline that today calls itself Artificial Intelligence traces its institutional founding to the 1956 Dartmouth conference, but its intellectual founding belongs to a question David Hilbert posed in 1928: is there an effective procedure that, given any well-formed statement, decides whether it is provable? Gödel and Turing answered, separately, that no such procedure exists for arithmetic in full — and, in answering it, founded the disciplines we now call computer science, mathematical logic, and artificial intelligence at once. From that point forward, the question of what it means for a machine to reason has been one question: what can we represent, what can we compute over that representation, and what can such computation be trusted to mean?
A half-century of work followed. Church and Turing settled what could be computed in principle. Kowalski and Colmerauer's Prolog was the revolutionary first move: a language in which one could, for the first time, answer the question of what rather than how — freed from the mechanics of an algorithm, focused instead on the specification it was intended to meet. Prolog opened the space of declarative thought, and with it the space of new questions. One of the deepest of those new questions concerned the meaning of Prolog's own primitives. What was the declarative content of negation-as-failure? This was the question Michael Gelfond and Vladimir Lifschitz answered with stable model semantics. In asking and answering it, they did more than advance the ball. They inaugurated a discipline: the move from operational specification to declarative semantics is the foundation on which knowledge representation, as a field, was built. Answer-set Prolog — the logical formalism and methodology — preceded answer-set programming, the computational paradigm, and it is from that formalism's principled treatment of defaults, exceptions, dynamics, and the messy realities of represented knowledge that the foundation the present AI conversation now reaches for has been quietly built.
Three Wrong Turns
The present conversation has converged on a diagnosis — that large language models lack what their proponents claimed for them — and has diverged on the remedy.
Three families of proposals now dominate. The first is the pure scaling bet — that capabilities sufficient for reasoning will emerge from sufficiently large models trained on sufficiently much text. The bet has not been wrong about everything; scaling has produced surface competence nobody predicted. What it has not produced, and what its advocates increasingly concede, is inference. Pattern matching, at any scale, does not become inference, and the largest models produce reasoning-shaped text; the gap between text shaped like reasoning and the structure of reasoning itself is the gap the discipline of knowledge representation has spent sixty years naming.
The second family is the most diagnostically perceptive. World models — internal representations of how things stand and how they change under action — are the named missing piece. Yann LeCun, the most visible advocate of this diagnosis, has proposed joint-embedding predictive architectures, energy-based models, and latent-state predictors — attempts to give a deep network something more like a world to consult than a distribution to sample from. The diagnosis is right; the prescription remains within the family of techniques that produced the wall. Probabilistic pattern matching is not representation, however sophisticated the architecture wrapped around it; a latent space whose semantics are read off post hoc, from probes, is not the same kind of object as a representation whose semantics are specified in advance and computable over.
The third family is the symbolic-leaning attempt — pairing large language models with an external scaffold of structured facts to consult and reason against. Knowledge-graph augmentation, GraphRAG, OWL- and RDF-backed reasoning over entity-and-relation triples: this is real work, and the work it does is real. Where pattern matching fails to keep facts straight, a knowledge graph can. The work is honest; the foundation is incomplete. World models are built not only of facts and relations but of defaults with weak exceptions; of non-monotonic conclusions that retract under new information; of action and change; of constraint and optimization; and of probabilistic and epistemic state. The implicit reading — that knowledge representation just is knowledge graphs — passes over the forty-year-old discipline that has been building precisely this machinery.
Each of these three reaches in a direction that misses the foundation the field has been overlooking — the one provided by the knowledge representation community.
Hidden in Plain Sight: The Discipline Already Here
What the field has been overlooking has been here all along. The discipline of knowledge representation — constituted by the move from operational specification to declarative semantics — has spent four decades building precisely the machinery a world model requires. Stable model semantics, Gelfond and Lifschitz's contribution to the semantics of logic programs, made possible a particular use of them: in answer-set Prolog, the program is the world model of a rational agent reasoning about a domain; its stable models are the possible worlds the agent considers operative; reasoning is how the agent navigates them. This is identity, not analogy.
From that methodological identity, the rest of the landscape follows. Action languages enable us to define world models involving reasoning about actions and change, with semantics specified in advance, for what becomes true when something is done. Defaults with their various exceptions encode the agent's standard expectations and the cases that override them. P-Log layers probabilistic uncertainty as a distribution over the possible worlds the program admits. Epistemic and multi-agent extensions name what one agent knows about what another knows. And answer-set solvers operationalize the edifice: real systems compute verifiable inference over models built in this language, at the speed real production work demands.
For sixty years the field has tried to render this kind of structured knowledge in something close to natural language — SHRDLU in the 1970s, Attempto Controlled English and Inform 7 in the decades that followed, and, most recently, the LLM-powered translators that map English specifications to Python or SQL on the assumption that surface and meaning can be aligned by enough examples. Each has reached for the same goal — letting domain experts express what they mean in their own idiom — and each has reached without the two things that would let it succeed: a foundation in which the expression could be grounded, and a methodology for using one. The discipline supplies both. The conversations have proceeded in parallel; the work that would complete them has been here throughout.
The methodology has existed for forty years. The era has finally produced demand for what the methodology supports.
Programming is Knowledge Representation
What the methodology supports is what programming itself has been carrying out in another vocabulary the whole time. Programming is knowledge representation in another guise. Not an analogy; not a use relation. Identity. Every line is a knowledge claim about what is to be true after the line runs; every type is a structural assertion about what kinds of things the program will handle; every test is a representation of expected behavior; every comment that explains why is a representation of the author's correctness argument. The conventional imperative-instruction view — programming as the giving of instructions to a machine — is the misreading. The instructions are the dressing; the knowledge they represent is the activity.
The move has been programming's own move, recognized by its most careful practitioners as what they were doing. John McCarthy designed LISP simultaneously as a programming language, a notation for the lambda calculus, and a representation language for artificial intelligence. Tony Hoare's calculus of preconditions and postconditions represents the change in knowledge a program effects. Edsger Dijkstra's derivation-from-specification practice treats the specification as a representation and the program as a derivation establishing it. Niklaus Wirth's typed declarations are representations of domain structure. Donald Knuth's literate programming is the program rendered as human knowledge for human understanding. The two activities have been one all along, asked in different vocabularies.
The category, named properly, is world model development. That is the discipline knowledge representation has been developing under that name and others since the 1960s, and it is also what programming, at its most disciplined, has been all along. The era's question — what an AI system should reason over and how — is the question of what a world model has been built. The credible player in the category is the one who names it, hands programmers and domain experts the tools to develop within it, and ships verifiable inference at the bottom.
Hybrid AI, Properly Constructed
None of what comes next requires putting large language models aside. The diagnosis is not that LLMs are the wrong tool, but that they are not the whole tool. Pattern matching is excellent at what pattern matching is for, and what it is unusually good at — as years of LLM development have established beyond reasonable dispute — is mapping natural language onto structured form. The work of taking a domain expert's careful sentences and rendering them as a structured representation suitable for compilation is exactly the work an LLM does best.
This places LLMs in the part of the pipeline they were meant for. The pipeline a world-model authoring system requires takes this shape: domain expert + large language model → KRML → answer-set programming / Flint & Steel → verifiable inference. Each tool does what it does best. The expert holds the domain knowledge to be represented. The LLM pattern-matches the expert's natural language into the structured form of KRML, the methodology's authoring surface. KRML compiles into answer-set programs that Flint & Steel and other solvers can compute over. The system at the bottom delivers verifiable inference — not text shaped like reasoning, but reasoning that can be checked against a world model whose terms are explicit. This is the practical form of the thought partners picture — agents that work alongside humans rather than replacing them.
The posture this implies is not oppositional. Flyover AI does not compete with the LLM ecosystem; it provides the layer the ecosystem needs to graduate from pattern matching to reasoning. The hybrid picture is positive-sum: the language models do what they do well, the methodology does what it does well, and the result is something neither could deliver alone. Flyover AI has built — and is building — exactly the parts of that pipeline the present moment has been missing.
What We Build
The first piece is KRML — a structured, naturalistic-English authoring surface for the methodology. KRML is the leap past the sixty-year history of English-as-medium attempts — SHRDLU through Attempto, Inform 7, the wider CNL-for-ASP family, and the LLM-powered NL-to-code translators of today, each a necessary first reach at the same problem. KRML speaks the agent's domain in the agent's own idiom and compiles, without loss in translation, into the methodology's formalism beneath. Where prior systems mapped English to a formalism, KRML maps English to a methodology — the Gelfond methodology, the structural primitives four decades of work have produced — and lets the methodology compile down to its formalism. Three intentionally aligned layers: methodology (Gelfond), surface (naturalistic English), foundation (answer-set programming today, Flint & Steel longer-term). A KRML excerpt — defaults, exceptions, and a counting constraint over a benefits policy — makes the difference visible:
"Employee" is a type. "Full-time-employee" is a type of employee. "Part-time-employee" is a type of employee. "Contractor" is a type of employee. "Benefits-package" is a type. An employee may be "health-insurance-eligible". An employee may be "enrolled" in a benefits-package. Normally, a full-time-employee X is health-insurance-eligible. A part-time-employee X is health-insurance-eligible if X's weekly-hours >= 30. Contractors cannot be health-insurance-eligible. A contractor X cannot be enrolled in more than 2 benefits-packages.
The text is read directly by domain experts and by the compiler. The Normally default, the conditional rule, the hard exception, and the more than 2 counting constraint are the methodological primitives the program reasons over — surfaced in the language the policy was already being written in. Counting constraints of that form are notoriously hard for language models to express precisely; KRML expresses them as natural English the compiler reads losslessly.
Flint & Steel is a high-performance, mission-critical answer-set programming platform — an alternative to existing answer-set solving stacks that addresses their limitations while building on the foundation the discipline has been developing for forty years. Flint & Steel is typed from the ground up and structured as a multi-frontend platform: a pipeline of typed intermediate representations with pluggable surface languages — KRML, clingo-compatible, SPARC, and others — shaped along the lines of modern compiler platforms such as LLVM and rustc. The platform is performance-engineered for the decision-making that real production work demands — finance, defense, regulated and mission-critical settings where both speed and verifiability matter. Formal verification, via Lean, sits on the longer-term trajectory: the implementation is structured to make that reach achievable, not aspirational. Where clingo is the C/ASM of the ASP world, Flint & Steel is its Rust — the same performance ceiling, a raised safety floor, type-driven dispatch instead of operational expertise, and modern engineering throughout.
KRML and Flint & Steel form a coherent stack for world model development — KRML at the authoring surface, Flint & Steel as the platform underneath, with additional frontends and targets joining as the ecosystem matures. The discipline gets the tooling it needs end-to-end.
Why Us, Why Now
The work continues a research line that has produced the discipline. Michael Gelfond and Vladimir Lifschitz published stable model semantics in 1988; the methodology built on it runs through four decades, including Gregory Gelfond's own research and that of Flyover AI. The research carries: a Ph.D. on multi-agent epistemic action languages (Arizona State, Baral lab, 2018); roughly sixteen peer-reviewed papers and one patent over 2005–2023; venues including AAAI, AAMAS, TPLP, Artificial Intelligence, and Springer LNCS — exactly the territory Flint & Steel now extends. The engineering discipline is demonstrated, not promised: the KRML prototype carries roughly 1,900 tests across 86,000 lines of Rust, a five-check pre-commit gate, complete architecture documentation, and board-governed design review. The bar is not the company saying it will be disciplined; the bar is the discipline already shipping.
The era has produced the demand. Large language models have surfaced what they cannot do, and the requirement for verifiable reasoning has moved from research goal to engineering need at exactly the time the methodology that supports it has reached production maturity. Forty years of foundation-building meet the era's question; the question and the answer converge for the first time. The category is also unclaimed. The major answer-set toolchain is EU academic research infrastructure rather than a product company, and the wider knowledge-representation laboratories publish exceptional work without shipping production systems at scale. The LLM labs build at the pattern-matching layer of the stack — the layer that complements the methodology, not the one that constitutes it. The window is open. Flyover AI is positioned to take it.
The foundation has been ready longer than the moment has been. The moment is here. The work of making world model development a discipline that programmers and domain experts can practice — in their own idiom, with formal semantics underneath, with verifiable inference at the bottom — is the work we have set out to do. The discipline does not, in the end, ask anything more of machines than what its founders asked: that what we represent, we be able to compute, and that what we compute, we be able to trust.