Event calculus

Last updated

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.

Contents

The event calculus represents the state of the world at any time by the set of all the facts (called fluents ) that hold at the time. Events initiate and terminate fluents:

A fluent holds at a time
if the fluent is initiated by an event that happens at an earlier time
and the fluent is not terminated by any event that happens in the meantime.[ citation needed ]

The event calculus differs from most other approaches for reasoning about change by reifying time, associating events with the time at which they happen, and associating fluents with the times at which they hold.

The original version of the event calculus, introduced by Robert Kowalski and Marek Sergot in 1986, [1] was formulated as a logic program and developed for representing narratives and database updates. [2] Kave Eshghi showed how to use the event calculus for planning, [3] by using abduction to generate hypothetical actions to achieve a desired state of affairs.

It was extended by Murray Shanahan and Rob Miller in the 1990s [4] and reformulated in first-order logic with circumscription. These and later extensions have been used to formalize non-deterministic actions, concurrent actions, actions with delayed effects, gradual changes, actions with duration, continuous change, and non-inertial fluents.

Van Lambalgen and Hamm showed how a formulation of the event calculus as a constraint logic program can be used to give an algorithmic semantics to tense and aspect in natural language. [5]

Fluents and events

In the event calculus, fluents are reified. This means that fluents are represented by terms. For example, expresses that the is on the at time . Here is a predicate, while is a term. In general, the atomic formula

expresses that the holds at the

Events are also reified and represented by terms. For example, expresses that the is moved onto the at time . In general:

expresses that the happens at the

The relationships between events and the fluents that they initiate and terminate are also represented by atomic formulae:

expresses that if the happens at the then the becomes true after the .
expresses that if the happens at the then the ceases to be true after the .

Domain-independent axiom

The event calculus was developed in part as an alternative to the situation calculus, [6] [7] as a solution to the frame problem, of representing and reasoning about the way in which actions and other events change the state of some world.

There are many variants of the event calculus. But the core axiom of one of the simplest and most useful variants can be expressed as a single, domain-independent axiom:

The axiom states that

a fluent holds at a time if
an event happens at a time and
initiates at and
is before and
it is not the case that there exists an event and a time such that
happens at and
terminates at and
is before or at the same time as and
is before .

The event calculus solves the frame problem by interpreting this axiom in a non-monotonic logic, such as first-order logic with circumscription [8] or, as a logic program, in Horn clause logic with negation as failure. [1] In fact, circumscription is one of the several semantics that can be given to negation as failure, [9] and it is closely related to the completion semantics for logic programs [10] (which interprets if as if and only if).

The core event calculus axiom defines the predicate in terms of the , , , and predicates. To apply the event calculus to a particular problem, these other predicates also need to be defined.

The event calculus is compatible with different definitions of the temporal predicates and . In most applications, times are represented discretely, by the natural numbers, or continuously, by non-negative real numbers. However, times can also be partially ordered.

Domain-dependent axioms

To apply the event calculus in a particular problem domain, it is necessary to define the and predicates for that domain. For example, in the blocks world domain, an event of moving an object onto a place intitiates the fluent , which expresses that the object is on the place and terminates the fluent , which expresses that the object is on a different place:

If we want to represent the fact that a holds in an initial state, say at time 1, then with the simple core axiom above we need an event, say , which initiates the at any time:

Problem-dependent axioms

To apply the event calculus, given the definitions of the , , , and predicates, it is necessary to define the predicates that describe the specific context of the problem.

For example, in the blocks world domain, we might want to describe an initial state in which there are two blocks, a red block on a green block on a table, like a toy traffic light, followed by moving the red block to the table at time 1 and moving the green block onto the red block at time 3, turning the traffic light upside down:

A Prolog implementation

The event calculus has a natural implementation in pure Prolog (without any features that do not have a logical interpretation). For example, the blocks world scenario above can be implemented (with minor modifications) by the program:

holdsAt(Fluent,Time2):-before(Time1,Time2),happensAt(Event,Time1),initiates(Event,Fluent,Time1),not(clipped(Fluent,Time1,Time2)).clipped(Fluent,Time1,Time2):-terminates(Event,Fluent,Time),happensAt(Event,Time),before(Time1,Time),before(Time,Time2).initiates(initialise(Fluent),Fluent,Time).initiates(move(Object,Place),on(Object,Place),Time).terminates(move(Object,Place),on(Object,Place1),Time).happensAt(initialise(on(green_block,table)),0).happensAt(initialise(on(red_block,green_block)),0).happensAt(move(red_block,table),1).happensAt(move(green_block,red_block),3).

The Prolog program differs from the earlier formalisation in the following ways:

Given an appropriate definition [note 1] of the predicate before(Time1,Time2), the Prolog program generates all answers to the query what holds when? in temporal order:

?-holdsAt(Fluent,Time).Fluent=on(green_block,table),Time=1.Fluent=on(red_block,green_block),Time=1.Fluent=on(green_block,table),Time=2.Fluent=on(red_block,table),Time=2.Fluent=on(green_block,table),Time=3.Fluent=on(red_block,table),Time=3.Fluent=on(red_block,table),Time=4.Fluent=on(green_block,red_block),Time=4.Fluent=on(red_block,table),Time=5.Fluent=on(green_block,red_block),Time=5.

The program can also answer negative queries, such as which fluents do not hold at which times? However, to work correctly, all variables in negative conditions must first be instantiated to terms containing no variables. For example:

timePoint(1).timePoint(2).timePoint(3).timePoint(4).timePoint(5).fluent(on(red_block,green_block)).fluent(on(green_block,red_block)).fluent(on(red_block,table)).fluent(on(green_block,table)).?-timePoint(T),fluent(F),not(holdsAt(F,T)).F=on(green_block,red_block),T=1.F=on(red_block,table),T=1.F=on(red_block,green_block),T=2.F=on(green_block,red_block),T=2.F=on(red_block,green_block),T=3.F=on(green_block,red_block),T=3.F=on(red_block,green_block),T=4.F=on(green_block,table),T=4.F=on(red_block,green_block),T=5.F=on(green_block,table),T=5.

Reasoning tools

In addition to Prolog and its variants, several other tools for reasoning using the event calculus are also available:

Extensions

Notable extensions of the event calculus include Markov logic networks–based variants [11] probabilistic, [12] epistemic [13] and their combinations. [14]

See also

Related Research Articles

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.

Logic programming is a programming, database and knowledge representation paradigm based on formal logic. A logic program is a set of sentences in logical form, representing knowledge about some problem domain. Computation is performed by applying logical reasoning to that knowledge, to solve problems in the domain. Major logic programming language families include Prolog, Answer Set Programming (ASP) and Datalog. In all of these languages, rules are written in the form of clauses:

Lambda calculus is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation that can be used to simulate any Turing machine. It was introduced by the mathematician Alonzo Church in the 1930s as part of his research into the foundations of mathematics.

<span class="mw-page-title-main">Relative density</span> Ratio of two densities

Relative density, also called specific gravity, is a dimensionless quantity defined as the ratio of the density of a substance to the density of a given reference material. Specific gravity for liquids is nearly always measured with respect to water at its densest ; for gases, the reference is air at room temperature. The term "relative density" is often preferred in scientific usage, whereas the term "specific gravity" is deprecated.

Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming languages. It is based on combinators, which were introduced by Schönfinkel in 1920 with the idea of providing an analogous way to build up functions—and to remove any mention of variables—particularly in predicate logic. A combinator is a higher-order function that uses only function application and earlier defined combinators to define a result from its arguments.

In programming language theory, subtyping is a form of type polymorphism. A subtype is a datatype that is related to another datatype by some notion of substitutability, meaning that program elements, written to operate on elements of the supertype, can also operate on elements of the subtype.

The meet-in-the-middle attack (MITM), a known plaintext attack, is a generic space–time tradeoff cryptographic attack against encryption schemes that rely on performing multiple encryption operations in sequence. The MITM attack is the primary reason why Double DES is not used and why a Triple DES key (168-bit) can be brute-forced by an attacker with 256 space and 2112 operations.

System F is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorphism in programming languages, thus forming a theoretical basis for languages such as Haskell and ML. It was discovered independently by logician Jean-Yves Girard (1972) and computer scientist John C. Reynolds.

Predicate transformer semantics were introduced by Edsger Dijkstra in his seminal paper "Guarded commands, nondeterminacy and formal derivation of programs". They define the semantics of an imperative programming paradigm by assigning to each statement in this language a corresponding predicate transformer: a total function between two predicates on the state space of the statement. In this sense, predicate transformer semantics are a kind of denotational semantics. Actually, in guarded commands, Dijkstra uses only one kind of predicate transformer: the well-known weakest preconditions.

In propositional logic, a propositional formula is a type of syntactic formula which is well formed and has a truth value. If the values of all variables in a propositional formula are given, it determines a unique truth value. A propositional formula may also be called a propositional expression, a sentence, or a sentential formula.

The situation calculus is a logic formalism designed for representing and reasoning about dynamical domains. It was first introduced by John McCarthy in 1963. 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 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 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:

In mathematics, Church encoding is a means of representing data and operators in the lambda calculus. The Church numerals are a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded data in the lambda calculus this way.

SLD resolution is the basic inference rule used in logic programming. It is a refinement of resolution, which is both sound and refutation complete for Horn clauses.

In artificial intelligence and related fields, an argumentation framework is a way to deal with contentious information and draw conclusions from it using formalized arguments.

Vector logic is an algebraic model of elementary logic based on matrix algebra. Vector logic assumes that the truth values map on vectors, and that the monadic and dyadic operations are executed by matrix operators. "Vector logic" has also been used to refer to the representation of classical propositional logic as a vector space, in which the unit vectors are propositional variables. Predicate logic can be represented as a vector space of the same type in which the axes represent the predicate letters and . In the vector space for propositional logic the origin represents the false, F, and the infinite periphery represents the true, T, whereas in the space for predicate logic the origin represents "nothing" and the periphery represents the flight from nothing, or "something".

Algorithmic logic is a calculus of programs that allows the expression of semantic properties of programs by appropriate logical formulas. It provides a framework that enables proving the formulas from the axioms of program constructs such as assignment, iteration and composition instructions and from the axioms of the data structures in question see Mirkowska & Salwicki (1987), Banachowski et al. (1977).

In model checking, a branch of computer science, linear time properties are used to describe requirements of a model of a computer system. Example properties include "the vending machine does not dispense a drink until money has been entered" or "the computer program eventually terminates". Fairness properties can be used to rule out unrealistic paths of a model. For instance, in a model of two traffic lights, the liveness property "both traffic lights are green infinitely often" may only be true under the unconditional fairness constraint "each traffic light changes colour infinitely often".

References

  1. 1 2 Kowalski, Robert; Sergot, Marek (1986-03-01). "A logic-based calculus of events". New Generation Computing. 4 (1): 67–95. doi:10.1007/BF03037383. ISSN   1882-7055. S2CID   7584513.
  2. Kowalski, Robert (1992-01-01). "Database updates in the event calculus". The Journal of Logic Programming . 12 (1): 121–146. doi: 10.1016/0743-1066(92)90041-Z . ISSN   0743-1066.
  3. Eshghi, Kave (1988). "Abductive planning with event calculus". Iclp/SLP: 562–579.
  4. Miller, Rob; Shanahan, Murray (2002), Kakas, Antonis C.; Sadri, Fariba (eds.), "Some Alternative Formulations of the Event Calculus", Computational Logic: Logic Programming and Beyond: Essays in Honour of Robert A. Kowalski Part II, Lecture Notes in Computer Science, Berlin, Heidelberg: Springer, pp. 452–490, doi:10.1007/3-540-45632-5_17, ISBN   978-3-540-45632-2 , retrieved 2020-10-05
  5. Lambalgen, Hamm (2005). The proper treatment of events. Malden, MA: Blackwell Pub. ISBN   978-0-470-75925-7. OCLC   212129657.
  6. J. McCarthy and P. Hayes (1969). Some philosophical problems from the standpoint of artificial intelligence. In B. Meltzer and D. Michie, editors, Machine Intelligence, 4:463–502. Edinburgh University Press, 1969.
  7. R. Reiter (1991). The frame problem in the situation calculus: a simple solution (sometimes) and a completeness result for goal regression. In Vladimir Lifshitz, editor, Artificial intelligence and mathematical theory of computation: papers in honour of John McCarthy, pages 359–380, San Diego, CA, USA. Academic Press Professional, Inc. 1991.
  8. Shanahan, M. (1997) Solving the frame problem: A mathematical investigation of the common sense law of inertia . MIT Press.
  9. Gelfond, M.; Przymusinska, H.; Przymusinski, T. (1989). "On the relationship between circumscription and negation as failure". Artificial Intelligence . 38 (1): 75–94. doi:10.1016/0004-3702(89)90068-4.
  10. Clark, K.L. (1977). "Negation as Failure". Logic and Data Bases. Boston, MA: Springer US. pp. 293–322. doi:10.1007/978-1-4684-3384-5_11. ISBN   978-1-4684-3386-9.
  11. Skarlatidis, Anastasios; Paliouras, Georgios; Artikis, Alexander; Vouros, George A. (2015-02-17). "Probabilistic Event Calculus for Event Recognition". ACM Transactions on Computational Logic . 16 (2): 11:1–11:37. arXiv: 1207.3270 . doi:10.1145/2699916. ISSN   1529-3785. S2CID   6389629.
  12. Skarlatidis, Anastasios; Artikis, Alexander; Filippou, Jason; Paliouras, Georgios (March 2015). "A probabilistic logic programming event calculus". Theory and Practice of Logic Programming . 15 (2): 213–245. arXiv: 1204.1851 . doi: 10.1017/S1471068413000690 . ISSN   1471-0684. S2CID   5701272.
  13. Ma, Jiefei; Miller, Rob; Morgenstern, Leora; Patkos, Theodore (2014-07-28). "An Epistemic Event Calculus for ASP-based Reasoning About Knowledge of the Past, Present and Future". EPiC Series in Computing. EasyChair. 26: 75–87. doi: 10.29007/zswj .
  14. D'Asaro, Fabio Aurelio; Bikakis, Antonis; Dickens, Luke; Miller, Rob (2020-10-01). "Probabilistic reasoning about epistemic action narratives". Artificial Intelligence . 287: 103352. doi:10.1016/j.artint.2020.103352. ISSN   0004-3702. S2CID   221521535.

Further reading

Notes

  1. For example:
    before(Time1,Time2):-timeline(Eternity),append(Before,[Time2|After],Eternity),member(Time1,Before).timeline([0,1,2,3,4,5]).