LP, the Larch Prover — The statistics command

The statistics command displays information about the resources consumed by LP, as well as about the usage of rewrite and deduction rules.

Syntax

<statistics-command> ::= statistics [ <statistics-option> ]
<statistics-option>  ::= time | usage [ <names> ]
Note: The first word of the <statistics-option> command can be abbreviated.

Examples

statistics
stat usage nat

Usage

The statistics command displays cumulative and recent (since the last display) information about LP's operation. The default option is time, which displays information about the time used by LP together with the current size of the heap, the amount of free space available, and the number of garbage collections that have occurred.

The usage option displays information about the use of the rewrite and deduction rules matched by <names>, which defaults to "*". For rewrite rules, the information includes the number of successful applications, the number of attempted applications, and the number of nontrivial critical pairs computed from the rule. For deduction rules, the information includes the number of successful applications. In the display, each name is preceded by (rr) or (dr) to indicate whether the named fact is a rewrite rule or a deduction rule. If two or more facts had the same name, then the display show separate statistics for each incarnation of the name (for example, if two theorems, thm.1 and thm.2, were proved by cases, then two separate rewrite rules would have received the name thmCaseHyp1.1).

See also