The situation calculus is a logic formalism designed for representing and reasoning about dynamical domains. It was first introduced by John McCarthy in 1963. [1] The main version of the situational calculus that is presented in this article is based on that introduced by Ray Reiter in 1991. It is followed by sections about McCarthy's 1986 version and a logic programming formulation.
The situation calculus represents changing scenarios as a set of first-order logic formulae. The basic elements of the calculus are:
A domain is formalized by a number of formulae, namely:
A simple robot world will be modeled as a running example. In this world there is a single robot and several inanimate objects. The world is laid out according to a grid so that locations can be specified in terms of coordinate points. It is possible for the robot to move around the world, and to pick up and drop items. Some items may be too heavy for the robot to pick up, or fragile so that they break when they are dropped. The robot also has the ability to repair any broken items that it is holding.
The main elements of the situation calculus are the actions, fluents and the situations. A number of objects are also typically involved in the description of the world. The situation calculus is based on a sorted domain with three sorts: actions, situations, and objects, where the objects include everything that is not an action or a situation. Variables of each sort can be used. While actions, situations, and objects are elements of the domain, the fluents are modeled as either predicates or functions.
The actions form a sort of the domain. Variables of sort action can be used and also functions whose result is of sort action. Actions can be quantified. In the example robot world, possible action terms would be to model the robot moving to a new location , and to model the robot picking up an object o. A special predicate Poss is used to indicate when an action is executable.
In the situation calculus, a dynamic world is modeled as progressing through a series of situations as a result of various actions being performed within the world. A situation represents a history of action occurrences. In the Reiter version of the situation calculus described here, a situation does not represent a state, contrarily to the literal meaning of the term and contrarily to the original definition by McCarthy and Hayes. This point has been summarized by Reiter as follows:
The situation before any actions have been performed is typically denoted and called the initial situation. The new situation resulting from the performance of an action is denoted using the function symbol do (Some other references [3] also use result). This function symbol has a situation and an action as arguments, and a situation as a result, the latter being the situation that results from performing the given action in the given situation.
The fact that situations are sequences of actions and not states is enforced by an axiom stating that is equal to if and only if and . This condition makes no sense if situations were states, as two different actions executed in two different states can result in the same state.
In the example robot world, if the robot's first action is to move to location , the first action is and the resulting situation is . If its next action is to pick up the ball, the resulting situation is . Situations terms like and denote the sequences of executed actions, and not the description of the state that result from execution.
Statements whose truth value may change are modeled by relational fluents, predicates that take a situation as their final argument. Also possible are functional fluents, functions that take a situation as their final argument and return a situation-dependent value. Fluents may be thought of as "properties of the world"'.
In the example, the fluent can be used to indicate that the robot is carrying a particular object in a particular situation. If the robot initially carries nothing, is false while is true. The location of the robot can be modeled using a functional fluent that returns the location of the robot in a particular situation.
The description of a dynamic world is encoded in second-order logic using three kinds of formulae: formulae about actions (preconditions and effects), formulae about the state of the world, and foundational axioms.
Some actions may not be executable in a given situation. For example, it is impossible to put down an object unless one is in fact carrying it. The restrictions on the performance of actions are modeled by literals of the form , where a is an action, s a situation, and Poss is a special binary predicate denoting executability of actions. In the example, the condition that dropping an object is only possible when one is carrying it is modeled by:
As a more complex example, the following models that the robot can carry only one object at a time, and that some objects are too heavy for the robot to lift (indicated by the predicate heavy):
Given that an action is possible in a situation, one must specify the effects of that action on the fluents. This is done by the effect axioms. For example, the fact that picking up an object causes the robot to be carrying it can be modeled as:
It is also possible to specify conditional effects, which are effects that depend on the current state. The following models that some objects are fragile (indicated by the predicate fragile) and dropping them causes them to be broken (indicated by the fluent broken):
While this formula correctly describes the effect of the actions, it is not sufficient to correctly describe the action in logic, because of the frame problem.
While the above formulae seem suitable for reasoning about the effects of actions, they have a critical weakness—they cannot be used to derive the non-effects of actions. For example, it is not possible to deduce that after picking up an object, the robot's location remains unchanged. This requires a so-called frame axiom, a formula like:
The need to specify frame axioms has long been recognised as a problem in axiomatizing dynamic worlds, and is known as the frame problem. As there are generally a very large number of such axioms, it is very easy for the designer to leave out a necessary frame axiom, or to forget to modify all appropriate axioms when a change to the world description is made.
The successor state axioms "solve" the frame problem in the situation calculus. According to this solution, the designer must enumerate as effect axioms all the ways in which the value of a particular fluent can be changed. The effect axioms affecting the value of fluent can be written in generalised form as a positive and a negative effect axiom:
The formula describes the conditions under which action a in situation s makes the fluent F become true in the successor situation . Likewise, describes the conditions under which performing action a in situation s makes fluent F false in the successor situation.
If this pair of axioms describe all the ways in which fluent F can change value, they can be rewritten as a single axiom:
In words, this formula states: "given that it is possible to perform action a in situation s, the fluent F would be true in the resulting situation if and only if performing a in s would make it true, or it is true in situation s and performing a in s would not make it false."
By way of example, the value of the fluent broken introduced above is given by the following successor state axiom:
The properties of the initial or any other situation can be specified by simply stating them as formulae. For example, a fact about the initial state is formalized by making assertions about (which is not a state, but a situation). The following statements model that initially, the robot carries nothing, is at location , and there are no broken objects:
The foundational axioms of the situation calculus formalize the idea that situations are histories by having . They also include other properties such as the second-order induction on situations.
Regression [4] is a mechanism for proving consequences in the situation calculus. [5] It is based on expressing a formula containing the situation in terms of a formula containing the action a and the situation s, but not the situation . By iterating this procedure, one can end up with an equivalent formula containing only the initial situation S0. Proving consequences is supposedly simpler from this formula than from the original one.
GOLOG is a logic programming language based on the situation calculus. [6] [7]
The main difference between the original situation calculus by McCarthy and Hayes and the one in use today is the interpretation of situations. In the modern version of the situational calculus, a situation is a sequence of actions. Originally, situations were defined as "the complete state of the universe at an instant of time". It was clear from the beginning that such situations could not be completely described; the idea was simply to give some statements about situations, and derive consequences from them. This is also different from the approach that is taken by the fluent calculus, where a state can be a collection of known facts, that is, a possibly incomplete description of the universe.
In the original version of the situation calculus, fluents are not reified. In other words, conditions that can change are represented by predicates and not by functions. Actually, McCarthy and Hayes defined a fluent as a function that depends on the situation, but they then proceeded always using predicates to represent fluents. For example, the fact that it is raining at place x in the situation s is represented by the literal . In the 1986 version of the situation calculus by McCarthy, functional fluents are used. For example, the position of an object x in the situation s is represented by the value of , where location is a function. Statements about such functions can be given using equality: means that the location of the object x is the same in the two situations s and .
The execution of actions is represented by the function result: the execution of the action a in the situation s is the situation . The effects of actions are expressed by formulae relating fluents in situation s and fluents in situations . For example, that the action of opening the door results in the door being open if not locked is represented by:
The predicates locked and open represent the conditions of a door being locked and open, respectively. Since these conditions may vary, they are represented by predicates with a situation argument. The formula says that if the door is not locked in a situation, then the door is open after executing the action of opening, this action being represented by the constant opens.
These formulae are not sufficient to derive everything that is considered plausible. Indeed, fluents at different situations are only related if they are preconditions and effects of actions; if a fluent is not affected by an action, there is no way to deduce it did not change. For example, the formula above does not imply that follows from , which is what one would expect (the door is not made locked by opening it). In order for inertia to hold, formulae called frame axioms are needed. These formulae specify all non-effects of actions:
In the original formulation of the situation calculus, the initial situation, later denoted by , is not explicitly identified. The initial situation is not needed if situations are taken to be descriptions of the world. For example, to represent the scenario in which the door was closed but not locked and the action of opening it is performed is formalized by taking a constant s to mean the initial situation and making statements about it (e.g., ). That the door is open after the change is reflected by formula being entailed. The initial situation is instead necessary if, like in the modern situation calculus, a situation is taken to be a history of actions, as the initial situation represents the empty sequence of actions.
The version of the situation calculus introduced by McCarthy in 1986 differs to the original one by the use of functional fluents (e.g., is a term representing the position of x in the situation s) and for an attempt to use circumscription to replace the frame axioms.
It is also possible (e.g. Kowalski 1979, Apt and Bezem 1990, Shanahan 1997) to write the situation calculus as a logic program:
Here Holds is a meta-predicate and the variable f ranges over fluents. The predicates Poss, Initiates and Terminates correspond to the predicates Poss, , and respectively. The left arrow ← is half of the equivalence ↔. The other half is implicit in the completion of the program, in which negation is interpreted as negation as failure. Induction axioms are also implicit, and are needed only to prove program properties. Backward reasoning as in SLD resolution, which is the usual mechanism used to execute logic programs, implements regression implicitly.
First-order logic—also called predicate logic, predicate calculus, quantificational logic—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.
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. For example, Hayes describes a "block world" with rules about stacking blocks together. In a first-order logic system, additional axioms are required to make inferences about the environment. The frame problem is the problem of finding adequate collections of axioms for a viable description of a robot environment.
The proof of Gödel's completeness theorem given by Kurt Gödel in his doctoral dissertation of 1929 is not easy to read today; it uses concepts and formalisms that are no longer used and terminology that is often obscure. The version given below attempts to represent all the steps in the proof and all the important ideas faithfully, while restating the proof in the modern language of mathematical logic. This outline should not be considered a rigorous proof of the theorem.
In many popular versions of axiomatic set theory, the axiom schema of specification, also known as the axiom schema of separation, subset axiom or axiom schema of restricted comprehension is an axiom schema. Essentially, it says that any definable subclass of a set is a set.
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems of intuitionistic logic do not assume the law of the excluded middle and double negation elimination, which are fundamental inference rules in classical logic.
Hoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician Tony Hoare, and subsequently refined by Hoare and other researchers. The original ideas were seeded by the work of Robert W. Floyd, who had published a similar system for flowcharts.
In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology instead of an unconditional tautology. Each conditional tautology is inferred from other conditional tautologies on earlier lines in a formal argument according to rules and procedures of inference, giving a better approximation to the natural style of deduction used by mathematicians than to David Hilbert's earlier style of formal logic, in which every line was an unconditional tautology. More subtle distinctions may exist; for example, propositions may implicitly depend upon non-logical axioms. In that case, sequents signify conditional theorems in a first-order language rather than conditional tautologies.
In mathematics, an affine space is a geometric structure that generalizes some of the properties of Euclidean spaces in such a way that these are independent of the concepts of distance and measure of angles, keeping only the properties related to parallelism and ratio of lengths for parallel line segments. Affine space is the setting for affine geometry.
In proof theory, the semantic tableau, also called an analytic tableau, truth tree, or simply tree, is a decision procedure for sentential and related logics, and a proof procedure for formulae of first-order logic. An analytic tableau is a tree structure computed for a logical formula, having at each node a subformula of the original formula to be proved or refuted. Computation constructs this tree and uses it to prove or refute the whole formula. The tableau method can also determine the satisfiability of finite sets of formulas of various logics. It is the most popular proof procedure for modal logics.
The Kripke–Platek set theory with urelements (KPU) is an axiom system for set theory with urelements, based on the traditional (urelement-free) Kripke–Platek set theory. It is considerably weaker than the (relatively) familiar system ZFU. The purpose of allowing urelements is to allow large or high-complexity objects to be included in the theory's transitive models without disrupting the usual well-ordering and recursion-theoretic properties of the constructible universe; KP is so weak that this is hard to do by traditional means.
In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.
Circumscription is a non-monotonic logic created by John McCarthy to formalize the common sense assumption that things are as expected unless otherwise specified. Circumscription was later used by McCarthy in an attempt to solve the frame problem. To implement circumscription in its initial formulation, McCarthy augmented first-order logic to allow the minimization of the extension of some predicates, where the extension of a predicate is the set of tuples of values the predicate is true on. This minimization is similar to the closed-world assumption that what is not known to be true is false.
In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation-complete theorem-proving technique for sentences in propositional logic and first-order logic. For propositional logic, systematically applying the resolution rule acts as a decision procedure for formula unsatisfiability, solving the Boolean satisfiability problem. For first-order logic, resolution can be used as the basis for a semi-algorithm for the unsatisfiability problem of first-order logic, providing a more practical method than one following from Gödel's completeness theorem.
The Yale shooting problem is a conundrum or scenario in formal situational logic on which early logical solutions to the frame problem fail. The name of this problem comes from a scenario proposed by its inventors, Steve Hanks and Drew McDermott, working at Yale University when they proposed it. In this scenario, Fred is initially alive and a gun is initially unloaded. Loading the gun, waiting for a moment, and then shooting the gun at Fred is expected to kill Fred. However, if inertia is formalized in logic by minimizing the changes in this situation, then it cannot be uniquely proved that Fred is dead after loading, waiting, and shooting. In one solution, Fred indeed dies; in another solution, the gun becomes mysteriously unloaded and Fred survives.
In artificial intelligence, a fluent is a condition that can change over time. In logical approaches to reasoning about actions, fluents can be represented in first-order logic by predicates having an argument that depends on time. For example, the condition "the box is on the table", if it can change over time, cannot be represented by ; a third argument is necessary to the predicate to specify the time: means that the box is on the table at time . This representation of fluents is modified in the situation calculus by using the sequence of the past actions in place of the current time.
The event calculus is a logical theory for representing and reasoning about events and about the way in which they change the state of some real or artificial world. It deals both with action events, which are performed by agents, and with external events, which are outside the control of any agent.
The fluent calculus is a formalism for expressing dynamical domains in first-order logic. It is a variant of the situation calculus; the main difference is that situations are considered representations of states. A binary function symbol is used to concatenate the terms that represent facts that hold in a situation. For example, that the box is on the table in the situation is represented by the formula . The frame problem is solved by asserting that the situation after the execution of an action is identical to the one before but for the conditions changed by the action. For example, the action of moving the box from the table to the floor is formalized as:
Axiomatic constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with "" and "" of classical set theory is usually used, so this is not to be confused with a constructive types approach. On the other hand, some constructive theories are indeed motivated by their interpretability in type theories.
In logic, especially mathematical logic, an axiomatic system, sometimes called a "Hilbert-style" deductive system, is a type of system of formal deduction developed by Gottlob Frege, Jan Łukasiewicz, Russell and Whitehead, and David Hilbert. These deductive systems are most often studied for first-order logic, but are of interest for other logics as well.
In mathematics and philosophy, Łukasiewicz logic is a non-classical, many-valued logic. It was originally defined in the early 20th century by Jan Łukasiewicz as a three-valued modal logic; it was later generalized to n-valued as well as infinitely-many-valued (ℵ0-valued) variants, both propositional and first order. The ℵ0-valued version was published in 1930 by Łukasiewicz and Alfred Tarski; consequently it is sometimes called the Łukasiewicz–Tarski logic. It belongs to the classes of t-norm fuzzy logics and substructural logics.