Find all lines matching a certain wff, up to

alphabetic change of bound variables and (possibly)

alphabetic change of a given list of free variables.

Optionally, you can treat the remaining free variables

as matching any given term (as you might do if you were

asserting an axiom).

e.g. (suppose P is an abbreviation or constant):

FIND-LINE "P a" () NO finds all lines that say "P a"

FIND-LINE "P a" ("a") NO also finds "P x" and "P y"

FIND-LINE "P a" () YES finds all the above, plus

"P [COMPOSE f g]"

FIND-LINE "a x" ("x") YES finds all lines of the form

"SOME-TERM some-var"

The command format for FIND-LINE is:

<n>FIND-LINE WFF VARS META

"GWFF0" "GVARLIST" "YESNO"

The arguments have the following meaning:

WFF : Wff to look for

VARS : Free variables that may be alphabetically changed

META : Treat remaining free vars as subterms?

© 1988-99, Carnegie Mellon University.