LP, the Larch Prover

LP is an interactive theorem proving system for multisorted first-order logic. It is currently used at MIT and elsewhere to reason about designs for circuits, concurrent algorithms, hardware, and software. Unlike most theorem provers, which attempt to find proofs automatically for correctly stated conjectures, LP is intended to assist users in finding and correcting flaws in conjectures---the predominant activity in the early stages of the design process.

LP works efficiently on large problems, has many important user amenities, and can be used by relatively naive users. It was developed by Stephen J. Garland and John V. Guttag at the MIT Laboratory for Computer Science. It is currently maintained by Stephen J. Garland.

For a general introduction to LP, see the following topics.

The entire set of pages describing LP is also available as a single, printable document.

 

Table of contents

 

Introduction

LP is an interactive theorem proving system for multisorted first-order logic. It is currently used at MIT and elsewhere to reason about designs for circuits, concurrent algorithms, hardware, and software. Unlike most theorem provers, which attempt to find proofs automatically for correctly stated conjectures, LP is intended to assist users in finding and correcting flaws in conjectures---the predominant activity in the early stages of the design process.

LP works efficiently on large problems, has many important user amenities, and can be used by relatively naive users. It was developed by Stephen J. Garland and John V. Guttag at the MIT Laboratory for Computer Science. It is currently maintained by Stephen J. Garland.

For a general introduction to LP, see the following topics.

The entire set of pages describing LP is also available as a single, printable document.

 

Design philosophy

The philosophy behind LP is different from that underlying most theorem provers. Its design is based on the observation that initial attempts to state interesting conjectures correctly, and then prove them, hardly ever succeed on the first try. Sometimes the conjecture is wrong. Sometimes the formalization is incorrect or incomplete. Sometimes the proof strategy is flawed or not detailed enough. As a result, LP is designed to assist in reasoning by carrying out routine (and possibly lengthy) steps in a proof automatically and by providing useful information about why proofs fail, if and when they do.

Because conjectures are often flawed, LP is not designed to find difficult proofs automatically. For example, LP does not use heuristics to formulate additional conjectures that might be useful in a proof. Instead, LP makes it easy for users to employ standard techniques such as simplification and proofs by cases, induction, and contradiction, either to construct proofs or to understand why they have failed.

LP also provides support for rechecking proofs following changes in axioms, conjectures, or proof strategies. This support assists users in regression testing during proof construction: when users discover they must change a formalization in order to establish some conjecture, regression testing ensures that the change does not invalidate previously constructed proofs. This support also promotes proof re-use: users can edit old proofs to prove new conjectures, and LP will check that the progress of the proof stays ``in sync'' with the users' intentions.

 

Some sample proofs

We illustrate how to use LP by presenting some sample proofs along with explanatory comments. The proofs show how to derive some basic facts about finite sets from a simple axiomatization.

 

Sample proofs: getting started

To invoke LP, type lp at the Unix command prompt. LP will respond with the following message: 
Welcome to LP (the Larch Prover), Release 3.1 (94/12/30).
Copyright (C) 1994, S. J. Garland and J. V. Guttag
Type `help lp' (followed by a carriage return) for help.

LP1:
LP is a command-driven system. The last line of LP's welcoming message, LP1:, is a prompt for the first command. LP prompts users to enter subsequent commands with LP2:, LP3:, ...

You can type input directly in response to LP's prompts, or you can create a file of LP commands (e.g., set1.lp) and then use LP's execute command to cause LP to execute the commands in that file as if you had typed them directly. Here's the start of a session in which commands are executed from the file set1.lp: 

LP1: execute set1

LP1.1: % Some simple theorems about finite sets

LP1.2:
The first command, execute set1, was typed by the user. The second was obtained from the file set1.lp. This command is a comment: LP ignores all input following a percent sign. The prompts LP1.1: and LP1.2: indicate that LP is taking input from the file being executed as a result of the command entered in response to the prompt LP1:.

 

Sample proof: declarations

The first three commands in set1.lp declare symbols for use in axiomatizing the properties of sets of elements. 
declare sorts E, S
declare variables e, e1, e2: E, x, y, z: S
declare operators
  {}:                   -> S
  {__}:            E    -> S
  insert:          E, S -> S
  __ \union __:    S, S -> S
  __ \in __:       E, S -> Bool
  __ \subseteq __: S, S -> Bool
  ..
The first declare command introduces names for two sorts, E and S. LP predefines the boolean sort Bool.

The second command introduces variables ranging over E and S. These variables will be used when stating axioms and conjectures.

The third command introduces symbols for the operators whose properties we will axiomatize. This command uses LP's multi-line input convention: if the arguments for a command do not fit on the line containing the command, they can be given on subsequent lines. Two periods (..) mark the end of the command.

The declaration for each operator specifies sorts for the operator's arguments and the sort of its result. Operators like {} with no arguments are constants. Operators like insert are used in functional notations like insert(e, x). The placeholders in operators like {__} and __\in__ indicate where their arguments belong in notations like {e} and e \in x.

 

Sample proof: axioms for finite sets

The next several commands in set1.lp axiomatize the properties of finite sets of elements. 
set name setAxioms
assert
  sort S generated by {}, insert;
  {e} = insert(e, {});
  ~(e \in {});
  e \in insert(e1, x) <=> e = e1 \/ e \in x;
  {} \subseteq x;
  insert(e, x) \subseteq y <=> e \in y /\ x \subseteq y;
  e \in (x \union y) <=> e \in x \/ e \in y
  ..
set name extensionality
assert \A e (e \in x <=> e \in y) => x = y
The set command directs LP to assign the names setAxioms.1, setAxioms.2, ... to the axioms introduced by the subsequent assert commands. When multiple axioms are asserted in a single command, they are separated by semicolons.

The axioms are formulated using declared symbols (for sorts, variables, and operators) together with logical symbols for equality (=), negation (~), conjunction (/\), disjunction (\/), implication (=>), logical equivalence (<=>), and universal quantification (\A). LP also provides a symbol for existential quantification (\E). LP uses a limited amount of \llink{precedence} when parsing formulas: for example, the logical operator <=> binds less tightly than the other logical operators, which bind less tightly than the equality operator, which bind less tightly than declared operators like \in and \union.

 

Sample proofs: useful kinds of axioms

The axioms in set1.lp fall into several categories:

Induction rules
The first axiom, sort Set generated by {}, insert, asserts that all elements of sort S can be obtained by finitely many applications of insert to {}. It provides the basis for definitions and proofs by induction.

Explicit definitions
The second axiom, {e} = insert(e, {}), is a single formula that defines the operator {__} (as a constructor for a singleton set).

Inductive definitions
The next two pairs of axioms provide induction definitions of the membership operator \in and the subset operator \subseteq. Inductive definitions generally consist of one formula per generator.

Implicit definitions
The final formula, e \in (x \union y) <=> e \in x \/ e \in y, in the first assert command, together with the other axioms, completely constrains the interpretation of the \union operator.

Constraining properties
The second assert command formalizes the principle of extensionality, which asserts that any two sets with exactly the same elements must be the same set.

 

Sample proofs: sample conjectures

We will illustrate LP's proof mechanisms by proving the following sample conjectures: 
set name setTheorems
prove e \in {e}
prove \E x \A e (e \in x <=> e = e1 \/ e = e2)
prove x \union {} = x
prove x \union insert(e, y) = insert(e, x \union y)
prove ac \union
prove e \in x /\ x \subseteq y => e \in y
prove x \subseteq y /\ y \subseteq x => x = y
prove (x \union y) \subseteq z <=> x \subseteq z /\ y \subseteq z
prove sort S generated by {}, {__}, \union
prove x \subseteq (x \union y)
prove x \subseteq x
Except for the fourth, the sample conjectures are like the sample axioms: they are either formulas or induction rules. The fourth, ac \union, is an abbreviation for the conjunction of the associative and commutative laws for the \union operator. It provides LP with useful operational information. For example, it allows LP to conclude that {} \union x is the same set as x \union {}; hence the third conjecture shows that both of these sets are the same as x.

The order in which we have stated these conjectures is not completely arbitrary. As we shall see, some of them are used to prove conjectures appearing later in the list.

 

Sample proofs: two easy theorems

The proof of the first theorem in set1.lp is straightforward. 
set name setTheorems
prove e \in {e}
qed
The prove command directs LP to initiate the proof of a conjecture, and the qed command directs LP to confirm that its proof is complete. LP proves this conjecture automatically by using the user-supplied axioms as rewrite rules. When using a formula as a rewrite rule, either LP rewrites terms matching the entire formula to true or, when the principal connective of the formula is = (equals) or <=> (if and only if), LP rewrites terms matching the left side of the formula to terms matching the right. Occasionally LP will reverse the order of terms in an equality to ensure that the resulting set of rewrite rules does not produce nonterminating (i.e., infinite) rewriting sequences. Here's how LP proves the first conjecture: 
e \in {e} ~> e \in insert(e, {})    by setAxioms.2
          ~> e = e \/ e \in {}      by setAxioms.4
          ~> true \/ e \in {}       by a hardwired axiom for =
          ~> true                   by a hardwired axiom for \/
Most proofs require user guidance. For example, to prove that for any two elements e1 and e2, there is a set that contains exactly these two elements, the user must provide a ``witness'' for the existential quantifier in the second conjecture: 
prove \E x \A e (e \in x <=> e = e1 \/ e = e2)
  resume by specializing x to insert(e2, {e1})
qed
Users can specify a proof method for a conjecture either as part of the prove command or in a separate resume command, which continues the proof of the conjecture.

 

Sample proofs: three theorems about union

The next three theorems in set1.lp follow from the principle of extensionality. 
prove x \union {} = x
  instantiate y by x \union {} in extensionality
qed
The instantiate command directs LP to form the substitution instance 
\A e (e \in x <=> e \in x \union {}) => x = x \union {}
of the fact name extensionality. LP rewrites this formula automatically to 
\A e (e \in x <=> e \in x \/ e \in {}) => x = x \union {}
using the definition of \union, then to 
\A e (e \in x <=> e \in x \/ false) => x = x \union {}
using the definition of \in, and then successively to 
\A e (e \in x <=> e \in x) => x = x \union {}
\A e (true) => x = x \union {}
true => x = x \union {}
x = x \union {}
using LP's hardwired axioms. LP orients this final simplification into the rewrite rule x \union {} -> x, which it uses to simplify the conjecture to true.

Two other theorems about union can also be proved by instantiating the extensionality axiom. Both proofs are left as exercises to the reader. 

prove x \union insert(e, y) = insert(e, x \union y)
prove ac \union

 

Sample proofs: alternative proofs of theorems about union

Explicit instantiation is not the only way to prove the three conjectures about union in set1.lp. Here's another technique: 
prove x \union {} = x by contradiction
  critical-pairs *Hyp with extensionality
qed
The prove command directs LP to begin an attempt to prove the conjecture by contradiction. LP does this by adding the negation, ~(xc \union {} = xc), of the conjecture as a hypothesis to its logical system. It replaces the variable x in the conjecture by the constant xc, because the negation of a conjecture about all sets x is a statement about some particular set xc. LP also orients this new hypothesis into a rewrite rule, xc \union {} = xc -> false.

The critical-pairs command directs LP to use the rewrite rule obtained from this new hypothesis, whose name setTheoremsContraHyp.1 matches the pattern *Hyp, together with that obtained from the fact whose name matches extensionality, to enlarge its set of rewrite rules. LP does this by finding a term that can be rewritten in two different ways by the two rewrite rules and then asserting that these two terms must be equal. LP finds such a term by unifying the left side of one rewrite rule with a subterm of the left side of the other. Here, LP unifies the left side of the hypothesized rewrite rule with a subterm of the extensionality principle (by mapping x to xc \union {} and y to xc) to obtain the formula 

\A e (e \in (xc \union {}) <=> e \in xc) => xc \union {} = xc
The extensionality axiom rewrites this formula to true, whereas the hypothesized rewrite rule rewrites it to 
\A e (e \in (xc \union {}) <=> e \in xc) => false
Hence these two results must be equivalent: 
\A e (e \in (xc \union {}) <=> e \in xc) => false <=> true
As in our first proof of the conjecture, this formula rewrites to true => false <=> true, which rewrites to false using LP's hardwired axioms. This inconsistency finishes the proof by contradiction.

The file set1.lp uses this technique to prove the second and third theorems about union.

 

Sample proofs: three theorems about subset

The next three theorems in set1.lp establish some basic properties of the subset relation. They illustrate how LP's proof techniques combine to establish conjectures. The user types a few commands to select proof strategies (e.g., a proof by induction or a proof by cases). LP generates subgoals appropriate for the selected strategies and fills in most of the details automatically. Sometimes the user needs to tell LP to work a little harder near the end of a proof to fill in the remaining details. 
set proof-methods normalization, =>
prove e \in x /\ x \subseteq y => e \in y by induction on x
      resume by case ec = e1c
        complete
qed
The set command directs LP to use an automatic proof technique whenever the user does not specify one explicitly. Here, it directs LP to try to prove conjectures first by rewriting, and then to assume the hypotheses of implications and try again. This setting for proof-methods is a good alternative to the standard setting, which consists of normalization alone.

A proof by induction

The user directs LP to begin the proof of the conjecture by induction on the variable x instead of by using one of the automatic proof methods. LP creates two subgoals for the proof by induction, a basis subgoal for the generator {} of sort S and an induction subgoal for the generator insert; it also formulates an induction hypothesis that can be used in the proof of the induction subgoal. 
Creating subgoals for proof by structural induction on `x'
Basis subgoal:
  Subgoal 1: e \in {} /\ {} \subseteq y => e \in y
Induction constant: xc
Induction hypothesis:
  setTheoremsInductHyp.1: e \in xc /\ xc \subseteq y => e \in y
Induction subgoal:
  Subgoal 2: e \in insert(e1, xc) /\ insert(e1, xc) \subseteq y => e \in y
LP proves the basis subgoal automatically by rewriting the term e \in {} to false, but it needs further guidance to prove the induction subgoal.

A proof technique for use with implications

LP uses the automatic => proof technique to create a subgoal for the induction step: 
Creating subgoals for proof of =>
New constants: e1c, ec, yc
Hypothesis:
  setTheoremsImpliesHyp.1:
     (ec = e1c \/ ec \in xc) /\ e1c \in yc /\ xc \subseteq yc
Subgoal:
  ec \in yc
The hypothesis for this subgoal is the result of reducing the hypothesis of the implication in the induction subgoal, after replacing its variables by new constants.

A proof by cases

The user must issue two more commands to finish the proof. The first directs LP to divide the proof into two cases, depending on whether the formula ec = e1c is true or not. 
Creating subgoals for proof by cases 
Case hypotheses:
  setTheoremsCaseHyp.1.1: ec = e1c
  setTheoremsCaseHyp.1.2: ~(ec = e1c)
Same subgoal for all cases:
  ec \in yc
LP finishes the first case by using the case hypothesis to rewrite the subterm ec of the subgoal ec \in yc to e1c; then it rewrites e1c \in yc to true using the second conjunct of the implication hypothesis.

In the second case, LP uses the case hypothesis and its hardwired rules to rewrite the first conjunct of the implication hypothesis to ec \in xc, at which point it gets stuck. The complete command directs LP to use what it knows to finish the proof by deriving a few critical-pair equations. First, LP derives xc \subseteq y => ec \in y as critical pair between ec \in xc and the induction hypothesis . Then it obtains ec \in yc as a critical pair between this fact and the last conjunct of the implication hypothesis. This finishes the proof by cases, the proof of the implication for the induction step of the conjecture, and the proof of the conjecture itself.

Two more theorems about subset

Similar techniques can be used to prove two more basic theorems about subset. In the first, the automatic => proof technique introduces xc = yc as a subgoal. To finish the proof, the user proves a lemma (using the <=> technique) suggested by the principle of extensionality. 
prove x \subseteq y /\ y \subseteq x => x = y
    prove e \in xc <=> e \in yc by <=>
        complete
        complete
    instantiate x by xc, y by yc in extensionality
qed
In the second, LP fills in all the details in a proof by induction without requiring further guidance from the user. 
prove (x \union y) \subseteq z <=> x \subseteq z /\ y \subseteq z by induction on x
qed

 

Sample proofs: an alternate induction rule

In order to prove a final theorem about subsets, x \subseteq x, it helps to use a different induction principle than the one we asserted as an axiom. We can prove that induction rule as follows: 
prove sort S generated by {}, {__}, \union
    resume by induction
      set name lemma
      critical-pairs *GenHyp with *GenHyp
      critical-pairs *InductHyp with lemma
qed
LP formulates an appropriate subgoal for the proof of this conjecture, together with additional hypotheses to be used in the proof, using a new operator isGenerated: 
Creating subgoals for proof of induction rule
Induction subgoal hypotheses:
  setTheoremsGenHyp.1: isGenerated({})
  setTheoremsGenHyp.2: isGenerated({e})
  setTheoremsGenHyp.3:
     isGenerated(s) /\ isGenerated(s1) => isGenerated(s \union s1)
Induction subgoal:
  isGenerated(s)
The user then directs LP to attempt to prove isGenerated(s) by induction (on s) using the asserted induction rule. LP proves the basis subgoal automatically using the hypothesis isGenerated({}). The user guides the proof of the induction subgoal by causing LP to compute critical pairs. The first critical-pairs command causes LP to derive 
lemma.1: isGenerated(s) => isGenerated(insert(e, s))
as a critical pair between the second and third isGenerated hypotheses. The second critical-pairs command causes LP to derive the induction subgoal, isGenerated(insert(e, sc)), as a critical pair between this lemma and the induction hypothesis. This finishes the proof of the induction rule.

 

Sample proofs: two final theorems about subset

The new induction rule, setTheorems.9, helps us prove the following theorem about subsets: 
prove x \subseteq (x \union y) by induction on x using setTheorems
qed
The prove command directs LP to use the induction rule just proved to formulate subgoals for the proof by induction using the generators {}, {__}, and \union instead of the generators {} and insert: 
Creating subgoals for proof by structural induction on `x'
Basis subgoals:
  Subgoal 1: {} \subseteq ({} \union y)
  Subgoal 2: {e} \subseteq ({e} \union y)
Induction constants: xc, xc1
Induction hypotheses:
  setTheoremsInductHyp.1: xc \subseteq (xc \union y)
  setTheoremsInductHyp.2: xc1 \subseteq (xc1 \union y)
Induction subgoal:
  Subgoal 3: (xc \union xc1) \subseteq (xc1 \union xc \union y)
LP establishes all three subgoals automatically.

Finally, we prove the last theorem by directing LP to compute a critical pair between the theorem just established and an earlier theorem, x \union {} = x. 

prove x \subseteq x
  critical-pairs setTheorems with setTheorems
qed

 

Sample proofs: how to guide a proof

Here are some things to try when LP and/or you get stuck trying to prove a conjecture.

 

Notational conventions

See:

 

Syntax descriptions

The syntax of LP is described using equations of the form 
<term> ::= <simpleId> | <simpleId> "(" <term>+, ")"
that are interpreted according to the following conventions to mean that a <term> is either a simple identifier or a simple identifier followed by a parenthesized list of terms separated by commas.
chars or "chars"
A terminal symbol
<chars>
A construct defined by a syntax equation
e f
An e followed by (whitespace and) an f
e | f
An e or an f
e ~ f
An e that is not an f
(e)
An e as a syntactic unit, as in (e | f) e. Without parentheses, e | f e is interpreted as e | (f e).
[e]
An optional e
e* or e*, or e*[,]
Zero or more e's, separated respectively by nothing, commas, or optional commas.
e+ or e+, or e+[,]
One or more e's, separated respectively by nothing, commas, or optional commas.

 

Symbols

LP divides its input into a sequence of symbols (also known as tokens) of the following kinds.

Simple identifiers

A <simpleId> is a string of letters, digits, apostrophes, and underscores. Exceptions: a <simpleId> cannot consist of an underscore or an apostrophe alone, and it cannot contain two adjacent underscores. Examples: Nat, 10, x', a_1.

A <number> is a <simpleId> consisting entirely of digits. See also keyword.

Operator identifiers

An <opId> is a string of operator characters, that is, characters chosen from among "!#$&*+-./<=>?@^|~", or it is the special symbol "/\". Exception: The symbol -> is not an <opId>. Examples: +, ~=, <=>.

Escaped identifiers

An <escapedId> consists of the escape character "\" alone or the escape character followed by a simple identifier, an operator character, an underscore, another escape character, or a punctuation mark. Examples: \in, \-, \_, \\, \(.

Punctuation marks

Each of the characters in ":,;()[]{}%" is a separate token, unless it is immediately preceded by the escape character. The marker symbol "__" is also treated as a punctuation mark.

Whitespace

A space, tab, or newline terminates the preceding token and is otherwise ignored. Likewise, all characters from an unescaped percent sign through the following newline are treated as whitespace. See the comment command.

Illegal characters

The characters """ and "`", as well as all control characters other than whitespace, are reserved for future use. They should not appear in LP scripts except within comments.

Strings

In certain contexts, LP reads its input without dividing it into tokens. A <string> is an arbitrary sequence of characters other than newlines. A <blank-free-string> is a <string> that does not contain any whitespace.

 

Keywords

The keywords by, else, if, in, then, when, and yield cannot be used as identifiers for sorts, variables, or operators.

The keywords to and with cannot be used as names for facts, or as components of a name pattern.

LP reserves other words (ac, commutative, depth, on, sort, using and well) in certain contexts within facts and conjectures, but does not prohibit their use as identifiers.

 

Command summary

LP is a command-driven system. Commands can be entered in upper, lower, or mixed case. They, and some of their arguments, can be abbreviated by unambiguous prefixes of their hyphen-separated components. LP prompts users for any missing arguments that it requires to execute a command. The syntax of each command is illustrated and described more fully in the description for that command.

Commands for creating axioms and facts

assert <assertion>+; [ ; ]
Assert axioms
declare operators <opdec>+[,]
Declare operators
declare sorts <sort>+,
Declare sorts
declare variables <vardec>+[,]
Declare variables
make <fact-status> ( <names> | conjecture )
Change the activity or immunity of facts or conjecture

Forward inference commands

apply <names> to <names>
Apply the named deduction rules to the named facts
complete
Run the Knuth-Bendix completion procedure
critical-pairs <names> with <names>
Find critical pair equations between each rewrite rule in the first named set and each in the second
fix <variable> as <term> in <names>
Eliminate one existential quantifier in the named facts, replacing the quantified variable by a term
instantiate ( <variable> by <term> )+, in <names>
Instantiate variables and/or eliminate universal quantifiers in the named facts, replacing the free and quantified variables by the terms
normalize <names> [ with [ reversed ] <names> ]
Normalize the named facts using the (reversals of the) hardwired and named rewrite rules
rewrite <names> [ with [ reversed ] <names> ]
Rewrite some subterm of each named fact using a hardwired or (the reversal of) a named rewrite rule

Backward inference commands

apply <names> to conjecture
Attempt to prove the current conjecture using the named deduction rules
cancel [ all | lemma ]
Cancel the current conjecture [and others]
normalize conjecture [ with <names> ]
Normalize the current conjecture using all hardwired and named rewrite rules
prove <conjecture> [ by <proof-method> ]
Attempt to prove the conjecture using <proof-method>
qed
Check that all conjectures have been proved
resume [ by <proof-method> ]
Resume work on the current conjecture using <proof-method>
rewrite conjecture [ with [ reversed ] <names> ]
Rewrite some subterm of the current conjecture using some hardwired or named rewrite rule
<>
Confirm the start of a subgoal in a proof
[]
Confirm the conclusion of a step in proof

Commands for user interaction

clear
Discard all information except global settings
delete <names>
Delete the named facts
define-class $<class> <names>
Define an abbreviation for <names>
display [ <information-type> ] [ <names> ]
Print information about the named facts
execute <file>
Execute commands from <file>.lp
execute-silently <file>
Same as execute, but suppressing all output
forget [ pairs ]
Discard information to save space
freeze <file>
Save the state of LP in <file>.lpfrz
help <topic>
Print help about the topics
history [ <number> | all ]
Print a history of [the <number> most recent] commands
pop-settings
Restore the values of local LP settings
push-settings
Remember the values of local LP settings
quit, q
Exit from LP
set
Print the current values of all LP settings
set <setting-name>
Print the current value of a setting and prompt for a new value
set <setting-name> <setting-value>
Change the value of a setting
show normal-form <term>
Display the reduction of a term to normal form
show unifiers <term>, <term>
Display all unifiers of two terms
statistics [ <statistics-option> ]
Print statistics on runtime, storage, and rule usage
stop
Stop execution of command files
thaw <file>
Restore a frozen state from <file>.lpfrz
unset [ <setting> | all ]
Reset setting to its default value
version
Display information about the current version of LP
write <file> [ <names> ]
Write the registry and the named facts to <file>.lp
% <comment>
Record a comment in the log and/or script file

Commands to control ordering

order [ <names> ]
Orient the named formulas into rewrite rules
register <ordering-constraints>
Provide constraints for orienting formulas
unorder [ <names> ]
Turn the named rewrite rules back into formulas
unregister <ordering-information>
Cancel the constraints for orienting formulas

 

Command arguments

Many commands take one or more arguments. If you know how to use a command, you can type its arguments on the same line as the command. If you don't, LP will prompt you for the arguments. For example, you can type an entire command 
set display-mode
in response to LP's command prompt, or you can type an abbreviation of the command without any arguments and await a further prompt: 
LP1: set display

The current display-mode is `unambiguous'.

New display-mode:
In response to this prompt, you can type

Commands that require a possibly lengthy argument allow you to enter it on more than one line. To do this, don't type the argument on the command line; instead, type it on the following lines, terminating your input with a line consisting of two periods (..). For example, 

LP1: declare sort Nat

LP2: declare operators
Please enter operator declarations, terminated with a `..' line, or `?' for
help:
0: -> Nat
s: Nat -> Nat
..
If you need help in the middle of typing a lengthy argument, type a question mark on a line by itself.

 

Abbreviations for commands

LP allows users to abbreviate a command with an unambiguous prefix of that command. For example, the declare command can be abbreviated to dec, but not to de because de is also a prefix of the delete command.

LP also allows users to abbreviate certain command arguments with unambiguous prefixes. When the argument can be a hyphenated word, it is enough to supply unambiguous prefixes of the hyphenated components. Examples: 

Command                              Abbreviation
-------                              ------------
declare operators 0, 1: -> Nat       dec op 0, 1: -> Nat
display rewrite-rules                dis r-r
When an argument to a command can contain reserved words (such as formulas) and names of facts, abbreviations used for reserved words must not conflict with any name-prefix established by the set command. For example, disp form is a legal abbreviation for the command display formulas unless the user has previously entered the command set name form, in which case LP interprets disp form as a request to display all facts whose name begins with the prefix form rather than to display all facts that are formulas.

 

Interrupting LP

Often one wants to interrupt an execute, order, critical-pairs, or complete command (e.g., to change the registry, to display the system, to alter the trace-level, or to freeze the system). This can be done by typing ^G (hold down the control key and type g), which will return the user to the LP command level (it may take several seconds for this to happen). The complete and order commands can be issued again to resume their execution.

 

Logical syntax and semantics

LP is a proof assistant for multisorted first-order logic. Except for the fact that it provides a rich set of notations for functions, LP is based on the syntax and semantics for first-order logic found in many textbooks. For a description of this syntax and semantics, see:

 

Sorts

A sort is a symbol that represents a non-empty set of objects. In LP, distinct sorts represent disjoint sets of objects. Sorts can be simple or compound. At present, LP accords no special treatment to compound sorts.

Syntax

<sort>          ::= <simple-sort> | <compound-sort>
<simple-sort>   ::= <simpleId>
<compound-sort> ::= <simpleId> "[" <sort>+, "]"

Examples

Nat
Set[Nat]
Map[Set[A],A]

Usage

LP automatically declares the sort Bool and treats it as representing a set containing two objects, true and false. LP also automatically declares several logical operators for this sort.

All sorts other than Bool must be declared in a declare sorts command. Except for Bool and bool, which denote the same sort, case is significant in sort identifiers. Thus Nat and nat are different sorts.

Since distinct sorts represent disjoint sets of objects, users who want to consider one ``sort'' (e.g., Nat) as a subset of another (e.g., Int) must resort to one of two devices. They can define the larger as a sort and the smaller by means of a unary predicate (e.g., isNat:Int->Bool). Alternatively, they can define both as sorts and introduce a mapping from one into the other (e.g., asInt:Nat->Int).

 

Variables

A variable is a symbol that represents an arbitrary element of some sort. A variable can be an unqualified variable identifier or a variable identifier qualified by a sort.

Syntax

<variable>   ::= <variableId> [ : <sort> ]
<variableId> ::= <simpleId>

Examples

x
x:Int
committee: Set[Person]

Usage

All variables must be declared in a declare variables command. Case is significant in variable identifiers. Thus x and X are different variables.

The same <variableId> can be overloaded to name two different variables, that is, two variables with different sorts. It can also be used to name a variable and an operator, provided the operator is not a constant of the same sort. LP uses context to disambiguate overloaded identifiers.

At times (e.g., when computing critical pairs or when proving an induction rule), LP creates variables, the identifiers for which consist of the first letter of the sort of the variable, followed by digits if necessary to avoid conflicts with constants and with other variables in the same term or formula.

 

Operators

An operator is a symbol that represents a total function. The signature of the operator specifies the domain and range of the function. Operators can be used with functional, infix, prefix, postfix, bracketed, and conditional notations.

Syntax

<operator>     ::= <opForm> [ : <signature> ]
<opForm>       ::= <functionId> | <simpleOpForm> | <bracketedOp> | <ifOp>
<functionId>   ::= <simpleId>
<simpleOpForm> ::= [ __ ] <simpleOp> [ __ ] | [ __ ] . <simpleId>
<simpleOp>     ::= <opId> | <escapedId>
<bracketedOp>  ::= [ __ ] <openSym> __*, <closeSym> [ __ ]
<openSym>      ::= { | "[" | \( | \<
<closeSym>     ::= } | "]" | \) | \>
<ifOp>         ::= if __ then __ else __
Note: All markers (__) may be omitted from a <simpleOpForm> when there is exactly one declared operator (with the indicated signature) that can be formed by adding some number of markers to the <simpleOpForm>.

Examples

<functionId>       f          0          gcd
<simpleOpForm>     -__        __<=>__    __\in__    __\Post    __.first 
<simpleOp>         -            <=>        \in        \Post
<bracketedOp>      __[__]     {}

Usage

LP automatically declares certain logical, equality, and conditional operators. All other operators must appear in a declare operators command. Case is significant in operator identifiers. Thus f and F are different operators, as are \in and \In.

Identifiers for most operators can be overloaded, that is, they can be used to represent operators with different signatures or with markers in different places. LP uses context to disambiguate overloaded identifiers.

The arity of an operator is the number of its arguments, that is, the number of sorts in its domain. A unary operator has arity 1, a binary operator has arity 2, and a constant has arity 0.

See also

 

Signatures

The signature of an operator specifies its domain and range sorts.

Syntax

<signature> ::= <domain> -> <range>
<domain>    ::= <sort>*,
<range>     ::= <sort>

Examples

->Nat
Signature for a nullary operator (constant) of sort Nat

Bool->Bool
Signature for a unary operator from sort Bool to sort Bool

Nat,Nat->Nat
Signature for a binary operator from sort Nat to sort Nat

Element,Set->Set
Signature for a binary operator from sorts Element and Set to sort Set

Usage

Signatures appear in declarations and qualifications for operators.

 

Constants

A constant is a 0-ary operator. An identifier for a constant can be either a <simpleId> (e.g., 0 and c) or a bracketed operator (e.g., {} and []).

The same identifier can be overloaded to name two different constants, that is, two constants with different sorts. A <simpleId> can also be used to name a variable and a constant, provided the variable does not have the same sort as the constant.

When LP formulates hypotheses for use in proving subgoals in a proof, it generally replaces all free variables in the hypotheses by constants. LP creates identifiers for these constants by appending the letter c and, if necessary, further digits to obtain an identifier that is not already in use. Thus LP may replace the variable x by the constants xc, xc1, ...

 

Equality operators

LP automatically declares an equality operator = and an inequality operator ~= with signature S,S:->Bool for each sort S. These operators have the standard interpretation: two objects of some sort S are equal if and only if they are identical.

Operationally, LP uses equational term-rewriting to reduce a term t to a normal form t' such that the formula t = t' is true. For this purpose, LP:

 

Logical operators

Syntax

LP automatically declares the sort Bool and the following logical operators.
true
A constant denoting the value true of sort Bool.
false
A constant denoting the value false of sort Bool.
~
A prefix operator, pronounced ``not'', denoting negation.
/\
An infix operator, pronounced ``and'', denoting conjunction.
\/
An infix operator, pronounced ``or'', denoting disjunction.
=>
An infix operator, pronounced ``implies'', denoting implication.
<=>
An infix operator, pronounced ``if and only if'', denoting equivalence. The operator <=> is a synonym for the equality operator =:Bool,Bool->Bool; it differs from = only in that it binds less tightly during parsing.

Semantics

LP treats /\, \/, and <=> as associative-commutative operators.

The meaning of the logical operators is given by the following hardwired rewrite rules. 

~true      -> false               true => p   -> p
~false     -> true                false => p  -> true
                                  p => true   -> true
p /\ true  -> p                   p => false  -> ~p
p /\ false -> false  
             
p \/ true  -> true                p <=> false -> ~p
p \/ false -> p                   p <=> true  -> p
LP uses these rewrite rules, together with the following, to simplify terms containing logical operators. 
~(~p)      -> p                   p => p      -> true
                                  p => ~p     -> ~p
p /\ p     -> p                   ~p => p     -> p
p /\ ~p    -> false
                                  p <=> p     -> true
p \/ p     -> p                   p <=> ~p    -> false
p \/ ~p    -> true                ~p <=> ~q   -> p <=> q
These rewrite rules are not sufficient to reduce all boolean tautologies to true. There are sets of rewrite rules that are complete in this sense, but they require exponential time and space, and they can expand rather than simplify expressions that do not reduce to true or false. Hence they are not hardwired into LP. Users wishing to use such a set can execute the file ~lp/boolequiv.lp or the file ~lp/boolxor.lp.

To assist in orienting formulas into rewrite rules, LP places true and false at the bottom of the registry, and it registers /\, \/, and <=> as having multiset status.

See also

 

Conditional operators

LP automatically declares a conditional operator if__then__else__ with signature Bool,S,S->S for each sort S. The meaning of this operator is given by the following two hardwired rewrite rules. 
if true then x else y  -> x
if false then x else y -> y
LP several additional hardwired rewrite rules to simplify terms containing conditional operators. It always uses the following two rules: 
if x then y else y -> y
if ~x then y else z -> if x then z else y
Unless the hardwired-usage setting dictates otherwise, it also uses the following rewrite rules: 
if x then true else y  -> x \/ y
if x then false else y -> ~x /\ y
if x then y else true  -> x => y
if x then y else false -> x /\ y
Likewise, unless the hardwired-usage setting dictates otherwise, LP uses the if-simplification metarule 
if t1 then t2[t1] else t3[t1] -> if t1 then t2[true] else t3[false]
to reduce terms when t1 occurs as a subterm of t2 or t3; here t2[true] is the result of substituting true for every occurrence of t1 as a subterm of t2, and t3[false] is defined similarly.

See also

 

Bracketed operators

LP allows users to employ bracketed notations for operators. These notations consist of opening and closing symbols interspersed with arguments (in terms) or markers (in declarations). LP recognizes the following opening and closing symbols: For example, the declarations 
declare operators
  {}:                         -> Set
  {__}:      Nat              -> Set
  __[__]:    Array, Nat       -> Nat
  __[__,__]: Matrix, Nat, Nat -> Nat
  [__]__:    Nat, Matrix      -> Array
  ..
enable the following notations:

 

Functional operators

LP allows users to declare symbols for use in ordinary functional notations in terms. A function identifier, or <functionId>, is just a simple identifier, that is, a <simpleId>. It can be used as a constant (e.g., 0) or as an operator that takes a parenthesized list of arguments (e.g., gcd(x, y)).

 

Infix, prefix, and postfix operators

LP allows users to declare symbols that can be used for infix, postfix, and prefix notations. Users can declare a simple operator (i.e., a <simpleOp>) for such use by decorating it with one or two markers (__) to indicate the location(s) of its arguments. For example, the declarations 
declare operators 
  __+__, __\mod__: Nat, Nat -> Nat   % infix operators
  -__:             Nat      -> Nat   % prefix operator
  __!:             Nat      -> Nat   % postfix operator
  ..
allow the use of infix (e.g., (x + 1) \mod n), prefix (e.g., ~p and -x), and postfix (e.g., 3!) notations. Users can also declare a selection operator for use in postfix notations. For example, the declaration 
declare operator __.first: Queue -> Element
allows the use of postfix notations such as q.first. See operator.

 

Quantifiers

Terms and formulas in LP can contain existential and universal first-order quantifiers. Examples: 
\A x \E y (x < y)
x < y => \E z (x < z /\ z < y)
The existential quantifier \E x is pronounced ``there exists an x''. The universal quantifier \A x is pronounced ``for all x''.

Syntax

<quantifier>    ::= <quantifierSym> <variable>
<quantifierSym> ::= \A | \E

Examples

\A x
\E i: Nat

Usage

All quantified variables must have been declared previously in a declare variables command.

The standard quantifier scope rules (from first-order logic) apply within terms and formulas. The scope of the leading quantifier in the terms \A x t and \E x t is the term t. An occurrence of a variable in a term is bound if it is in the scope of a quantifier over that variable; otherwise it is free. The free variables in a formula, rewrite rule, or deduction rule are understood to be quantified universally. LP suppresses the display of leading universal quantifiers.

LP uses the following hardwired rewrite rules to reduce terms containing quantifiers. 

\A x t -> t
\E x t -> t
\E x \E x1 ... xn (x = t /\ P(x))            -> \E x1 ... \E xn P(t)
\A x \A x1 ... xn (~(x = t) \/ Q(x))         -> \A x1 ... xn Q(t)
\A x \A x1 ... xn (x = t /\ P(x) => Q(x))    -> \A x1 ... xn (P(t) => Q(t))
\A x \A x1 ... xn (P(x) => ~(x = t) \/ Q(x)) -> \A x1 ... xn (P(t) => Q(t))
Here P(x) and Q(x) are arbitrary terms, t is a term with no free occurrences of x, and P(t) and Q(t) are the results of substituting t for x in P(x) and Q(x) with appropriate changes of bound variables to prevent a quantifier in P or Q from capturing a variable in t.

The fix and instantiate commands, together with the generalization and specialization proof methods, enable users to eliminate quantifiers from facts and conjectures.

See also prenex form.

 

Prenex form

Every formula is logically equivalent to a prenex formula, that is, to a formula consisting of a string of quantifiers applied to a quantifier-free formula. For example, the following formulas are logically equivalent: 
\E w \A x P(w, x) => \A y \E z P(z, y)
\A w \A y \E x \E z (P(w, x) => P(z, y))
\A w \A y \E x (P(w, x) => P(x, y))
Every quantifier in a formula can be classified as a prenex-universal, a prenex-existential quantifier, or neither depending on whether it corresponds to a universal (\A) quantifier, an existential (\E) quantifier, or more than one quantifier in a systematically derived logically equivalent prenex formula. The leading quantifiers in \A x P and \E x P are prenex-universal and prenex-existential quantifiers, respectively. If a quantifier is prenex-universal (prenex-existential) in P, then it is the same in P /\ Q, P \/ Q, Q => P, \A y P, and \E y P; it is prenex-existential (prenex-universal) in ~P and P => Q; and it is neither in any other formula, e.g., in P <=> Q.

Formulas can be transformed systematically into prenex formulas using changes of bound variables and the following logical validities. 

\A x P         <=>  P                            (x not free in P)
\E x P         <=>  P                            (x not free in P)
\A x ~P        <=>  ~\E x P
\E x ~P        <=>  ~\A x P
\A x (P /\ Q)  <=>  \A x P /\ \A x Q
\E x (P /\ Q)  <=>  \E x P /\ Q                  (x not free in Q)
\A x (P \/ Q)  <=>  \A x P \/ Q                  (x not free in Q)
\E x (P \/ Q)  <=>  \E x P \/ \E x Q
\A x (P => Q)  <=>  \E x P) => Q                 (x not free in Q)
\A x (P => Q)  <=>  P => \A x Q                  (x not free in P) 
\E x (P => Q)  <=>  \A x P => \E x Q
F(\A x P)      <=>  (F(true) /\ \A x P) 
                       \/ (F(false) /\ ~\A x P)

The instantiate and fix commands enable users to eliminate certain prenex-universal and prenex-existential quantifiers from facts. The generalization and specialization proof methods provide the corresponding functionality for conjectures.

 

Capturing variables

It is generally the case that, for any formula P(x) involving a variable x and any term t, the formula P(t) (i.e., the result of substituting t for each free occurrence of x in P) is a logical consequence of P(x). However, this may not be the case if the substitution captures some free variable in t, that is, if t contains a free variable that becomes bound by some quantifier in P. For example, if P(x) is \E y (x ~= y), then P(y) and P(s(y)) are not logical consequences of P(x) because the free variable y in the terms y and s(y) is captured by the quantifier in P.

For this reason, LP automatically changes bound variables to avoid captures during rewriting, in response to the fix and instantiate commands, and in response to the generalization and specialization proof methods.

 

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:

 

Overloaded identifiers

LP allows users to overload identifiers for variables and operators. For example, LP allows the simple identifier s to be used both as a function s:Nat->Nat and as a variable s:Set, and it allows the operator identifier - to be used both as a prefix operator and as an infix operator. LP automatically overloads the predefined equality and conditional operators (=, ~=, and if__then__else__), once for each declared sort. There are only two restrictions on overloading: LP disambiguates user input by using context to associate each identifier with a previous declaration. When context permits more than one association, users must supply additional annotations to resolve the ambiguity.

Disambiguating terms

Users can resolve potential ambiguities in terms by qualifying selected subterms with their sorts. For example, given the declarations 
declare variables x, y, z: Bool, x, y, w: Nat
the terms x = z and x = w are unambiguous, but the term x = y is ambiguous. It can be disambiguated in several ways, for example, as x:Nat = y or as x = y:Bool. Given the additional declarations 
declare operators f:Nat->Nat, f:Nat->Bool, f:Bool->Bool
the term f(z) is unambiguous, but the term f(w) needs to be disambiguated as either f(w):Nat or f(w):Bool, and the term f(x) needs to be disambiguated as one of f(x:Bool), f(x:Nat):Nat, or f(x:Nat):Bool.

Another potential ambiguity in terms arises from the treatment LP accords to the period symbol (.). For example, given the declarations 

declare operators
  1, min:                       -> Nat
  a:                            -> Array
  __.__:             Array, Nat -> Nat
  __ .size, __ .min: Array      -> Nat
  ..
the terms a.size and a.1 are unambiguous, but a.min could represent an application of either the infix operator . or the postfix operator .min. In such cases, LP disambiguates a.min as containing a postfix operator; users who want . to refer to the infix operator can write a.(min).

Disambiguating operators outside of terms

Users can resolve an ambiguous operator identifier by qualifying it with its signature or by decorating it with one or two markers (__) to indicate whether it is an infix, postfix, or prefix operator.

See also

 

Precedence

Parsing

When parsing a term, LP binds some operators more tightly than others, thereby reducing the need for parentheses. The operators in the following list bind increasingly tightly: Parentheses are required elsewhere to specify associativity, except that terms such as t1 + t2 + ... + tn, which involve a sequence of terms separated by a single infix identifier (other than =>, =, and ~=), do not need parentheses and are associated to the left.

Quantifiers bind more tightly than all operators.

Examples

Unparenthesized version    Interpretation
----------------------     --------------
a < b + c                  Error
p /\ q \/ r                Error
p => q => r                Error
x - y - z                  (x - y) - z
a = b + c => b < s(a)      (a = (b + c)) => (b < s(a))
a.b.c!                     ((a.b).c)!
~p /\ ~x.pre               (~p) /\ (~(x.pre))
\E x (x < c) => c > 0      (\E x (x < c)) => (c > 0)
\A x \E y x < y            (\A x \E y x) < y

Ordering

When orienting formulas into rewrite rules, LP sometimes uses a partial ordering on operators that is known in the literature as a precedence relation. See register.

 

Formulas

A formula is boolean-valued term.

Syntax

<formula> ::= <term>
Restriction: the sort of the <term> must be Bool.

Examples

x + s(y) = s(x + y)
x | y <=> \E z (y = x * z)
x < y \/ x = y \/ y < x
x < y => \E z (x < z /\ z < y)

Usage

Users can assert formulas, prove them, or derive them from other formulas by forward inference.

Operationally, LP uses formulas by orienting them (if possible) into a terminating set of rewrite rules. LP also automatically reduces all nonimmune formulas to normal form.

LP automatically rewrites formulas of the form ~p to p = false and formulas of the form ~p = false to p. Furthermore, it uses the following hardwired deduction rules to derive new formulas from existing formulas and rewrite rules. 

lp_and_is_true:  when p /\ q    yield  p, q
lp_or_is_false:  when ~(p \/ q) yield  ~p, ~q
LP uses the names of these deduction rules when it reports their application, but they cannot be entered by the user when naming objects.

To display the formulas that LP has not converted into rewrite rules, type display formulas (or dis fo for short).

 

Equations

An equation is a formula that consists of a pair of terms separated by an equality operator.

Syntax

<equation> ::= <term> (= | <=>) <term>
Restriction: The two <term>s in an equation must have the same sort. This sort must be Bool if the equality operator is <=>.

Examples

x + 0 = x
x <= y <=> x < y \/ x = y
x | y <=> \E z (y = x*z)

Usage

LP treats equations in the same manner as it treats formulas. Indeed, any formula is logically equivalent to an equation: F is logically equivalent to F <=> true.

 

Operational syntax and semantics

The basis for each proof in LP is a logical system that contains a collection of facts (axioms, hypotheses, and previously proved theorems) available for use in that proof. There is a separate logical system, known as a proof context, for the proof of each conjecture and subgoal.

The facts in a logical system have both semantic content (expressed by formulas in first-order logic) and operational content. For more information about this operational content, see:

 

Inconsistency

An inconsistency is a formula that is logically false.

LP automatically recognizes the formula x ~= t, where t is a term not involving the variable x, as inconsistent. Thus, LP rules out empty sorts. It also recognizes the formulas false and b = t, where t is a term not involving the boolean variable b, as inconsistent. Thus, the boolean sort contains two distinct values.

If an inconsistency arises during a proof by contradiction, that proof succeeds. If it arises during a proof by cases, the current case is deemed impossible.

 

Rewrite rules

A rewrite rule is an operational form for a formula. LP uses rewrite rules to rewrite terms to logically equivalent terms.

Syntax

<rewrite-rule> ::= <term> -> <term>
Restrictions: The two <term>s in a rewrite rule must have the same sort. The left side of the rule must not be a variable, the logical constant true, or the logical constant false. Every free variable in the right side must also occur free in left side.

Examples

x + 0 -> x
x <= y -> x < y \/ x = y
x | y -> \E z (y = x*z)
0 < 1 -> true

Usage

Users cannot assert or prove rewrite rules directly. Instead, they must assert or prove formulas, which LP then orients into rewrite rules. The logical content of a term is the equation that results from replacing -> by =.

LP maintains the invariant that all active rewrite rules have been applied to all nonimmune formulas, rewrite rules, and deduction rules in the system.

Some rewrite rules are hardwired into LP to define properties of the logical connectives, the conditional and equality operators, and the quantifiers.

The restriction that the left side of a rewrite rule not be a variable prevents ``rules'' like x -> f(x) from leading to a nonterminating rewriting sequence such as x -> f(x) -> f(f(x)) -> .... The restriction that it not be true or false preserves the meaning of those logical constants. The restriction that the right side not introduce a free variable is more technical. It prevents logically equivalent ``rules'' such as f(x) -> f(y) and f(u) -> f(v) from producing different results when applied to terms like y + f(x).

 

Operator theories

An operator theory is logically equivalent to a set of equations involving a single operator. At present, LP supports two operator theories: LP uses operator theories to circumvent problems with nonterminating rewriting systems. Because the commutative law cannot be oriented into a terminating rewrite rule, LP uses equational term-rewriting to match and unify terms modulo the ac and commutative operator theories.

Syntax

<operator-theory> ::= (ac | commutative) <operator>

Examples

ac +
commutative gcd

Usage

Users can assert or prove operator theories.

LP hardwires the logical connectives /\, \/, and <=> as associative-commutative operators. It hardwires the equality operator =:S,S->Bool as a commutative operator when the sort S is not Bool.

The fact ac op normalizes the fact commutative op to true.

To display the operator theories in LP's logical system, type display operator-theories (or disp o-t for short).

 

Induction rules

An induction rule is logically equivalent to an infinite set of formulas, which justify the use of proofs by induction.

Syntax

<induction-rule> ::= sort <sort> generated [ freely ] by <operator>+,
                       | well founded <operator>

Examples

sort Nat generated freely by 0, s
sort Set generated by {}, insert
sort Set generated by {}, {__}, \U
well founded <

Usage

Users can assert or prove induction rules.

Assertions like sort Nat generated by 0, s specify sets of generators for use in proofs by structural induction. The listed operators (e.g, 0 and s) must have the named sort (e.g., Nat) as their range. If none of the domain sorts of an operator is the same as its range sort, the operator is a basis generator (e.g., 0); otherwise, it is an inductive generator (e.g, s). Structural induction rules are logically equivalent to infinite sets of first-order formulas of the form 

P(0) /\ \A x (P(x) => P(s(x))) => \A x P(x)
where P is an arbitrary first-order formula.

The use of freely supplements a structural induction rule with a set of formulas asserting that the named operators are one-to-one and have disjoint ranges. For example, sort Nat generated freely by 0, s gives rise to the formulas s(x) = s(y) <=> x = y and 0 ~= s(x).

Assertions like well founded < specify a binary relation for use in proofs by well-founded induction. The listed operator must have a signature of the form S,S->Bool for some sort S. Well-founded induction rules are logically equivalent to infinite sets of first-order formulas of the form 

\A x (\A y (y < x => P(y)) => P(x)) => \A x P(x)
where P is an arbitrary first-order formula.

To display the induction rules that LP currently has available for use, type display induction-rules (or disp i-r for short).

 

Deduction rules

A deduction rule is logically equivalent to a single formula in multisorted first-order logic. That formula has the form of a logical implication. LP uses deduction rules to derive consequences from other formulas and rewrite rules.

Syntax

<deduction-rule> ::= when <hypothesis>+, yield <conclusion>+,
<hypothesis>     ::= <formula>
<conclusion>     ::= <formula>

Examples

when x < y, y < z yield x < z
when p /\ q yield p, q
when \A e (e \in s1 <=> e \in s2) yield s1 = s2

Usage

Users can assert or prove deduction rules. A deduction rule is logically equivalent to the formula obtained by having the conjunction of its hypotheses imply the conjunction of its conclusions. Thus the first example is logically equivalent to the formula x < y /\ y < z => x < z.

A deduction rule can be applied to a formula or rewrite rule if there is a substitution that matches the first hypothesis of the deduction rule to the formula or rewrite rule. The result of applying a deduction rule with one hypothesis is the set of formulas obtained by applying the substitution(s) that matched its hypothesis to each of its conclusions. For example, applying the second example to 1 < f(x) /\ f(x) < 2 yields two formulas, 1 < f(x) and f(x) < 2. Likewise, applying the third example to x \in s <=> x \in (s \U s) yields the formula s = s \U s.

The result of applying a deduction rule with more than one hypothesis is the set of deduction rules obtained by deleting its first hypothesis (i.e., the one that was matched) and applying the substitution(s) that matched this hypothesis to the remainder of the deduction rule. For example, applying the first example to the formula a < b yields the deduction rule 

when b < z yield a < z
On the other hand, applying the logically equivalent deduction rule 
when y < z, x < y yield x < z
to the same formula yields a different result, namely, 
when x < a yield x < b

When applying deduction rules, LP produces the strongest valid conclusions by changing, when appropriate, variables in the conclusions that do not occur freely in the hypotheses. For example, applying the deduction rule 

when P(x) yield Q(x, y)
to the formula P(f(y)) yields the result Q(f(y), y1) and not the weaker result Q(f(y), y).

The results of applying a deduction rule are given the default activity and immunity, as established by the set command.

LP maintains the invariant that all active deduction rules have been applied to all nonimmune formulas and rewrite rules in the system.

To display the deduction rules that LP currently has available for use, type display deduction-rules (or disp d-r for short).

See formulas for a list of deduction rules that are hardwired into LP. See also partitioned-by.

 

Partitioned by

The partitioned-by construct provides a convenient syntax for expressing the fact that two objects of a given sort are the same if they cannot be distinguished by an operator in a given list. Operationally, a <partitioned-by> is equivalent to a deduction rule.

Syntax

<partitioned-by> ::= sort <sort> partitioned by <operator>+,
Restriction: Each of the <operator>s must have <sort> in its domain.

Examples

sort Set partitioned by \in
sort Stack partitioned by isEmpty, top, pop

Usage

Users can assert or prove a <partitioned-by>, which LP automatically translates into a deduction rule. For example, LP translates the examples into the deduction rules 
when \A e (e \in s = e \in s1) yield s = s1
when isEmpty(s) = isEmpty(s1), top(s) = top(s1), pop(s) = pop(s1)
yield s = s1
In general, LP translates a statement like 
sort E partitioned by op1:E->R, op2:E,A->R, op3:E,E,A->R
into to the deduction rule 
when op1(e1) = op1(e2),
     \A a (op2(e1, a) = op2(e2, a)),
     \A a \A e3 (op3(e1, e3, a) = op3(e2, e3, a)),
     \A a \A e3 (op3(e3, e1, a) = op3(e3, e2, a))
yield e1 = e2
which uses auxiliary variables e1, e2, and e3 of sort E and a and a1 of sort A.

 

Assigning and using names

See

 

Assigning names to facts

Each fact in LP's logical system has a name consisting of an alphanumeric prefix followed by a series of numeric suffixes separated by periods.

Syntax

<name>      ::= <simpleId> <extension>*
<extension> ::= . <number>

Examples

arith.1
set.2.3

Usage

LP assigns new names to facts in response to the assert and fix commands, to critical pair equations in response to the critical-pairs and complete commands, and to conjectures in response to the prove command. These names have a single numeric <extension>, whose value increases each time a new name is required. Users can specify the name prefix for a fact in the assert command, or for a conjecture in the prove command, by writing :<simpleId>: before the fact. Otherwise the value of the name-prefix setting governs the <simpleId> used as a prefix for new names.

Normalization, ordering, unordering, and proofs preserve the names of formulas, rewrite rules, and deduction rules. LP assigns subnames (i.e., names with an additional <extension>) to instantiations of formulas, rewrite rules, and deduction rules, to the results of applying deduction rules, and to hypotheses introduced during the proof of a conjecture. The names of the results of applying a deduction rule to a formula extend the name of the deduction rule if the deduction rule has more than one hypothesis; otherwise they extend the name of the formula.

One fact is called a descendant of another (and the latter is called an ancestor of the former) if the name of the first extends, by zero or more <extension>s, the name of the second. A proper ancestor (or descendant) of a fact is an ancestor (or descendant) with a different name.

The names of the hardwired deduction rules for formulas begin with lp_. The hardwired rewrite rules for the logical connectives, the conditional and equality operators, and the quantifiers do not have names, nor do conjectures introduced as subgoals in proofs.

See also

 

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

See also <class>.

 

Name classes

A class is an expression that, when evaluated, produces a list of <name>s of facts.

Syntax

<class>          ::= <class-name> | <class-constant>
                        | <class-function> "(" <names> ")"
                        | contains-operator "(" <operator> ")"
                        | contains-variable "(" <variable> ")"
                        | copy "(" <class-name> ")"
<class-name>     ::= $ <simpleId>
<class-constant> ::= deduction-rules | formulas | induction-rules   
                       | operator-theories | rewrite-rules | active | passive 
                       | immune | nonimmune | ancestor-immune
<class-function> ::= ancestors | proper-ancestors | descendants
                       | proper-descendants | eval

Examples

$facts
contains-operator(+)
eval(* ~ $old)

Usage

The define-class command defines a <class-name> as an abbreviation for some <names>. Each <class>, other than ones beginning with copy or eval, also serves as an abbreviation for the names of facts matching a certain criterion. For example, contains-operator(+) describes the collection of all facts containing the operator +.

A <class-name> (or <class>) appearing in an argument to a command other than define-class is replaced by its definition (or evaluated) when the command is executed. Evaluation in the define-class command can be forced using one of the following operators:

copy($class)
Replaces the <class-name> $class by its current definition

eval(exp)
Replaces the <names> exp by an explicit list of the names of all facts in LP's logical system that match exp

See also

 

The assert command

The assert command adds axioms to LP's logical system.

Syntax

<assert-command> ::= assert <assertion>;+ [;]
<assertion>      ::= [:<simpleId>:] <fact>
<fact>           ::= <formula> | <deduction-rule> | <induction-rule> 
                        | <operator-theory> | <partitioned-by>

Examples

assert
  e1 \in insert(e2, s) <=> e1 = e2 \/ e1 \in s;
  when \A e (e \in s1 <=> e \in s2) yield s1 = s2;
  Set generated by {}, insert;
  ac \U;
  Set partitioned by \in
  ..

Usage

LP adds the asserted facts to its logical system. It assigns a name to each of these facts using the current name-prefix setting, unless an assertion begins with :<simpleId>:, in which case LP uses that identifier as the name-prefix for that assertion.

LP takes certain default actions when it adds assertions to its logical system.

 

The declare command

Except for certain predefined logical, equality, and conditional operators, all identifiers for sorts, variables, and operators must be declared in a declare command before any other use.

Syntax

<declare-command> ::= declare ( <sortDecs> | <varDecs> | <opDecs> )
<sortDecs>        ::= sorts <sort>+,
<varDecs>         ::= variables <varDec>+[,]
<varDec>          ::= <variableId>+, : <sort>
<opDecs>          ::= operators <opDec>+[,]
<opDec>           ::= <opForm>+, : <signature>
Restrictions: There must be at least one marker in each <opForm> that contains a <simpleOpForm>. The number of marker symbols in any <opForm> not containing a <functionId> must equal the number of sorts in the domain of the operator's signature. A period (.) can be declared as an infix operator, but not as a prefix or a postfix operator. The predefined operators cannot be overloaded with user-defined signatures.

Notes: The words sorts, operators, and variables can be abbreviated by any prefix, as well as by ops and vars.

Examples

declare sorts Nat, Set
declare variables i, j: Nat, s: Set
declare operators
  0:                     -> Nat
  s, __!:       Nat      -> Nat
  __+__, __*__: Nat, Nat -> Nat
  {}:                    -> Set
  {__}:         Nat      -> Set
  __\U__:       Set, Set -> Set
  ~__:          Set      -> Set
  ..

Usage

The declare sorts command introduces identifiers for use as sorts.

The declare variables command introduces variables with the indicated sorts.

The declare operators commands introduces operators with the indicated signatures. Marker symbols (__) in an <opForm> indicate where the arguments of the operator are placed when it is used in a term.

LP at times creates variables and operators in response to user commands. To avoid problems, it is a good idea for users to declare the identifiers they need before issuing commands (such as prove) that may cause LP to appropriate an identifier for its own use (e.g., by creating a variable s1 of sort Set and thereby preventing the user from later using s1 as a constant of sort Set).

The display symbols command produces a list of all declared identifiers.

 

The make command

The make command changes the activity or immunity of a collection of facts or of the current conjecture.

Syntax

<make_command> ::= make <fact-status> ( <names> | conjecture )
<fact-status>  ::= active | passive | immune | nonimmune | ancestor-immune
Note: The <fact-status> can be abbreviated.

Examples

make inactive rewrite-rules
make immune conjecture

Usage

LP automatically uses any rewrite rules made active by the make command to normalize terms appearing in the current conjecture or in nonimmune facts in LP's logical system. It also automatically applies any deduction rules made active by the make command.

LP automatically normalizes any rewrite rules and deduction rules made nonimmune by the make command, and it applies all active deduction rules to these deimmunized rules.

See the activity and immunity settings.

 

The order command

The order command directs LP to attempt to orient formulas into rewrite rules.

Syntax

<order-command> ::= order [ <names> ]

Examples

order
order nat

Usage

When the automatic-ordering setting is on, LP attempts to orient formulas into rewrite rules automatically. When it is off, LP orients formulas only in response to an explicit order or complete command. If no <names> are specified in an order command, LP attempts to orient all formulas in the system. If <names> are specified, LP attempts to orient only the named formulas (including any new formulas that LP generates during the ordering process, for example, as a result of applying a deduction rule to a newly reduced fact).

When a formula is an equation t1 = t2 or t1 <=> t2, LP uses the current ordering-method, if possible, to orient it into the rewrite rule t1 -> t2 or into the rewrite rule t2 -> t1. When a formula f is not an equation (i.e., when its principal operator is neither = nor <=>), LP orients it into the rewrite rule f -> true (or into the rewrite rule f1 -> false, if f has the form ~f1).

If the current ordering method is a registered or polynomial ordering, the order command also attempts to orient the formulas into a provably terminating set of rewrite rules. If the current ordering method is a brute-force ordering, the order command may orient the formulas into a nonterminating set of rewrite rules.

Users can interrupt and resume the operation of the order command.

 

Brute-force orderings

LP's brute-force ordering procedures give users complete control over the direction in which formulas are oriented into rewrite rules, but provide no guarantees about termination.

The left-to-right ordering

This ordering