diff options
Diffstat (limited to 'books/workshops/1999/ivy/ivy-v2/ivy-sources/examples/steam')
| -rw-r--r-- | books/workshops/1999/ivy/ivy-v2/ivy-sources/examples/steam | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/books/workshops/1999/ivy/ivy-v2/ivy-sources/examples/steam b/books/workshops/1999/ivy/ivy-v2/ivy-sources/examples/steam new file mode 100644 index 0000000..1d890af --- /dev/null +++ b/books/workshops/1999/ivy/ivy-v2/ivy-sources/examples/steam @@ -0,0 +1,35 @@ +;; IVY operation: PROVE +;; +;; Schubert's Steamroller. + +(imp (and (all x (imp (Wolf x) (animal x))) + (all x (imp (Fox x) (animal x))) + (all x (imp (Bird x) (animal x))) + (all x (imp (Snail x) (animal x))) + (all x (imp (Grain x) (plant x))) + (exists x (Wolf x)) + (exists x (Fox x)) + (exists x (Bird x)) + (exists x (Snail x)) + (exists x (Grain x)) + (all x (all y (imp (and (Snail x) (Bird y)) (Smaller x y)))) + (all x (all y (imp (and (Bird x) (Fox y)) (Smaller x y)))) + (all x (all y (imp (and (Fox x) (Wolf y)) (Smaller x y)))) + (all x (imp (Snail x) (exists y (and (plant y) (eats x y))))) + (all x (all y (imp (and (Wolf x) (Fox y)) (not (eats x y))))) + (all x (all y (imp (and (Wolf x) (Grain y)) (not (eats x y))))) + (all x (all y (imp (and (Bird x) (Snail y)) (not (eats x y))))) + (all x (imp (animal x) + (or (all y (imp (plant y) (eats x y))) + (all z (imp (and (animal z) + (Smaller z x) + (exists u (and (plant u) + (eats z u)))) + (eats x z))))))) + + (exists x (exists y (and (animal x) + (animal y) + (eats x y) + (all z (imp (grain z) (eats y z))))))) + + |