LP, the Larch Prover -- Terms

A term in multisorted first-order logic denotes an element of some sort. A term can be an atomic term (i.e., a variable or a constant), or it can be a compound term with one of the following forms:

functional, e.g., f(x) or min(x, y)
infix, e.g., x + y
prefix, e.g., -x
postfix, e.g, x! or q.last
bracketed, e.g., a[i]
conditional, e.g., if x < 0 then -x else x
quantified, e.g., \A x \E y (x < y)

Syntax

<term>          ::= if <term> then <term> else <term>
                       | <subterm>
<subterm>       ::= <subterm> ( <simpleOp> <subterm> )+
                       | ( <simpleOp> | <quantifier> )* <simpleOp> <secondary>
                       | ( <simpleOp> | <quantifier> )* <quantifier> <primary>
                       | <secondary> <simpleOp>*
<secondary>     ::= <primary>
                       | [ <bracketPre> ] <bracketed> [ <bracketPost> ]
<primary>       ::= <primaryHead> <primaryTail>*
<primaryHead>   ::= <simpleId> [ "(" <term>+, ")" ]
                       | "(" <term> ")"
<primaryTail>   ::= "." <primaryHead> | <qualification>
<qualification> ::= ":" <sort>
<bracketPre>    ::= <primaryHead> | <primary> . <primaryHead>
<bracketed>     ::= <openSym> <term>*, <closeSym> [ <qualification> ]
<bracketPost>   ::= <primary> | . <primaryHead> <primaryTail>*

Restrictions: Terms must type-check, that is, all operators must be applied to arguments with sorts in the operator's signature. The following combinations of <simpleOp>s cannot appear in a <subterm> unless they are separated by <simpleOp>s that bind less tightly:

more than one =>, =, or ~=
both /\ and \/
both = and ~=
two different user-declared <simpleOp>s

Usage

LP uses the following kinds of information to resolve potential ambiguities in terms:

Operator precedence, when two <simpleOp>s appear in the same <subterm>
Context, when overloaded operators appear in a term
Explicit <qualification>s appearing in a term