A truth maintenance system keeps track of why each belief is held. This example is a small assumption-based one: it records which sets of assumptions support each conclusion, and which sets support contradictory conclusions and are therefore inconsistent.
Run it in the playground · Source
A robot has two sensors and an operator who can override them. Under each combination of readings, may the robot move? And under which combinations do the conclusions contradict each other?
An environment is a set of assumptions, such as “the clear-path sensor fired”. A justification derives a belief from assumptions or from other beliefs.
environment(clear_only, [sensor_clear]).
environment(blocked_only, [sensor_blocked]).
environment(conflicting_sensors, [sensor_clear, sensor_blocked]).
environment(override_blocked, [sensor_blocked, operator_override]).
justification(j_clear_path, [assumption(sensor_clear)], clear_path).
justification(j_blocked_path, [assumption(sensor_blocked)], blocked_path).
justification(j_permit_from_clear, [clear_path], permit_go).
justification(j_forbid_from_blocked, [blocked_path], forbid_go).
justification(j_override, [assumption(operator_override), blocked_path], permit_go).
Justifications are data, so the system can report which one fired, not only what was concluded.
supported(Environment, Belief) :-
justification(_, Preconditions, Belief),
all_hold(Environment, Preconditions).
inconsistent(Environment) :-
supported(Environment, Left),
supported(Environment, Right),
contradicts(Left, Right).
A belief is supported in an environment when all preconditions of some
justification hold there. An environment is inconsistent when it supports two
beliefs that contradict each other, here permit_go and forbid_go.
eyeprolog examples/truth-maintenance-system.pl
tmsSupport(clear_only, permit_go).
tmsSupport(blocked_only, forbid_go).
tmsSupport(override_blocked, forbid_go).
tmsSupport(override_blocked, permit_go).
tmsInconsistent(conflicting_sensors).
tmsInconsistent(override_blocked).
This is a selection of the 25 answers. With both sensors firing, the system
supports both moving and not moving. With the override, it still derives
forbid_go from the blocked path, so that environment is inconsistent too.
step(inconsistent(conflicting_sensors),
rule(17),
['Environment' = conflicting_sensors, 'Left' = permit_go, 'Right' = forbid_go],
[supported(conflicting_sensors, permit_go),
supported(conflicting_sensors, forbid_go),
contradicts(permit_go, forbid_go)]).
The conflicting-sensors environment is inconsistent because it supports
permit_go, it supports forbid_go, and the two contradict each other. Each
of those uses has its own step further down in the proof.
condition('C1', resolution, ok, 81).
condition('C4', coverage, ok, 134).
condition('C5', re_decision, ok, 6).
claims(25).
verdict(checked).
All 25 claims are covered. The checker replays 81 rule and fact steps and
recomputes 6 member/2 steps, without any trusted boundary.
forbid_go, and see
whether override_blocked stays inconsistent.permit_go under each environment:
--goal 'tmsJustification(E, J, permit_go)'.Learn more in The Art of EyeProlog, Chapter 14.