Inductive Theorem Proving and Computer Algebra in the Mathweb Software Bus

Reasoning systems have reached a high degree of maturity in the last decade. However, even the most successful systems are usually not general purpose problem solvers but are typically specialised on problems in a certain domain. The MathWeb SOftware Bus (Mathweb-SB) is a system for combining reasoning specialists via a common osftware bus. We described the integration of the lambda-clam systems, a reasoning specialist for proofs by induction, into the MathWeb-SB. Due to this integration, lambda-clam now offers its theorem proving expertise to other systems in the MathWeb-SB. On the other hand, lambda-clam can use the services of any reasoning specialist already integrated. We focus on the latter and describe first experimnents on proving theorems by induction using the computational power of the MAPLE system within lambda-clam.

Large Rayleigh number thermal convection: heat flux predictions and strongly nonlinear solutions

We investigate the structure of strongly nonlinear Rayleigh–Bénard convection cells in the asymptotic limit of large Rayleigh number and fixed, moderate Prandtl number. Unlike the flows analyzed in prior theoretical studies of infinite Prandtl number convection, our cellular solutions exhibit dynamically inviscid constant-vorticity cores. By solving an integral equation for the cell-edge temperature distribution, we are able to predict, as a function of cell aspect ratio, the value of the core vorticity, details of the flow within the thin boundary layers and rising/falling plumes adjacent to the edges of the convection cell, and, in particular, the bulk heat flux through the layer. The results of our asymptotic analysis are corroborated using full pseudospectral numerical simulations and confirm that the heat flux is maximized for convection cells that are roughly square in cross section.