Prev Up Next
Go backward to 2.3.1 Quantifications
Go up to 2.3 Axioms
Go forward to 2.3.3 Atomic Formulae

2.3.2 Logical Connectives

These formulae determine the usual logical connectives on the sub-formulae. Conjunction and disjunction apply to lists of two or more formulae; they both have weaker precedence than negation. When mixed, they have to be explicitly grouped, using parentheses `(...)'.

Both implication (which may be written in two different ways) and equivalence have weaker precedence than conjunction and disjunction. When the `forward' version of implication is iterated, it is implicitly grouped to the right; the `backward' version is grouped to the left. When these constructs are mixed, they have to be explicitly grouped.

  • Conjunction
  • Disjunction
  • Implication
  • Equivalence
  • Negation

  • CoFI Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
    Comments to

    Prev Up Next