Here are the formulas. =0pt
This relates the operator not as applied to fluents to logical negation.
This tells us that an action succeeds in a situation s if all its preconditions hold in the situation. Actually, it's a definition of the predicate succeeds.
If an action succeeds in a situation and it is one that causes a fluent to hold, then the fluent holds in the situation that results from the preformance of the action.
This tells us that unless an action affects a fluent, then the fluent holds after the action if it held before the action.
This and the next axiom give the effects of events different from actions.
This is an abbreviation for the situation that results from an action after all the events that occur after it have happened.
This is the first axiom specifically about the effects of flying. It says that flying from x to y causes being at y.
You must be at x to fly from there to y.
Also you must have a ticket.
And there must be a flight.
The effect of losing a ticket.
The effect of buying a ticket.
This is the first fact about the initial situation S0. The traveller is at Glasgow.
He has a ticket in S0
The necessary flights exist.
This is the circumscription of the predicates causes, precond, noninertial and occurs with holds allowed to vary that is done with the conjunction (called Facts) of these axioms. Understanding this may require reading [McCarthy 1987]; (Lifschitz 1987) would also help. Once the circumscription has been done, we can show
but not if we add
However, in this case we can show
