automatic construction of finite algebras

This paper deals withmodel generation for equational theories, i.e., automatically generating (finite) models of a given set of (logical) equations. Our method of finite model generation and a tool for automatic construction of finite algebras is described. Some examples are given to show the applications of our program. We argue that, the combination of model generators and theorem provers enables us to get a better understanding of logical theories. A brief comparison between our tool and other similar tools is also presented.

constructing finite algebras with falcon

The generation of models and counterexamples is an important form of reasoning. In this paper, we give a formal account of a system, called FALCON, for constructing finite algebras from given equational axioms. The abstract algorithms, as well as some implementation details and sample applications, are presented. The generation of finite models is viewed as a constraint satisfaction problem, with ground instances of the axioms as constraints. One feature of the system is that it employs a very simple technique, called the least number heuristic, to eliminate isomorphic (partial) models, thus reducing the size of the search space. The correctness of the heuristic is proved. Some experimental data are given to show the performance and applications of the system.

Abel Inversion of Axially-Symmetric Shock Wave Flows

Finite-fringe interferograms produced for axisymmetric shock wave flows are analyzed by Fourier transform fringe analysis and an Abel inversion method to produce density field data for the validation of numerical models. For the Abel inversion process, we use basis functions to model phase data from axially-symmetric shock wave structure. Steady and unsteady flow problems are studied, and compared with numerical simulations. Good agreement between theoretical and experimental results is obtained when one set of basis functions is used during the inversion process, but the shock front is smeared when another is used. This is because each function in the second set of basis functions is infinitely differentiable, making them poorly-suited to the modelling of a step function as is required in the representation of a shock wave.