theory Rules begin // The syntax for rules is: rule RuleName: [ Premise1(), Premise2(), PremiseK() ] --[ Action1(), Action2(), ActionK() ]-> [ Conclusion1(), Conclusion2(), ConclusionK() ] /* * Facts can have any arity, of course, and the same * fact can appear multiple times. If a rule is /silent/, * i.e., it has no action, then --[ ]-> can be abbreviated -->. * For example: */ rule SilentRule: [ Premise1(), Premise2(), PremiseK() ] --> [ Conclusion1(), Conclusion2(), ConclusionK() ] /* * Of course, this is a correct program, so you can run it! * (There is still nothing to be verified, though!) */ end