Motivating Example

The Venezuelan car manufacturer "Sucre" has been developing a futuristic electric car, called the Quipos. The Quipos has only three digital control circuits: the Energy Control Circuit (ECQ), the Wheel Control Circuit (WCQ), and the Human Haptics Detection (HHD) circuit (don't blame me for their strange acronyms). During development one of the circuits was repeatedly sending faulty signals to the WCQ, causing it to fail, with corresponding downstream impact on the car's self-steering and automatic braking features. The engineers needed to determine which circuit was sending the faulty signals to the WCQ. The following facts were known about the signals being sent between the circuits:

Automated Theorem Proving was used to analyse this issue, and it turned out that the WCQ was sending faulty signals to itself, causing itself to fail!

Another version