| Formulae |
| predn(arg1,...,argn) | atomic |
| (c = c') | equality |
| ~A | negation |
| (A & B) | conjunction |
| (A | B) | disjunction |
| EX A | existential |
| <>A | modal |
| +pred(arg) | additive particle |
| (A - B) | apposition |
|
- Equality statements have parentheses. pred(arg) statements do not.
- Pronouns are written pN, where N is any integer. They can be arguments to predicates and =.
- Variables must be in capital letters.
- No free variables.
- The existential binds exactly one variable (though Es can be nested).
- White space in formulae is ignored.
- In appositives A - B, formula B is interpreted in the actual state (even when deeply embedded).
- A formula +pred(arg) is defined iff pred(arg') is entailed by the input state, for arg ≠ arg'. Where defined,
the update is pred(arg).
|