Logic programming is a programming paradigm based on mathematical logic. A logic program, written in a language like Prolog, is a set of axioms representing a logical theory. When such a program is executed, the computer attempts to prove or disprove the theory, and due to the connection to mathematical logic a logic programming system can take advantage of established proof procedures. As logical theories are a way of expressing reasoning problems, logic programming is used to automate the solving of intelligent reasoning tasks. The paradigm was influenced by Artificial Intelligence research, and it continues to be of interest in this field, particularly for expert systems, theorem proving and the Semantic Web.
An autonomous agent is a program that interacts with some (possibly artificial) environment. The environment is perceived with *sensors*. Based on its percepts an autonomous agent decides on the actions to take, which are then executed with the help of special *effectors* for manipulating the environment. An agent may pro-actively initiate some behaviors to achieve goals. Autonomous robots can be seen as special cases of autonomous agents that interact with the real world instead of an artificial environment.
The specification of behaviors an agent may execute is a complex task, particularly if several agents have to cooperate to achieve a goal. The use of formal specification methods allows for proving certain features of a behavior, e.g. the absence of unwanted side effects, which is especially important in safety critical application domains like rescue scenarios.