In artificial intelligence, with implications for cognitive science, the frame problem describes an issue with using first-order logic to express facts about a robot in the world.
Representing the state of a robot with traditional first-order logic requires the use of many axioms that simply imply that things in the environment do not change arbitrarily.
In a first-order logic system, additional axioms are required to make inferences about the environment (for example, that a block cannot change position unless it is physically moved).
In this paper, and many that came after, the formal mathematical problem was a starting point for more general discussions of the difficulty of knowledge representation for artificial intelligence.
Issues such as how to provide rational default assumptions and what humans consider common sense in a virtual environment.
In the logical context, actions are typically specified by what they change, with the implicit assumption that everything else (the frame) remains unchanged.
A scenario with a door, which can be open or closed, and a light, which can be on or off, is statically represented by two propositions
While the three formulae above are a direct expression in logic of what is known, they do not suffice to correctly draw consequences.
[clarification needed] In other words, the problem is that of formalizing a dynamical domain without explicitly specifying the frame axioms.
Alternative solutions were then proposed, involving predicate completion, fluent occlusion, successor state axioms, etc.
By the end of the 1980s, the frame problem as defined by McCarthy and Hayes was solved[clarification needed].
In this article, only the expression in logic is shown, and only in the simplified language with no action names.
The rationale of this solution is to represent not only the value of conditions over time, but also whether they can be affected by the last executed action.
Occlusion can be viewed as “permission to change”: if a condition is occluded, it is relieved from obeying the constraint of inertia.
The rationale is that a condition can change value only if the corresponding occlusion predicate is true at the next time point.
In turn, the occlusion predicate is true only when an action affecting the condition is executed.
An action results in a change if and only if it makes true a condition that was previously false or vice versa.
The successor state axioms are used in the variant to the situation calculus proposed by Ray Reiter.
It solves the frame problem by using first-order logic terms, rather than predicates, to represent the states.
For example, the action of opening the door at time 0 is represented by the formula: The action of closing the door, which makes a condition false instead of true, is represented in a slightly different way: This formula works provided that suitable axioms are given about
For example: To solve a problem, such as which fluents hold at time 5?, it is necessary to pose the problem as a goal, such as: In this case, obtaining the unique solution: The event calculus solves the frame problem, eliminating undesired solutions, by using a non-monotonic logic, such as first-order logic with circumscription[3] or by treating the event calculus as a logic program using negation as failure.
Steve Hanks and Drew McDermott argued, on the basis of their Yale shooting example, that this solution to the frame problem is unsatisfactory.
Hudson Turner showed, however, that it works correctly in the presence of appropriate additional postulates.
The counterpart of the default logic solution in the language of answer set programming is a rule with strong negation: (if
Separation logic is a formalism for reasoning about computer programs using pre/post specifications of the form
Separation logic is an extension of Hoare logic oriented to reasoning about mutable data structures in computer memory and other dynamic resources, and it has a special connective *, pronounced "and separately", to support independent reasoning about disjoint memory regions.
[5][6] Separation logic employs a tight interpretation of pre/post specs, which say that the code can only access memory locations guaranteed to exist by the precondition.
[9] There appears to be some similarity between the separation logic solution to the frame problem and that of the fluent calculus mentioned above.
[further explanation needed] Action description languages elude the frame problem rather than solving it.
Typically, however, a translation is given from these languages to answer set programming rather than first-order logic.