1. Não usa regra de reescrita.
2. Usa foward rules.
3. Usa grule
4. Faz reason aritmético
Ex: identidades
5. Não infere: A \in \power A
6. Faz simplificações lógicas
Ex: (PREDICATE \iff true) é substituído por (PREDICATE)
Assinar:
Postar comentários (Atom)
Nenhum comentário:
Postar um comentário