Change the top connective of a formula. For example,

"cntop or" will change "A and B" into "A or B";

"cntop exists" will change "forall x P x" into "exists x P x".

The calling scheme for CHANGE-TOP is:

(CHANGE-TOP CONN GWFF)

"SYMBOL" "GWFF"

The result is of type GWFF.

The arguments have the following meaning:

CONN : Connective or Quantifier

GWFF : Wff

© 1988-99, Carnegie Mellon University.