O'Reilly logo

Handbook of Automated Reasoning by Andrei Voronkov, Alan J.A. Robinson

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

In the above picture, nodes satisfying φ are shown solid (or as a shaded area), whereas ψ nodes are indicated by a circle.

The operator A U+ can be expressed by E U+ and A F+ . This characterization is similar to the definition of the unless-operator in linear temporal logic, cf. page 1648:

A ( φ U + ψ ) ( A ( φ W + ψ ) A F + ψ ) = ( ¬ E ( ¬ ψ U + ¬ ( φ ψ ) ) A F + ψ ) .

si245_e

Therefore, it is sufficient to consider only the two basic operators E U + and A F+ in formal proofs and algorithms. Similarly, the formula E(φ W+ ψ) can be replaced by (E(φ U+ ψ) ∨ EG+ φ). However, there is no negation-free ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required