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.

Syntax

<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

Examples

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

Usage

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, ...