No description available.

Thesis (Ph.D.)--Massachusetts Institute of Technology, Dept. of Mathematics, 1982. / MICROFICHE COPY AVAILABLE IN ARCHIVES AND SCIENCE / Vita. / Bibliography: leaves 135-137. / by Kenneth Sidney Alexander. / Ph.D.

This project looks at using diagrammatic reasoning to prove mathematical theorems. The work is motivated by a need for theorem provers whose reasoning is readily intelligible to human beings. It should also have practical applications in mathematics teaching. We focus on the continuous domain of analysis - a geometric subject, but one which is taught using a dry algebraic formalism which many students find hard. The geometric nature of the domain makes it suitable for a diagram-based approach. However it is a difficult domain, and there are several problems, including handling alternating quantifiers, sequences and generalisation. We developed representations and reasoning methods to solve these. Our diagram logic isn't complete, but does cover a reasonable range of theorems. It utilises computers to extend diagrammatic reasoning in new directions – including using animation. This work is tested for soundness, and evaluated empirically for ease of use. We demonstrate that computerised diagrammatic theorem proving is not only possible in the domain of real analysis, but that students perform better using it than with an equivalent algebraic computer system.

Kakutani’s fixed point theorem has many applications in economics and game theory. One of its most well known applications is in John Nash’s paper [8], where the theorem is used to prove the existence of an equilibrium strategy in n-person games. Sperner’s lemma, on the other hand, is a combinatorial result concerning the labelling of the vertices of simplices and their triangulations. It is known that Sperner’s lemma is equivalent to a result called Brouwer’s fixed point theorem, of which Kakutani’s theorem is a generalization. A natural question that arises is whether we can prove Kakutani’s fixed point theorem directly using Sperner’s lemma without going through Brouwer’s theorem. The objective of this thesis to understand Kakutani’s theorem, Sperner’s lemma, and how they are related. In particular, I explore ways in which Sperner’s lemma can be used to prove Kakutani’s theorem and related results.

Results from combinatorial topology have shown that certain combinatorial lemmas are equivalent to certain topologocal fixed point theorems. For example, Sperner’s lemma about labelings of triangulated simplices is equivalent to the fixed point theorem of Brouwer. Moreover, since Sperner’s lemma has a constructive proof, its equivalence to the Brouwer fixed point theorem provides a constructive method for actually finding the fixed points rather than just stating their existence. The goal of this research project is to develop a combinatorial analogue for the Poincare ́-Birkhoff fixed point theorem.

We give an overview of the basic properties of Banach Algebras. After that we specialize to the case of commutative Banach Algebras and study the Gelfand Map. We study the main characteristic of that map, and work on some applications.

A variety of new mean value theorems are presented along with interesting proofs and generalizations of the standard theorems. Three proofs are given for the ordinary Mean Value Theorem for derivatives, the third of which is interesting in that it is independent of of Rolle's Theorem. The Second Mean Value Theorem for derivatives is generalized, with the use of determinants, to three functions and also generalized in terms of nth order derivatives. Observing that under certain conditions the tangent line to the curve of a differentiable function passes through the initial point, we find a new type of mean value theorem for derivatives. This theorem is extended to two functions and later in the paper an integral analog is given together with integral mean value theorems. Many new mean value theorems are presented in their respective settings including theorems for the total variation of a function, the arc length of the graph of a function, and for vector-valued functions. A mean value theorem in the complex plane is given in which the difference quotient is equal to a linear combination of the values of the derivative. Using a regular derivative, the ordinary Mean Value Theorem for derivatives is extended into Rn, n>1.

Thesis (Ph. D.)--Oregon State University, 2002. / Printout. Includes bibliographical references (leaves 58-61). Also available on the World Wide Web.

The current Thesis is devoted to comprehensive studies of comparison, or stochastic domination, theorems. It presents a combination of theoretical research and practical ideas formulated in several specific examples. Previously known results and their place it the theory of stochastic processes and stochastic differential equations is reviewed. This part of the work yielded three new theoretical results, formulated as theorems. Two of them are extensions of commonly used methods to more sophisticated processes and conditions. The third theorem is proven using previously not exploited technique. The place of all three results in the global theory is demonstrated by examining interconnections and possible distinctions between old and new theorems. Second and equally important part of the work focuses on more practical issues. Its main goal is to demonstrate where and how various theoretical findings can be applied to typical financial problems, such as option pricing, hedging, risk management and others. The example chapter summarizes the best of the obtained results in this direction. / Mathematical Finance

Developing logic in machines has always been an area of concern for scientists. Automated Theorem Proving is a field that has implemented the concept of logical consequence to a certain level. However, if the number of available axioms is very large then the probability of getting a proof for a conjecture in a reasonable time limit can be very small. This is where the ability to learn from previously proved theorems comes into play. If we see in our own lives, whenever a new situation S(NEW) is encountered we try to recollect all old scenarios S(OLD) in our neural system similar to the new one. Based on them we then try to find a solution for S(NEW) with the help of all related facts F(OLD) to S(OLD). Similar is the concept in this research. The thesis deals with developing a solution and finally implementing it in a tool that tries to prove a failed conjecture (a problem that the ATP system failed to prove) by extracting a sufficient set of axioms (we call it Refined Axiom Set (RAS)) from a large pool of available axioms. The process is carried out by measuring the similarity of a failed conjecture with solved theorems (already proved) of the same domain. We call it "process1", which is based on syntactic selection of axioms. After process1, RAS may still have irrelevant axioms, which motivated us to apply semantic selection approach on RAS so as to refine it to a much finer level. We call this approach as "process2". We then try to prove failed conjecture either from the output of process1 or process2, depending upon whichever approach is selected by the user. As for our testing result domain, we picked all FOF problems from the TPTP problem domain called SWC, which consisted of 24 broken conjectures (problems for which the ATP system is able to show that proof exists but not able to find it because of limited resources), 124 failed conjectures and 274 solved theorems. The results are produced by keeping in account both the broken and failed problems. The percentage of broken conjectures being solved with respect to the failed conjectures is obviously higher and the tool has shown a success of 100 % on the broken set and 19.5 % on the failed ones.