GWFF-PROP is an argument type.
One 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.

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage