Proof theory

Dawood, Hend, and Yasser Dawood. "Universal Intervals: Towards a Dependency-Aware Interval Algebra." In Mathematical Methods in Interdisciplinary Sciences. Hoboken, New Jersey: John Wiley and Sons, 2020. Abstractuniversal_intervals_abstract_dawood_wiley_2020.pdf

Interval computations are most fundamental in addressing uncertainty and imprecision. The intended status of this chapter is to be both an introduction and a treatise on some theoretical and practical aspects of interval mathematics. In the body of the work, there is room for novelties which may not be devoid of interest to researchers and specialists. The theories of classical intervals and parametric intervals are formally constructed and their mathematical structures are uncovered. By means of the logical concepts of Skolemization and quantification dependence, the notion of interval dependency is formalized by putting on a systematic basis its meaning, and thus gaining the advantage of indicating formally the criteria by which it is to be characterized and, accordingly, deducing its fundamental properties in a merely logical manner. Moreover, with a view to treating some problems of the present interval theories, a new alternate theory of intervals, namely the "theory of universal intervals", is presented and proved to have a nice S-field algebra, which extends the ordinary field of the reals. Our approach is formal by the pursuit of formulating the mathematical concepts in a strictly accurate manner, our perspective is systematic by taking the passage from the informal treatments to the formal technicalities of mathematical logic, and our concern is to take one small step towards paving the way for developing dependency-aware interval methods.

Keywords: Interval mathematics, Classical interval arithmetic, Parametric interval arithmetic, Universal interval arithmetic, Interval dependency, Functional dependence, Guaranteed enclosures, S-Semiring, S-Field, Skolemization.

Dawood, Hend, and Nefertiti Megahed. "A Consistent and Categorical Axiomatization of Differentiation Arithmetic Applicable to First and Higher Order Derivatives." Punjab University Journal of Mathematics 51, no. 11 (2019): 77-100. Abstractpujm_51-11_p77-100_dawood.pdfWebsite

Differentiation arithmetic is a principal and accurate technique for the computational evaluation of derivatives of first and higher order. This article aims at recasting real differentiation arithmetic in a formalized theory of dyadic real differentiation numbers that provides a foundation for first and higher order automatic derivatives. After we set the stage by putting on a systematic basis certain fundamental notions of the algebra of differentiation numbers, we begin by setting up an axiomatic theory of real differentiation arithmetic, as a many-sorted extension of the theory of a continuously ordered field, and then establish the proofs for its consistency and categoricity. Next, we carefully construct the algebraic system of real differentiation arithmetic, deduce its fundamental properties, and prove that it constitutes a commutative unital ring. Furthermore, we describe briefly the extensionality of the system to an interval differentiation arithmetic and to an algebraically closed commutative ring of complex differentiation arithmetic. Finally, a word is said on machine realization of real differentiation arithmetic and its correctness, with an addendum on how to compute automatic derivatives of first and higher order.

Keywords: Automatic differentiation; Categorical differentiation arithmetic; Consistent differentiation arithmetic; Commutative unital ring; Interval differentiation arithmetic; Algebraically closed commutative rings.

Dawood, Hend, and Yasser Dawood. On the Metamathematics of the Theory of Interval Numbers. Giza: Department of Mathematics, Faculty of Science, Cairo University, 2010. Abstract

The aim of this paper is to provide a metamathematical investigation of the theory of intervals with the requisite predicate calculi and axiomatic set theory.

Dawood, Hend, and Yasser Dawood. Logical Aspects of Interval Dependency. Giza: Department of Mathematics, Faculty of Science, Cairo University, 2013. Abstract

By means of the most fundamental logical concepts of quantification theory, the notion of interval dependency is axiomatized and its fundamental properties are deduced.

Dawood, Hend, and Yasser Dawood. The Form of the Uncertain: On the Mathematical Structures of Uncertainty. Giza: Department of Mathematics, Faculty of Science, Cairo University, 2016. Abstract

In this report, we investigate into the algebraic structures underlying the mathematics of uncertainty.

Dawood, Hend. "Interval Mathematics as a Potential Weapon against Uncertainty." In Mathematics of Uncertainty Modeling in the Analysis of Engineering and Science Problems. Hershey, PA: IGI Global, 2014. Abstractinterval_mathematics_as_a_potential_weapon_against_uncertainty.pdf

This chapter is devoted to introducing the theories of interval algebra to people who are interested in applying the interval methods to uncertainty analysis in science and engineering. In view of this purpose, we shall introduce the key concepts of the algebraic theories of intervals that form the foundations of the interval techniques as they are now practised, provide a historical and epistemological background of interval mathematics and uncertainty in science and technology, and finally describe some typical applications that clarify the need for interval computations to cope with uncertainty in a wide variety of scientific disciplines.

Keywords: Interval mathematics, Uncertainty, Quantitative Knowledge, Reliability, Complex interval arithmetic, Machine interval arithmetic, Interval automatic differentiation, Computer graphics, Ray tracing, Interval root isolation.

Dawood, Hend. Interval Mathematics: Foundations, Algebraic Structures, and Applications. Cairo: Cairo University, 2012. Abstractinterval_mathematics_msc_thesis_by_hend_dawood.pdf

We begin by constructing the algebra of classical intervals and prove that it is a nondistributive abelian semiring. Next, we formalize the notion of interval dependency, along with discussing the algebras of two alternate theories of intervals: modal intervals, and constraint intervals. With a view to treating some problems of the present interval theories, we present an alternate theory of intervals, namely the "theory of optimizational intervals", and prove that it constitutes a rich S-field algebra, which extends the ordinary field of the reals, then we construct an optimizational complex interval algebra. Furthermore, we define an order on the set of interval numbers, then we present the proofs that it is a total order, compatible with the interval operations, dense, and weakly Archimedean. Finally, we prove that this order extends the usual order on the reals, Moore's partial order, and Kulisch's partial order on interval numbers.

Classical interval arithmetic, Machine interval arithmetic, Interval dependency, Constraint intervals, Modal intervals, Classical complex intervals, Optimizational intervals, Optimizational complex intervals, S-field algebra, Ordering subsets of the reals, Interval arithmetic, Ordering interval numbers, Ordinal power, Total order, Well order, Order compatibilty, Weak Archimedeanity, Dedekind completeness, Interval lattice, Interval order topology, Moore's partial order, Kulisch's partial order.