Regenerate the tau database relative to the current enabled theory
General Form: (regenerate-tau-database)
The tau database is regenerated by scanning the current logical world and re-processing every rule-generating event in it relative to the current enabled theory and current tau auto mode settings. See introduction-to-the-tau-system for background details.
This command was intended to allow the user to remove a fact from the tau
database, by regenerating the database without the fact. But as the following
Suppose, for example, that you wanted to remove a signature rule provided by some rule with name rune. You could disable rune and regenerate the database. We discuss why you might — or might not — want to do this later. But suppose you did it. Unfortunately, the database you get will not be just like the one you started with minus the signature rule. The reason is that the database you started with was generated incrementally and the current theory might have evolved. To take a simple example, your starting database might have included a rule that has been disabled since it was first added. Thus, the part of your starting database built before the disabling was constructed with the rule enabled and the part built afterwards has the rule disabled. You are unlikely to get the same database whether you enable or disable that rule now.
You might hope that the avoidance of
The reason we hope that it will not be necessary to remove tau facts is that the tau system is designed merely to be fast and benign (see Design Philosophy in introduction-to-the-tau-system). The tau system's coverage should grows monotonically with the addition of rules. According to this understanding of tau, adding a signature rule, for example, may allow tau to prove some additional goals but will not prevent it from proving goals it could prove previously. If this is understanding of tau is accurate, we see no fundamental reason to support the removal of a fact. This, of course, ignores the possibility that the user wishes to explore alternative proof strategies or measure performance.
We welcome user observations and experience on this issue.