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:

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