LP, the Larch Prover -- The write command

The write command creates a file containing commands that can be executed to recreate LP's current logical system.


<write-command> ::= write <file> [ <names> ]


write axioms
write intSet int, set


The write command creates a file named <file>.lp (unless <file> contains a period, in which case LP does not supply the suffix .lp) in LP's current working directory. This file can be executed later with the execute command to recreate the named set of facts (or the whole system, if no names are specified). In particular, LP writes declarations for all identifiers in the named set of facts followed by commands to register ordering constraints for the facts and to assert the facts.

Unlike the freeze command, the write command does not save information about the state of uncompleted proofs. But unlike thawing a frozen file, which replaces all of LP's logical system, executing a written file adds information to the current system. Hence it can be used to combine axiomatizations.

Rewrite rules written by the write command are asserted as formulas. The numeric extensions in the names assigned to facts may change when the .lp file is executed; hence facts that are ancestor-immune may behave differently when the system is recreated.

See also