By Dominique Snyers
It's proven that theorem proving tools can result in application synthesis and set of rules implementation through the use of pairs of common sense legislation: a deductive legislation for proving the concept and a optimistic legislation for synthesizing this system or set of rules. a scientific exam of deductive legislation and of optimistic legislation is gifted. The set of all attainable pairs of legislation presents us with a device for classifying the various ways for materializing algorithms (e.g. undefined, microprogramming, algorithmic programming, declarative programming, deductive procedure for recursive routines).