1.
2.
3.
Al-Zoubi, Noura, et al.
(författare)
Elastic properties of 4d transition metal alloys : Values and trends
2019
Ingår i: Computational materials science. - : ELSEVIER SCIENCE BV. - 0927-0256 .- 1879-0801. ; 159, s. 273-280
Tidskriftsartikel (refereegranskat) abstract
Using the Exact Muffin-Tin Orbitals method within the Perdew-Burke-Ernzerhof exchange-correlation approximation for solids and solid surfaces (PBEso1), we study the single crystal elastic constants of 4d transition metals (atomic number Z between 39 and 47) and their binary alloys in the body centered cubic (bcc) and face centered cubic (fcc) structures. Alloys between the first neighbors Z(Z + 1) and between the second neighbors Z(Z + 2) are considered. The lattice constants, bulk moduli and elastic constants are found in good agreement with the available experimental and theoretical data. It is shown that the correlation between the relative tetragonal shear elastic constant C-fcc'-2C(bcc)' and the structural energy difference between the fcc and bcc lattices Delta E is superior to the previously considered models. For a given crystal structure, the equiatomic Z(Z + 2) alloys turn out to have similar structural and elastic properties as the pure elements with atomic number (Z + 1). Furthermore, alloys with composition Z(1-x)(Z + 2)(x) possess similar properties as Z(1-2x)(Z + 1)(2x). The present theoretical data on the structural and the elastic properties of 4d transition metal alloys provides consistent input for coarse scale modeling of material properties.
4.
Curzi, Gianluca, 1991, et al.
(författare)
Computational expressivity of (circular) proofs with fixed points
2023
Ingår i: LICS.
Konferensbidrag (refereegranskat) abstract
We study the computational expressivity of proof systems with fixed point operators, within the ‘proofs-as-programs’ paradigm. We start with a calculus μLJ (due to Clairambault) that extends intuitionistic logic by least and greatest positive fixed points. Based in the sequent calculus, μLJ admits a standard extension to a ‘circular’ calculus CμLJ.Our main result is that, perhaps surprisingly, both μLJ and CμLJ represent the same first-order functions: those provably total in Π12−CA0, a subsystem of second-order arithmetic beyond the ‘big five’ of reverse mathematics and one of the strongest theories for which we have an ordinal analysis (due to Rathjen). This solves various questions in the literature on the computational strength of (circular) proof systems with fixed points.For the lower bound we give a realisability interpretation from an extension of Peano Arithmetic by fixed points that has been shown to be arithmetically equivalent to Π12−CA0 (due to Möllerfeld). For the upper bound we construct a novel computability model in order to give a totality argument for circular proofs with fixed points. In fact we formalise this argument itself within Π12−CA0 in order to obtain the tight bounds we are after. Along the way we develop some novel reverse mathematics for the Knaster-Tarski fixed point theorem.
5.
