Complex number is a major mathematical discovery. It can be used in many scientific fields, including engineering, electromagnetism, quantum physics, applied mathematics, and chaos theory. The aim of this paper investigates the problems of algebra, trigonometry and geometry, which can be solved cleverly by the properties of complex numbers.

Weighted polynomial regression of degree d with weight function Exp(£\ x) on an interval is considered. The D-optimal designs £i_d^* are completely characterized via three differential equations. Some invariant properties of £i_d^* under affine transformation are derived. The design £i_d^* as d goes to 1, is shown to converge weakly to the arcsin distribution. Comparisons of £i_d^* with the arcsin distribution are also made.

We look from a new point of view at the definition and basic properties of the Lebesgue measure and integral on Euclidean spaces, on abstract spaces, and on locally compact Hausdorff spaces. We use mini sums to give all of them a unified treatment that is more efficient than the standard ones. We also give Fubini's theorem a proof that is nicer and uses much lighter technical baggage than the usual treatments.

Theorem provers are faced with the challenges of size and complexity, fueled by the increasing range of applications. The use of concurrent/ distributed programming paradigms to engineer better theorem provers merits serious investigation, as it provides: more processing power and opportunities for implementing novel approaches to address theorem proving tasks hitherto infeasible in a sequential setting. Investigation of these opportunities for two diverse theorem prover settings with an emphasis on desirable implementation criteria is the core focus of this thesis. Concurrent programming is notoriously error prone, hard to debug and evaluate. Thus, implementation approaches which promote easy prototyping, portability, incremental development and effective isolation of design and implementation can greatly aid the enterprise of experimentation with the application of concurrent techniques to address specific theorem proving tasks. In this thesis, we have explored one such approach by using Alice ML, a functional programming language with support for concurrency and distribution, to implement the prototypes and have used programming abstractions to encapsulate the implementations of the concurrent techniques used. The utility of this approach is illustrated via proof-of-concept prototypes of concurrent systems for two diverse case studies of theorem proving: the propositional satisfiability problem (SAT) and LCF style (first-order) theorem proving, addressing some previously unexplored parallelisation opportunities for each, as follows:. SAT: We have developed a novel hybrid approach for SAT and implemented a prototype for the same: DPLL-Stalmarck. It uses two complementary algorithms for SAT, DPLL and Stalmarck’s. The two solvers run asynchronously and dynamic information exchange is used for co-operative solving. Interaction of the solvers has been encapsulated as a programming abstraction. Compared to the standalone DPLL solver, DPLL-Stalmarck shows significant performance gains for two of the three problem classes considered and comparable behaviour otherwise. As an exploratory research effort, we have developed a novel algorithm, Concurrent Stalmarck, by applying concurrent techniques to the Stalmarck algorithm. A proof-of-concept prototype for the same has been implemented. Implementation of the saturation technique of the Stalmarck algorithm in a parallel setting, as implemented in Concurrent Stalmarck, has been encapsulated as a programming abstraction. LCF: Provision of programmable concurrent primitives enables customisation of concurrent techniques to specific theorem proving scenarios. In this case study, we have developed a multilayered approach to support programmable, sound extensions for an LCF prover: use programming abstractions to implement the concurrent techniques; use these to develop novel tacticals (control structures to apply tactics), incorporating concurrent techniques; and use these to develop novel proof search procedures. This approach has been implemented in a prototypical LCF style first-order prover, using Alice ML. New tacticals developed are: fastest-first; distributed composition; crossTalk: a novel tactic which uses dynamic, collaborative information exchange to handle unification across multiple sub-goals, with shared meta-variables; a new tactic, performing simultaneous proof-refutation attempts on propositional (sub- )goals, by invoking an external SAT solver (SAT case study), as a counter-example finder. Examples of concrete theorem proving scenarios are provided, demonstrating the utility of these extensions. Synthesis of a variety of automatic proof search procedures has been demonstrated, illustrating the scope of programmability and customisation, enabled by our multilayered approach.

Diploma thesis deals especially with practical examples on the topic of conics. It is divided into two parts. The first part includes chapters with examples on the topics discussed in the course Geometry I. In the second part affine properties of conics, which can be used in construction tasks, Pascal's theorem and Brianchon's theorem and their use are mentioned. The aim of this thesis is to ilustrate the conics on typical examples for those interested and then to show them the interesting properties, for which there is no space in the course Geometry I.

This diploma thesis is focused on Selected problems in planimetry. The aim of this diploma thesis is description not only planimetric problems and their verification in a dynamic mathematical program GeoGebra, but also presentation of the author after whom it is called. The thesis is illustrated with pictures, which can help the reader to understand the problem and verification. This thesis can be used as a supplement the curriculum in secondary schools, where using dynamic program GeoGebra and subsequent verification may reach a better understanding of the topic.

Submitted by Cássia Santos (cassia.bcufg@gmail.com) on 2017-03-20T12:17:35Z No. of bitstreams: 2 Dissertação - Wesley da Silva Carvalho - 2016.pdf: 2739140 bytes, checksum: 009cb3705c3ac6a28927493419d88e0c (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Approved for entry into archive by Luciana Ferreira (lucgeral@gmail.com) on 2017-03-20T14:06:03Z (GMT) No. of bitstreams: 2 Dissertação - Wesley da Silva Carvalho - 2016.pdf: 2739140 bytes, checksum: 009cb3705c3ac6a28927493419d88e0c (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Made available in DSpace on 2017-03-20T14:06:03Z (GMT). No. of bitstreams: 2 Dissertação - Wesley da Silva Carvalho - 2016.pdf: 2739140 bytes, checksum: 009cb3705c3ac6a28927493419d88e0c (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Previous issue date: 2016-12-09 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES / In this dissertation, we first state Euler's polyhedral formula for a set of points with Euler characteristic 2. We address the two known ways to prove Euler's Theorem: beginning with the classical proof by using Euclidian Geometry and afterwards we take the advantage of Spherical Geometry to give another proof. Furthermore, we address a version of Euler's formula for planar polyhedron, as well as, Pick's formula and the equivalence between Euler and Pick's formula. In the end, we provide application of Euler and Pick's formula, via two pedagogy tools Geoplano and GeoGebra, by giving examples to teach in classroom. / Esta dissertação trata inicialmente da Fórmula de Euler e de sua validade para os conjuntos de pontos com característica de Euler igual a 2. São feitas duas demonstrações da Fórmula de Euler, uma utilizando conceitos de Geometria Euclidiana e uma outra via Geometria Esférica, além da apresentação de uma versão para poliedros planos da Fórmula de Euler. Posteriormente, é apresentada a Fórmula de Pick para o cálculo de áreas de polígonos simples reticulados e sua relação de equivalência com a Fórmula de Pick para poliedros planos. Finalmente mostramos duas possibilidades de trabalho com a Fórmula de Pick, no Geoplano e no software GeoGebra.

In this thesis we summarise several results in the literature which show the approximation capabilities of multilayer feedforward artificial neural networks. We show that multilayer feedforward artificial neural networks are capable of approximating continuous and measurable functions from Rn to R to any degree of accuracy under certain conditions. In particular making use of the Stone-Weierstrass and Hahn-Banach theorems, we show that a multilayer feedforward artificial neural network can approximate any continuous function to any degree of accuracy, by using either an arbitrary squashing function or any continuous sigmoidal function for activation. Making use of the Stone-Weirstrass Theorem again, we extend these approximation capabilities of multilayer feedforward artificial neural networks to the space of measurable functions under any probability measure.

No description available.

Automated Theorem Provers (ATP) are software programs which carry out inferences over logico-mathematical systems, often with the goal of finding proofs to some given theorem. ATP systems are enormously powerful computer programs, capable of solving immensely difficult problems. Currently, many automated theorem provers exist like E, vampire, SPASS, ACL2, Coq etc. However, all the available theorem provers have some common problems: (1) Current ATP systems tend not to try to find proofs entirely on their own. They need help from human experts to supply lemmas, guide the proof, etc. (2) There is not a single proof system available which provides fully automated platforms for both First Order Logic (FOL) and other Higher Order Logic (HOL). (3) Finally, current proof systems do not have an easy way to quickly deploy and reason over new logical systems, which a logic researcher may want to test. In response to these problems, I introduce the MATR framework. MATR is a platform-independent, codelet-based (independently operating processes) proof system with an easy-to-use Graphical User Interface (GUI), where multiple codelets can be selected based on the formal system desired. MATR provides a platform for different proof strategies like deduction and backward reasoning, along with different formal systems such as non-classical logics. It enables users to design their own proof system by selecting from the list of codelets without needing to write an ATP from scratch.