LP, the Larch Prover -- Hints on formalizing axioms and conjectures

Be careful not to confuse variables and constants. If x is a variable and c is a constant, then e(x) is a stronger assertion than e(c). The first means \A x e(x). In the absence of other assertions involving c, the second only implies \E x e(x). If you don't know whether an identifier is a variable or a constant, type display symbols to find out.

Be careful about the use of free variables in formulas. The formula x = {} => subset(x, y) correctly (albeit awkwardly) expresses the fact that the empty set is a subset of any set. However, its converse, subset(x, y) => x = {}, does not express the fact that any set that is a subset of all sets must be the empty set. That fact is expressed by the equivalent formulas \A x (\A y subset(x, y) => x = {}) and \A x \E y (subset(x, y) => x = {}).

An axiom or conjecture of the form when A yield B has the same logical content as one of the form A => B, but different operational content. Given the axiomization

declare variable x: Bool
declare operators
  a: -> Bool
  f, g, h: Bool -> Bool
  ..
assert 
  when f(x) yield g(x);
  g(x) => h(x);
  f(a)
  ..

LP will automatically derive the fact g(a) from f(a) by applying the deduction rule, but it will not derive h(a) from g(a) unless it is instructed to compute critical-pairs.

A multiple-hypothesis deduction rule of the form when A, B yield C has the same logical content as a single-hypothesis rule of the form when A /\ B yield C. They differ operationally in that, if the user asserts or proves two formulas that are matched by A and B, LP will apply the multiple-hypothesis rule but not the single-hypothesis rule.