EXTENDING THE PROOF PLAN METHODOLOGY TO COMPUTER CONFIGURATION PROBLEMS

Can the technique of proof plans, developed originally for use in theorem proving, be successfully applied outside mathematics? We look at a problem associated with the configuration of large computer systems, namely that of checking orders drawn up by sales people on behalf of customers. Strategies exist for this task which may be explicitly encoded. We discuss the formation of plans for order checking and the factors involved in determining whether such plans can be guaranteed to succeed.