Simulating reactive systems by a deduction system

Simulation by deduction is a technique in which the behavior of the simulated model is deduced by a reasoning system. A simulation system that uses this technique can explain the reasons for the simulation results and thus aid the localization of bugs. Furthermore, simulation by deduction enables symbolic simulation, i.e. simulating a scenario given only a partial description of the environment and the simulated model. This allows verifying properties of an evolving design at any stage of the design process, and thus checking the consequences of the design decisions made so far. These ideas were implemented in a system called SIP (simulation by proof), which simulates the behavior of reactive systems