Search

Differential dynamic logic (dL) is a formal framework for specifying and reasoning about hybrid systems, i.e., dynamical systems that exhibit both continuous and discrete behaviors. These kinds of systems arise in many safety- and mission-critical applications. This paper presents a formalization of dL in the Prototype Verification System (PVS) that includes the semantics of hybrid programs and dL's proof calculus. The formalization embeds dL into the PVS logic, resulting in a version of dL whose proof calculus is not only formally verified, but is also available for the verification of hybrid programs within PVS itself. This embedding, called Plaidypvs (Properly Assured Implementation of dL for Hybrid Program Verification and Specification), supports standard dL style proofs, but further leverages the capabilities of PVS to allow reasoning about entire classes of hybrid programs. The embedding also allows the user to import the well-established definitions and mathematical theories available in PVS., Comment: In Proceedings LSFA/HCVS 2023, arXiv:2404.13672

Large Language Models (LLMs) such as ChatGPT and LlaMA are advancing rapidly in generative Artificial Intelligence (AI), but their immense size poses significant challenges, such as huge training and inference costs, substantial energy demands, and limitations for on-site deployment. Traditional compression methods such as pruning, distillation, and low-rank approximation focus on reducing the effective number of neurons in the network, while quantization focuses on reducing the numerical precision of individual weights to reduce the model size while keeping the number of neurons fixed. While these compression methods have been relatively successful in practice, there is no compelling reason to believe that truncating the number of neurons is an optimal strategy. In this context, this paper introduces CompactifAI, an innovative LLM compression approach using quantum-inspired Tensor Networks that focuses on the model's correlation space instead, allowing for a more controlled, refined and interpretable model compression. Our method is versatile and can be implemented with - or on top of - other compression techniques. As a benchmark, we demonstrate that a combination of CompactifAI with quantization allows to reduce a 93% the memory size of LlaMA 7B, reducing also 70% the number of parameters, accelerating 50% the training and 25% the inference times of the model, and just with a small accuracy drop of 2% - 3%, going much beyond of what is achievable today by other compression techniques. Our methods also allow to perform a refined layer sensitivity profiling, showing that deeper layers tend to be more suitable for tensor network compression, which is compatible with recent observations on the ineffectiveness of those layers for LLM performance. Our results imply that standard LLMs are, in fact, heavily overparametrized, and do not need to be large at all., Comment: 5 pages, 4 figures, 2 tables, and supplementary information of 2 pages and 1 figure. Revised version with new benchmarks for LlaMA2-7B

This study presents the results concerning six red giant stars members of the globular cluster NGC 6558. Our analysis utilized high-resolution near-infrared spectra obtained through the CAPOS initiative (the APOgee Survey of Clusters in the Galactic Bulge), which focuses on surveying clusters within the Galactic Bulge, as a component of the Apache Point Observatory Galactic Evolution Experiment II survey (APOGEE-2). We employ the BACCHUS (Brussels Automatic Code for Characterizing High accUracy Spectra) code to provide line-by-line elemental-abundances for Fe-peak (Fe, Ni), $\alpha$-(O, Mg, Si, Ca, Ti), light-(C, N), odd-Z (Al), and the $s$-process element (Ce) for the 4 stars with high signal-to-noise ratios. This is the first reliable measure of the CNO abundances for NGC 6558. Our analysis yields a mean metallicity for NGC 6558 of $\langle$[Fe/H]$\rangle$ = $-$1.15 $\pm$ 0.08, with no evidence for a metallicity spread. We find a Solar Ni abundance, $\langle$[Ni/Fe]$\rangle$ $\sim$ $+$0.01, and a moderate enhancement of $\alpha$-elements, ranging between $+$0.16 to $<+$0.42, and a slight enhancement of the $s$-process element $\langle$[Ce/Fe]$\rangle$ $\sim$ $+$0.19. We also found low levels of $\langle$[Al/Fe]$\rangle \sim $+$0.09$, but with a strong enrichment of nitrogen, [N/Fe]$>+$0.99, along with a low level of carbon, [C/Fe]$<-$0.12. This behaviour of Nitrogen-Carbon is a typical chemical signature for the presence of multiple stellar populations in virtually all GCs; this is the first time that it is reported in NGC 6558. We also observed a remarkable consistency in the behaviour of all the chemical species compared to the other CAPOS bulge GCs of the same metallicity., Comment: To appear in MNRAS. The paper is 11 pages long, containing 5 figures, 4 tables

We present the first detailed chemical analysis from APOGEE-2S observations of stars in six regions of recently discovered substructures in the outskirts of the Magellanic Clouds extending to 20 degrees from the LMC center. We also present, for the first time, the metallicity and alpha-abundance radial gradients of the LMC and SMC out to 11 degrees and 6 degrees, respectively. Our chemical tagging includes 13 species including light, alpha, and Fe-peak elements. We find that the abundances of all of these chemical elements in stars populating two regions in the northern periphery - along the northern "stream"-like feature - show good agreement with the chemical patterns of the LMC, and thus likely have an LMC origin. For substructures located in the southern periphery of the LMC, we find more complex chemical and kinematical signatures, indicative of a mix of LMC-like and SMC-like populations. However, the southern region closest to the LMC shows better agreement with the LMC, whereas that closest to the SMC shows a much better agreement with the SMC chemical pattern. When combining this information with 3-D kinematical information for these stars, we conclude that the southern region closest to the LMC has likely an LMC origin, whereas that closest to the SMC has an SMC origin, and the other two southern regions have a mix of LMC and SMC origins. Our results add to the evidence that the southern substructures of the LMC periphery are the product of close interactions between the LMC and SMC, and thus likely hold important clues that can constrain models of their detailed dynamical histories., Comment: 21 pages, 15 figures, 9 tables; Accepted for publication in A&A

It has been proposed that the globular cluster-like system Terzan 5 is the surviving remnant of a primordial building block of the Milky Way bulge, mainly due to the age/metallicity spread and the distribution of its stars in the $\alpha$-Fe plane. We employ Sloan Digital Sky Survey (SDSS-IV) data from the Apache Point Observatory Galactic Evolution Experiment (APOGEE 2) to test this hypothesis. Adopting a random sampling technique, we contrast the abundances of 10 elements in Terzan 5 stars with those of their bulge field counterparts with comparable atmospheric parameters, finding that they differ at statistically significant levels. Abundances between the two groups differ by more than 1$\sigma$ in Ca, Mn, C, O, and Al, and more than 2$\sigma$ in Si and Mg. Terzan 5 stars have lower [$\alpha$/Fe] and higher [Mn/Fe] than their bulge counterparts. Given those differences, we conclude that Terzan 5 is not the remnant of a $major$ building block of the bulge. We also estimate the stellar mass of the Terzan 5 progenitor based on predictions by the Evolution and Assembly of GaLaxies and their Environments (EAGLE) suite of cosmological numerical simulations, concluding that it may have been as low as $\sim3\times10^8$ M$_\odot$ so that it was likely unable to significantly influence the mean chemistry of the bulge/inner disk, which is significantly more massive ($\sim10^{10}$ M$_\odot$). We briefly discuss existing scenarios for the nature of Terzan 5 and propose an observational test that may help elucidate its origin., Comment: 15 pages, 10 figures, accepted for publication by MNRAS

In this research we test the ability of a three Washington filter combination, (C-T1)-(T1-T2), compared with that of the traditional C-T1 color to find multiple populations on two globular clusters: NGC 7099 and NGC 1851, types I and II Globular clusters, respectively. Our improved photometry and membership selection, now using Gaia proper motions, finds that the second population stars are more centrally concentrated than first population stars, as expected and contrary to our previous findings for NGC 7099. We find that multiple populations are more easily detected in both clusters using the new (C-T1)-(T1-T2) color, although C-T1 conserves the best width/error ratio. We also search for differences of both colors while splitting the red-RGB and the blue-RGB in NGC 1851, but no significant improvement was found., Comment: 23 pages, 5 Tables, 9 figures

We report the first 3-D kinematical measurements of 88 stars in the direction of several recently discovered substructures in the southern periphery of the Large Magellanic Cloud (LMC) using a combination of Gaia proper motions and radial velocities from the APOGEE-2 survey. More specifically, we explore stars lie in assorted APOGEE-2 pointings in a region of the LMC periphery where various overdensities of stars have previously been identified in maps of stars from Gaia and DECam. By using a model of the LMC disk rotation, we find that a sizeable fraction of the APOGEE-2 stars have extreme space velocities that are distinct from, and not a simple extension of, the LMC disk. Using N-body hydrodynamical simulations of the past dynamical evolution and interaction of the LMC and Small Magellanic Cloud (SMC), we explore whether the extreme velocity stars may be accounted for as tidal debris created in the course of that interaction. We conclude that the combination of LMC and SMC debris produced from their interaction is a promising explanation, although we cannot rule out other possible origins, and that these new data should be used to constrain future simulations of the LMC-SMC interaction. We also conclude that many of the stars in the southern periphery of the LMC lie out of the LMC plane by several kpc. Given that the metallicity of these stars suggest they are likely of Magellanic origin, our results suggest that a wider exploration of the past interaction history of the Magellanic Clouds is needed.

(ABRIDGED) We have performed the first detailed spectral analysis of red giant members of the relatively high-metallicity globular cluster (GC) Tononzintla~2 (Ton~2) using high-resolution near-infrared spectra collected with the Apache Point Observatory Galactic Evolution Experiment II survey (APOGEE-2), obtained as part of the bulge Cluster APOgee Survey. We investigate chemical abundances for a variety of species including the light-, odd-Z, $\alpha$-, Fe-peak, and neutron-capture elements from high S/N spectra of seven giant members. The derived mean cluster metallicity is [Fe/H]$=-0.70\pm0.05$, with no evidence for an intrinsic metallicity spread. Ton~2 exhibits a typical $\alpha$-enrichment that follows the trend for high-metallicity Galactic GCs, similar to that seen in 47~Tucanae and NGC~6380. We find a significant nitrogen spread ($>0.87$ dex), and a large fraction of nitrogen-enriched stars that populate the cluster. Given the relatively high-metallicity of Ton~2, these nitrogen-enriched stars are well above the typical Galactic levels, indicating the prevalence of the multiple-population phenomenon in this cluster which also contains several stars with typical low, first-generation N abundances. We also identify the presence of [Ce/Fe] abundance spread in Ton~2, which is correlated with the nitrogen enhancement, indicating that the \textit{s}-process enrichment in this cluster has been produced likely by relatively low-mass Asymptotic Giant Branch stars. Furthermore, we find a mean radial velocity of the cluster, $-178.6\pm0.86$ km s$^{-1}$ with a small velocity dispersion, 2.99$\pm$0.61 km s$^{-1}$, which is typical of a GC. We also find a prograde bulge-like orbit for Ton~2 that appears to be radial and highly eccentric., Comment: Accepted for publication in A&A; 12 pages, 9 figures, 2 tables. arXiv admin note: text overlap with arXiv:2106.00027

Globular Clusters (GCs) are now well known to almost universally show multiple popu-lations (MPs). The HST UV Legacy Survey of a large number of Galactic GCs in UV filters optimized to explore MPs finds that a small fraction of GCs, termed Type II, also display more complex, anomalous behavior. Several well-studied Type II GCs show intrinsic Fe abundance variations, suggesting that the other, less well-studied, Type II GCs should also exhibit similar behavior. Our aim is to perform the first detailed metallicity analysis of NGC 1261, an intermediate mass Type II GC, in order to determine if this object shows an intrinsic Fe variation. We determined the Fe abundance in eight red giant members using Magellan-MIKE and UVES-FLAMES high-resolution, high S/N spectroscopy. The full range of [Fe/H] for the entire sample from the spectra is from -1.05 to -1.43 dexwith an observed spread sigma_obs=0.133 dex. Compared with the total internal error of Sigma_tot=0.06,this indicates a significant intrinsic metallicity spread of Sigma_int=0.119 dex. We found a very similar variation in [Fe/H] using an independent method to derive the atmospheric parameters based on near-IR photometry. More importantly, the mean metallicity of the five presumed normal metallicity stars is -1.37+/-0.02, while that of the three presumed anomalous/highmetallicity stars is -1.18+/-0.09. This difference is significant at the $\pm$2.4Sigma level. We find indications from existing data of other Type II GCs that several of them presumedto have real metallicity spreads may in fact posses none. The minimum mass required for a GC to acquire an intrinsic Fe spread appears to be $\pm$10^5 Msun. We find no strong correlation betwee nmass and metallicity variation for Type II GCs. The metallicity spread is also independent of the fraction of anomalous stars within the Type II GCs and of GC origin., Comment: 12 pages, 7 figures. Accepted for publication in MNRAS

We present results from a study of fifteen red giant members of the intermediate-metallicity globular cluster (GC) FSR 1758 using high-resolution near-infrared spectra collected with the Apache Point Observatory Galactic Evolution Experiment II survey (APOGEE-2), obtained as part of CAPOS (the bulge Cluster APOgee Survey). Since its very recent discovery as a massive GC in the bulge region, evoking the name Sequoia, this has been an intriguing object with a highly debated origin, and initially led to the suggestion of a purported progenitor dwarf galaxy of the same name. In this work, we use new spectroscopic and astrometric data to provide additional clues to the nature of FSR 1758. Our study confirms the GC nature of FSR 1758, and as such we report for the first time the existence of the characteristic N-C anti-correlation and Al-N correlation, revealing the existence of the multiple-population phenomenon, similar to that observed in virtually all GCs. Furthermore, the presence of a population with strongly enriched aluminium makes it unlikely FSR 1758 is the remnant nucleus of a dwarf galaxy, as Al-enhanced stars are uncommon in dwarf galaxies. We find that FSR 1758 is slightly more metal rich than previously reported in the literature, with a mean metallicity [Fe/H] between $-1.43$ to $-1.36$ (depending on the adopted atmospheric parameters), and with a scatter within observational error, again pointing to its GC nature. Overall, the $\alpha$-enrichment ($\gtrsim+0.3$ dex), Fe-peak (Fe, Ni), light- (C, N), and odd-Z (Al) elements follow the trend of intermediate-metallicity GCs. ... A new examination of its dynamical properties with the \texttt{GravPot16} model favors an association with the Gaia-Enceladus-Sausage accretion event. Thus, paradoxically, the cluster that gave rise to the name of the Sequoia dwarf galaxy does not appear to belong to this specific merging event., Comment: 15 pages, 8 pages, 3 Tables. Abridged abstract. Accepted for publication in Astronomy & Astrophysics (A&A)

Context. Bulge globular clusters (BGCs) are exceptional tracers of the formation and chemodynamical evolution of this oldest Galactic component. However, until now, observational difficulties have prevented us from taking full advantage of these powerful Galactic archeological tools. Aims. CAPOS, the bulge Cluster APOgee Survey, addresses this key topic by observing a large number of BGCs, most of which have only been poorly studied previously. Even their most basic parameters, such as metallicity, [{\alpha}/Fe], and radial velocity, are generally very uncertain. We aim to obtain accurate mean values for these parameters, as well as abundances for a number of other elements, and explore multiple populations. In this first paper, we describe the CAPOS project and present initial results for seven BGCs. Methods. CAPOS uses the APOGEE-2S spectrograph observing in the H band to penetrate obscuring dust toward the bulge. For this initial paper, we use abundances derived from ASPCAP, the APOGEE pipeline. Results. We derive mean [Fe/H] values of $-$0.85$\pm$0.04 (Terzan 2), $-$1.40$\pm$0.05 (Terzan 4), $-$1.20$\pm$0.10 (HP 1), $-$1.40$\pm$0.07 (Terzan 9), $-$1.07$\pm$0.09 (Djorg 2), $-$1.06$\pm$0.06 (NGC 6540), and $-$1.11$\pm$0.04 (NGC 6642) from three to ten stars per cluster. We determine mean abundances for eleven other elements plus the mean [$\alpha$/Fe] and radial velocity. CAPOS clusters significantly increase the sample of well-studied Main Bulge globular clusters (GCs) and also extend them to lower metallicity. We reinforce the finding that Main Bulge and Main Disk GCs, formed in situ, have [Si/Fe] abundances slightly higher than their accreted counterparts at the same metallicity. We investigate multiple populations and find our clusters generally follow the light-element (anti)correlation trends of previous studies of GCs of similar metallicity. We finally explore the abundances ..., Comment: 27 pages, 10 figures, 5 tables. Abridged abstract. Accepted for publication in Astronomy & Astrophysics (A&A)

More than a decade has passed since the definition of Globular Cluster (GC) changed, and now we know that they host Multiple Populations (MPs). But few GCs do not share that behaviour and Ruprecht 106 is one of these clusters. We analyzed thirteen member red giant branch stars using spectra in the wavelength range 6120-6405 Angstroms obtained through the GIRAFFE Spectrograph, mounted at UT2 telescope at Paranal, as well as the whole cluster using C, V, R and I photometry obtained through the Swope telescope at Las Campanas. Atmospheric parameters were determined from the photometry to determine Fe and Na abundances. A photometric analysis searching for MPs was also carried out. Both analyses confirm that Ruprecht 106 is indeed one on the few GCs to host Simple Stellar Population, in agreement with previous studies. Finally, a dynamical study concerning its orbits was carried out to analyze the possible extra galactic origin of the Cluster. The orbital integration indicates that this GC belongs to the inner halo, while an Energy plane shows that it cannot be accurately associated with any known extragalactic progenitor., Comment: 10 Figures (Figure 2 are 2 files) 3 tables (1 table without number)

The Independent Configurable Architecture for Reliable Operations of Unmanned Systems (ICAROUS) is a software architecture incorporating a set of algorithms to enable autonomous operations of unmanned aircraft applications. This paper provides an overview of Monitoring ICAROUS, a project whose objective is to provide a formal approach to generating runtime monitors for autonomous systems from requirements written in a structured natural language. This approach integrates FRET, a formal requirement elicitation and authoring tool, and Copilot, a runtime verification framework. FRET is used to specify formal requirements in structured natural language. These requirements are translated into temporal logic formulae. Copilot is then used to generate executable runtime monitors from these temporal logic specifications. The generated monitors are directly integrated into ICAROUS to perform runtime verification during flight., Comment: In Proceedings FMAS 2020, arXiv:2012.01176

Test instability in a floating-point program occurs when the control flow of the program diverges from its ideal execution assuming real arithmetic. This phenomenon is caused by the presence of round-off errors that affect the evaluation of arithmetic expressions occurring in conditional statements. Unstable tests may lead to significant errors in safety-critical applications that depend on numerical computations. Writing programs that take into consideration test instability is a difficult task that requires expertise on finite precision computations and rounding errors. This paper presents a toolchain to automatically generate and verify a provably correct test-stable floating-point program from a functional specification in real arithmetic. The input is a real-valued program written in the Prototype Verification System (PVS) specification language and the output is a transformed floating-point C program annotated with ANSI/ISO C Specification Language (ACSL) contracts. These contracts relate the floating-point program to its functional specification in real arithmetic. The transformed program detects if unstable tests may occur and, in these cases, issues a warning and terminate. An approach that combines the Frama-C analyzer, the PRECiSA round-off error estimator, and PVS is proposed to automatically verify that the generated program code is correct in the sense that, if the program terminates without a warning, it follows the same computational path as its real-valued functional specification., Comment: 32 pages. arXiv admin note: text overlap with arXiv:1808.04289

The steep learning curve of formal technologies is a well-known barrier to the adoption of formal verification tools in industry. This paper presents VSCode-PVS, a modern integrated development environment for the Prototype Verification System (PVS). This new environment integrates the editing and proof management functionalities of PVS in Visual Studio Code, a popular code editor widely used by software developers. VSCode-PVS provides functionalities that developers expect to find in modern verification tools, but are not available in the standard Emacs front-end of PVS, such as auto-completion, point-and-click navigation of definitions, live diagnostics for errors, and literate programming. The main features and architecture of the environment are presented, along with a comparison with other similar tools., Comment: In Proceedings F-IDE 2019, arXiv:1912.09611

Round-off errors arising from the difference between real numbers and their floating-point representation cause the control flow of conditional floating-point statements to deviate from the ideal flow of the real-number computation. This problem, which is called test instability, may result in a significant difference between the computation of a floating-point program and the expected output in real arithmetic. In this paper, a formally proven program transformation is proposed to detect and correct the effects of unstable tests. The output of this transformation is a floating-point program that is guaranteed to return either the result of the original floating-point program when it can be assured that both its real and its floating-point flows agree or a warning when these flows may diverge. The proposed approach is illustrated with the transformation of the core computation of a polygon containment algorithm developed at NASA that is used in a geofencing system for unmanned aircraft systems., Comment: Pre-proceedings paper presented at the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2018), Frankfurt am Main, Germany, 4-6 September 2018 (arXiv:1808.03326)

Over the last decade, the classical definition of Globular Clusters (GCs) as simple stellar populations was revolutionized due to the discovery of "Multiple Populations" (MPs). However, our knowledge of this phenomenon and its characteristics is still lacking greatly observationally, and there is currently no scenario that adequately explains its origin. It is therefore important to study as many GCs as possible to characterize whether or not they have MPs, and determine their detailed behavior to enlighten formation scenarios, using a wide range of techniques. The Washington photometric system has proved to be useful to find MPs thanks mainly to the UV-sensitivity and high efficiency of the C filter. We search for MPs in the Galactic GC NGC 7099 (M30), the second GC being searched for MPs using this system. We obtained photometric data using the Swope 1m telescope at Las Campanas Observatory, as well as the 4m SOAR facility. Our reduction procedure included addstar experiments to properly assess photometric errors. We find a clear signal of MPs based on an intrinsically wide color spread on the RGB, in particular due to a relatively small fraction of stars significantly bluer than the main RGB locus. These stars should correspond to so-called first generation stars, which we estimate to be roughly 15\% of the total. However, we find these first-generation stars to be more spatially concentrated than their second generation counterparts, which is the opposite to the general trend found in other clusters. We briefly discuss possible explanations for this phenomenon., Comment: 11 pages, 8 figures, 2 tables

This volume contains the proceedings of DCM 2015, the 11th International Workshop on Developments in Computational Models held on October 28, 2015 in Cali, Colombia. DCM 2015 was organized as a one-day satellite event of the 12th International Colloquium on Theoretical Aspects of Computing (ICTAC 2015). Several new models of computation have emerged in the last few years, and many developments of traditional computational models have been proposed with the aim of taking into account the new demands of computer systems users and the new capabilities of computation engines. A new computational model, or a new feature in a traditional one, usually is reflected in a new family of programming languages, and new paradigms of software development. The aim of the DCM workshop series is to bring together researchers who are currently developing new computational models or new features for traditional computational models, in order to foster their interaction, to provide a forum for presenting new ideas and work in progress, and to enable newcomers to learn about current activities in this area. Topics of interest include all abstract models of computation and their applications to the development of programming languages and systems.

This volume contains selected papers from the proceedings of the First International Workshop on Strategies in Rewriting, Proving, and Programming (IWS 2010), which was held on July 9, 2010, in Edinburgh, UK. Strategies are ubiquitous in programming languages, automated deduction and reasoning systems. In the two communities of Rewriting and Programming on one side, and of Deduction and Proof engines (Provers, Assistants, Solvers) on the other side, workshops have been launched to make progress towards a deeper understanding of the nature of strategies, their descriptions, their properties, and their usage, in all kinds of computing and reasoning systems. Since more recently, strategies are also playing an important role in rewrite-based programming languages, verification tools and techniques like SAT/SMT engines or termination provers. Moreover strategies have come to be viewed more generally as expressing complex designs for control in computing, modeling, proof search, program transformation, and access control. IWS 2010 was organized as a satellite workshop of FLoC 2010. FLoC 2010 provided an excellent opportunity to foster exchanges between the communities of Rewriting and Programming on one side, and of Deduction and Proof engines on the other side. IWS2010 was a joint follow-up of two series of worshops, held since 1997: the Strategies workshops held by the CADE-IJCAR community and the Workshops on Reduction Strategies (WRS) held by the RTA-RDP community.

The Plan Execution Interchange Language (PLEXIL) is a synchronous language developed by NASA to support autonomous spacecraft operations. In this paper, we propose a rewriting logic semantics of PLEXIL in Maude, a high-performance logical engine. The rewriting logic semantics is by itself a formal interpreter of the language and can be used as a semantic benchmark for the implementation of PLEXIL executives. The implementation in Maude has the additional benefit of making available to PLEXIL designers and developers all the formal analysis and verification tools provided by Maude. The formalization of the PLEXIL semantics in rewriting logic poses an interesting challenge due to the synchronous nature of the language and the prioritized rules defining its semantics. To overcome this difficulty, we propose a general procedure for simulating synchronous set relations in rewriting logic that is sound and, for deterministic relations, complete. We also report on two issues at the design level of the original PLEXIL semantics that were identified with the help of the executable specification in Maude.

Real number calculations on elementary functions are remarkably difficult to handle in mechanical proofs. In this paper, we show how these calculations can be performed within a theorem prover or proof assistant in a convenient and highly automated as well as interactive way. First, we formally establish upper and lower bounds for elementary functions. Then, based on these bounds, we develop a rational interval arithmetic where real number calculations take place in an algebraic setting. In order to reduce the dependency effect of interval arithmetic, we integrate two techniques: interval splitting and taylor series expansions. This pragmatic approach has been developed, and formally verified, in a theorem prover. The formal development also includes a set of customizable strategies to automate proofs involving explicit calculations over real numbers. Our ultimate goal is to provide guaranteed proofs of numerical properties with minimal human theorem-prover interaction.