A list of some of the following properties of gwffs:

ALL : true for all gwffs

FIRST-ORDER : true for first-order gwffs

SK-FIRST-ORDER : true for gwffs that are first-order after skolemizing.

HIGHER-ORDER : true for non-first-order gwffs

SK-HIGHER-ORDER : true for gwffs that are non-first-order after skolemizing.

WITH-EQUALITY : true of gwffs that contain an equality

WITH-DEFN : true of gwffs that contain a definition

PROVEN : true of gwffs that have been marked as proven in the library

UNPROVEN : true of all gwffs that aren't PROVEN

AUTO-PROOF : true of all gwffs with automatic or semi-automatic proofs.

For the first- and higher-order checks, equalities are rewritten as specified

by the flag REWRITE-EQUALITIES; if any equalities remain in the gwff after

rewriting, these are considered first-order if they are equalities between

base types.

© 1988-99, Carnegie Mellon University.