NAIVE : FLAG-MODE

NAIVE is a mode.
Sets flags so all definitions and equalities will be rewritten,
skolemizing will be done using SK1, but equalities will be rewritten
using the Leibniz definition.
Flags are set as follows:
Flag Value in Mode Current Value
SKOLEM-DEFAULT SK1 SK1
REWRITE-DEFNS '(LAZY1) (EAGER)
REWRITE-EQUALITIES 'LEIBNIZ ALL
REMOVE-LEIBNIZ T T
MIN-QUANTIFIER-SCOPE NIL NIL
USE-RULEP NIL T
USE-SYMSIMP NIL T

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage