Microstructure and mechanical properties of fine grained uranium prepared by ECAP and subsequent intermediate heat treatment

The microstructure and mechanical properties of fine grained uranium prepared by equal channel angular pressing(ECAP)and subsequent intermediate heat treatment were investigated systematically by the confocal laser scanning microscope(CLSM),electron backscatter diffraction(EBSD)and split Hopkinson pressure bar(SHPB).The results show that the initial coarse grained uranium was refined from about 1000 to 6.5μm prepared by ECAP at 3 passes and subsequent heat treatment,and the corresponding dynamic yield strength increased from 135 to 390 MPa.For the ECAPed uranium samples,the relationship between grain size and yield strength could be described by classical Hall−Petch relationship,and the fitting Hall−Petch relationship for the fine grained uranium samples prepared by ECAP was drawn.

Dynamic Spallation in Uranium under Laser Shock Loading

The spall behavior of uranium is investigated using direct laser ablation loading experiments. The uranium targets are cut and ground to 0.05 mm, 0.1 mm, and 0.15 mm in thickness. Laser energies are varied to yield a constant peak pressure. This results in different strain rates and varying degrees of damage to the uranium targets. The spall strength is calculated and analyzed from the free surface velocity histories recorded using a line velocity interferometer for any reflections system. The spall strength increases from 4.3 GPa to 9.4 GPa with strain rates ranging from 4.0 × 10~6 s^(-1) to 1.7 × 10~7 s^(-1). Post-mortem analysis is performed on the recovered samples, revealing the twin-matrix interfaces together with the inclusions to be the primary factor governing the spall fracture of uranium.

An Improvement of Herbrand's Theorem and Its Application to Model Generation Theorem Proving

This paper presents an improvement of Herbrand's theorem.We propose a method for specifying a subuniverse of the Herbrand universe of a clause set S for each argument of predicate symbols and function symbols in S.We prove that a clause set S is unsatisfiable if and only if there is a finite unsatisfiable set of ground instances of clauses of S that are derived by only instantiating each variable,which appears as an argument of predicate symbols or function symbols,in S over its corresponding argument's sub-universe of the Herbrand universe of S.Because such sub-universes are usually smaller(sometimes considerably)than the Herbrand universe of S,the number of ground instances may decrease considerably in many cases.We present an algorithm for automatically deriving the sub-universes for arguments in a given clause set,and show the correctness of our improvement.Moreover,we introduce an application of our approach to model generation theorem proving for non-range-restricted problems,show the range-restriction transformation algorithm based on our improvement and provide examples on benchmark problems to demonstrate the power of our approach.