Options
Examples
Click the following examples to load them.
Syntax
- first-order variables start with a lowercase letter: x,x',y1,z_n...
- second-order variables start with an uppercase letter: X,X',Y1,Z_i...
- Boolean conjunction is denoted by /\
- Boolean disjunction is denoted by \/
- Boolean implication is infix ->
- Boolean negation is prefix !
- Falsity and truth constants are F and T
- The following infix symbols allow one to compare variables, with
their usual interpretations: <, >, <=, =>, =,
<>, \in
- Existential quantification is written '\E x, ...'
- Universal quantification is written '\A x, ...'
(the order of the quantitifications is determined by the case
of the variable name; successive quantifications of the same kind
can be grouped as follows: '\E x Y Z, ...',
'\A x Y Z, ...')
|
|