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:

Usage

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