LP, the Larch Prover -- Variables

A variable is a symbol that represents an arbitrary element of some sort. A variable can be an unqualified variable identifier or a variable identifier qualified by a sort.

Syntax

<variable>   ::= <variableId> [ : <sort> ]
<variableId> ::= <simpleId>

Examples

x
x:Int
committee: Set[Person]

Usage

All variables must be declared in a declare variables command. Case is significant in variable identifiers. Thus x and X are different variables.

The same <variableId> can be overloaded to name two different variables, that is, two variables with different sorts. It can also be used to name a variable and an operator, provided the operator is not a constant of the same sort. LP uses context to disambiguate overloaded identifiers.

At times (e.g., when computing critical pairs or when proving an induction rule), LP creates variables, the identifiers for which consist of the first letter of the sort of the variable, followed by digits if necessary to avoid conflicts with constants and with other variables in the same term or formula.