LP, the Larch Prover -- Naming facts in commands

Many LP commands require one or two sets of facts as arguments, which users describe in terms of the names and kinds of facts they contain.


<names>          ::= <name-primary>+,
                        | <name-primary> ("/" <name-primary>)+
                        | <name-primary> ("~" <name-primary>)+
<name-primary>   ::= <name-pattern> | <class> | "(" [ <names> ] ")"
<name-pattern>   ::= <prefix-pattern> [ . ] 
                        | <prefix-pattern> <extension>+ [ : <last> ] [ ! ]
<prefix-pattern> ::= ( <simpleId> | "*" )+
<last>           ::= <number> | last


arith, set.2:last
* ~ (nat, set)


Subsets of LP's logical system are described by expressions (called <names>) built up from primitive descriptions using operators for union (","), intersection ("/"), and difference ("~"). Parentheses specify the associativity of these infix operators. The empty set is named by (), and the set of all facts in LP's logical system is named by *.

Primitive <names> include <name>s (e.g., set.2) and <name-pattern>s of the following forms, where N is a <name> that may have asterisks embedded in its alphanumeric prefix (e.g., * and *Hyp.1), and where m and n are positive integers.

Pattern    Facts denoted by pattern
-------    ------------------------
N!         those with names that can be obtained from N by replacing the
           asterisks in N by alphanumeric characters
N          those denoted by N! and all their descendents
N.m:n!     those denoted by N.m!, N.m+1!, ..., N.n!
N.m:n      those denoted by N.m, N.m+1, ..., N.n
N.m:last!  those denoted N.m!, N.m+1!, ...
N.m:last   those denoted N.m, N.m+1, ...

See also <class>.