Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain

This paper reports a case study in the use of proof planning in the context of higher order syntax. Rippling is a heuristic for guiding rewriting steps in induction that has been used successfully in proof planning inductive proofs using first order representations. Ordinal arithmetic provides a natural set of higher order examples on which transfinite induction may be attempted using rippling. Previously Boyer-Moore style automation could not be applied to such domains. We demonstrate that a higher-order extension of the rippling heuristic is sufficient to plan such proofs automatically. Accordingly, ordinal arithmetic has been implemented in lambda-clam, a higher order proof planning system for induction, and standard undergraduate text book problems have been successfully planned. We show the synthesis of a fixpoint for normal ordinal functions which demonstrates how our automation could be extended to produce more interesting results than the textbook examples tried so far.

Fundamental behaviour of Virtual-Build-to-Order systems

Virtual-Build-to-Order (VBTO) is an emerging order fulfilment system within the automotive sector that is intended to improve fulfilment performance by taking advantage of integrated information systems. The primary innovation in VBTO systems is the ability to make available all unsold products that are in the production pipeline to all customers. In a conventional system the pipeline is inaccessible and a customer can be fulfilled by a product from stock or having a product Built-to-Order (BTO), whereas in a VBTO system a customer can be fulfilled by a product from stock, by being allocated a product in the pipeline, or by a build-to-order product. Simulation is used to investigate and profile the fundamental behaviour of the basic VBTO system and to compare it to a Conventional system. A predictive relationship is identified, between the proportions of customers fulfilled through each mechanism and the ratio of product variety / pipeline length. The simulations reveal that a VBTO system exhibits inherent behaviour that alters the stock mix and levels, leading to stock levels being higher than in an equivalent conventional system at certain variety / pipeline ratios. The results have implications for the design and management of order fulfilment systems in sectors such as automotive where VBTO is a viable operational model.

Review of order fulfilment models for Catalogue Mass Customization

Mass Customization (MC) is not a mature business strategy and hence it is not clear that a single or small group of operational models are dominating. Companies tend to approach MC from either a mass production or a customization origin and this in itself gives reason to believe that several operational models will be observable. This paper reviews actual and theoretical fulfilment systems that enterprises could apply when offering a pre-engineered catalogue of customizable products and options. Issues considered are: How product flows are structured in relation to processes, inventories and decoupling point(s); - Characteristics of the OF process that inhibit or facilitate fulfilment; - The logic of how products are allocated to customers; - Customer factors that influence OF process design and operation. Diversity in the order fulfilment structures is expected and is found in the literature. The review has identified four structural forms that have been used in a Catalogue MC context: - fulfilment from stock; - fulfilment from a single fixed decoupling point; - fulfilment from one of several fixed decoupling points; - fulfilment from several locations, with floating decoupling points. From the review it is apparent that producers are being imaginative in coping with the demands of high variety, high volume, customization and short lead times. These demands have encouraged the relationship between product, process and customer to be re-examined. Not only has this strengthened interest in commonality and postponement, but, as is reported in the paper, has led to the re-engineering of the order fulfilment process to create models with multiple fixed decoupling points and the floating decoupling point system