Truth or reason maintenance systems can be used to handle inferred information about facts and derived facts.
There are various kinds of truth maintenance systems and this post concentrates on particular kind of: justification based truth maintenance system. Especially the version shipped with Stilpo is talked about. Because justification based truth maintenance system is such a long thing to type all the time, I’m using acronym JTMS instead.
JTMS deals with truths and their relations. Truth can be a premise, which are always considered to be true. It can be an assumption that might or might not be true. Sometimes assumption is based on one or more truths, in which case it has a justification. Some assumptions are marked as contradictions.
For example: “Weather is warm” is truth in this system. So is “Weather is cold”. “Wear warm clothes” is also truth. If we state “if weather is cold, wear warm clothes” we justify wearing warm clothes with cold weather and create a connection between those two things. Assuming that both “Weather is warm” and “Weather is cold” are both assumptions and not premises, JTMS can reason if “Wear warm clothes” is enabled or not, depending on the state of weather. “If weather is both warm and cold, we have a problem” is contradiction, justified by both weather states.
So far the JTMS looks just like a big bunch of if-then statements with some fancy terms thrown in the mix. What can one actually do with such a thing?
One application is using JTMS to store and detect contradictions as a part of other search algorithm or problem solver. Every time the other algorithm makes a decision, respective truth and related dependencies are stored in JTMS. If the other algorithm detects an unwanted situation, it is recorded as a contradiction. Later on when search algorithm comes to a situation where it might make the same choice again, JTMS is able to signal before the choice is actually made that it would lead into a contradiction. Moreover, it can also explain via justifications, what causes this situation be undesired. The other algorithm can then adjust and try other kind of approach. In cases where computing if a situation is good or not takes a long time, this can save quite a bit of time.
I mentioned that JTMS is able to show what causes a truth (be it contradiction or not) be enabled. This is based on the fact that each truth is either premise, explicitly enabled assumption or a derived assumption (it has a justification). Following justifications back to premises and explicitly enabled assumptions enables system to reason what could be changed in order to disable a contradiction.
Next time I’m going to dive into more code and give some more concrete examples on how JTMS works.