A logic developed by Leslie Lamport, which combines Temporal Logic with a logic of actions. It is used to describe behaviours of concurrent programs. Leslie Lamport Dr. Leslie Lamport is an American computer scientist. ...
Statements in temporal logic of the form [A]t, where A is an action and t contains a subset of the variables appearing in A. An action is an expression containing primed and non-primed variables, such as x + x' * y = y'. The meaning of the non-primed variables is the variable's value in this state. The meaning of primed variables is the variable's value in the next state. The above expression means the value of x now, plus the value of x tomorrow times the value of y now, equals the value of y tomorrow.
The meaning of [A]t is that either A is valid now, or the variables appearing in t do not change. This allows for stuttering steps, in which none of the program variables change their values.
Mathematical logic really refers to two distinct areas of research: the first is the application of the techniques of formal logic to mathematics and mathematical reasoning, and the second, in the other direction, the application of mathematical techniques to the representation and analysis of formal logic.
The boldest attempt to apply logic to mathematics was undoubtedly the logicism pioneered by philosopher-logicians such as Gottlob Frege and Bertrand Russell: the idea was that mathematical theories were logical tautologies, and the programme was to show this by means to a reduction of mathematics to logic.
Logic is extensively applied in the fields of artificial intelligence, and computer science, and these fields provide a rich source of problems in formal logic.