This thesis seeks to shed further light on how blockchain technology has fostered increases in efficiency at an overall level looking specifically at the Ethereum network, and a continued analysis of its evolving state. A network at the forefront of blockchain technology and smart contract utilization. Firstly, we introduce blockchain technology itself and the various facets of the technology, including consensus protocols, smart contracts and smart contract applications. Subsequently, we further analyse and showcase how blockchain technology has developed in efficiency over its maturation recently. Through the employment of various econometric models and strong discussion promotes insights to the key metrics of the Ethereum network. Finally, we explore whether we are able to note these changes over time and look to the future of blockchain technology. Not only to shed light on how this evolving state will continue to cultivate but also detail the other necessary advances needed to continue this growth.

La confiance formelle en une propriété abstraite provient de l'existence d'une preuve de sa correction, qu'il s'agisse d'un théorème mathématique ou d'une qualité du comportement d'un logiciel ou processeur. Il existe de nombreuses définitions différentes de ce qu'est une preuve, selon par exemple qu'elle est écrite soit par des humains soit par des machines, mais ces définitions sont toutes concernées par le problème d'établir qu'un document représente en fait une preuve correcte. Le cadre des Certificats de Preuve Fondamentaux (Foundational Proof Certificates, FPC) est une approche proposée récemment pour étudier ce problème, fondée sur des progrès de la théorie de la démonstration pour définir la sémantique des formats de preuve. Les preuves ainsi définies peuvent être vérifiées indépendamment par un noyau vérificateur de confiance codé dans un langage de programmation logique. Cette thèse étend des résultats initiaux sur la certification de preuves du premier ordre en explorant plusieurs dimensions logiques essentielles, organisées en combinaisons correspondant à leur usage en pratique: d'abord, la logique classique sans points fixes, dont les preuves sont générées par des démonstrateurs automatiques de théorème; ensuite, la logique intuitionniste avec points fixes et égalité,dont les preuves sont générées par des assistants de preuve. Les certificats de preuve ne se limitent pas comme précédemment à servir de représentation des preuves complètes pour les vérifier indépendamment. Leur rôle s'étend pour englober des transformations de preuve qui peuvent enrichir ou compacter leur représentation. Ces transformations peuvent rendre des certificats plus simples opérationnellement, ce qui motive la construction d'une suite de vérificateurs de preuve de plus en plus fiables et performants. Une autre nouvelle fonction des certificats de preuve est l'écriture d'aperçus de preuve de haut niveau, qui expriment des schémas de preuve tels qu'ils sont employés dans la pratique des mathématiciens, ou dans des techniques automatiques comme le property-based testing. Ces développements s'appliquent à la certification intégrale de résultats générés par deux familles majeures de démonstrateurs automatiques de théorème, utilisant techniques de résolution et satisfaisabilité, ainsi qu'à la création de langages programmables de description de preuve pour un assistant de preuve. / Formal trust in an abstract property, be it a mathematical result or a quality of the behavior of a computer program or a piece of hardware, is founded on the existence of a proof of its correctness. Many different kinds of proofs are written by mathematicians or generated by theorem provers, with the common problem of ascertaining whether those claimed proofs are themselves correct. The recently proposed Foundational Proof Certificate (FPC) framework harnesses advances in proof theory to define the semantics of proof formats, which can be verified by an independent and trusted proof checking kernel written in a logic programming language. This thesis extends initial results in certification of first-order proofs in several directions. It covers various essential logical axes grouped in meaningful combinations as they occur in practice: first,classical logic without fixed points and proofs generated by automated theorem provers; later, intuitionistic logic with fixed points and equality as logical connectives and proofs generated by proof assistants. The role of proof certificates is no longer limited to representing complete proofs to enable independent checking, but is extended to model proof transformations where details can be added to or subtracted from a certificate. These transformations yield operationally simpler certificates, around which increasingly trustworthy and performant proof checkers are constructed. Another new role of proof certificates is writing high-level proof outlines, which can be used to represent standard proof patterns as written by mathematicians, as well as automated techniques like property-based testing. We apply these developments to fully certify results produced by two families of standard automated theorem provers: resolution- and satisfiability-based. Another application is the design of programmable proof description languages for a proof assistant.

No description available.

Blockchain is a decentralized database that is distributed among a computer network. To enable a smooth decision making process without any authority, different blockchain applications use their own consensus algorithms. The problem is that for a new blockchain application, there is limited aid in deciding which algorithm it should implement. Selecting consensus algorithms is crucial because reaching consensus is the fundamental issue of a decentralized system. Different algorithms are designed with their own advantages and limitations, making it complex to navigate one’s way through a list of consensus algorithms. This thesis attempts to contribute to solving this problem by surveying 15 existing cryptocurrencies’ consensus algorithms used in their blockchain application and then producing a decision tree as the aid for algorithm selection. The top 5 algorithms from each category in Proof of Work (PoW), Proof of Stake (PoS), and Hybrid Proof of Work + Proof of Stake (PoW + PoS) are selected. The research method is qualitative. The study shows that different consensus algorithms often share some properties, but they are usually built to solve the issues of another algorithm, which means they also have their own distinctive advantages. Therefore, the decision tree reveals how these algorithms are logically connected and the key properties blockchain consensus algorithms possess. Based on the result of this thesis, further research can be conducted to include more algorithms in order to make the decision tree more comprehensive. Implementations of these algorithms in similar network setup can also be done to experiment with their claimed properties. The decision tree can be sent to industry for further feedback. / Blockchain är en decentraliserad databas som distribueras i ett datornätverk. För att möjliggöra en smidig beslutsprocess utan någon auktoritet använder olika blockkedjeapplikationer sina egna konsensusalgoritmer. Problemet är att för en ny blockchain-applikation finns det begränsad hjälp för att bestämma vilken algoritm den ska implementera. Att välja konsensusalgoritmer är avgörande eftersom att nå konsensus är den grundläggande frågan för ett decentraliserat system. Olika algoritmer är designade med sina egna fördelar och begränsningar, vilket gör det komplicerat att navigera sig igenom en lista med konsensusalgoritmer. Forskningsmetoden är kvalitativ. Det här dokumentet försöker bidra till att lösa detta problem genom att kartlägga 15 befintliga kryptovalutors konsensusalgoritmer som används i deras blockkedjeapplikation och sedan ta fram ett beslutsträd som hjälp för val av algoritmer. De 5 bästa algoritmerna från varje kategori i Proof of Work (PoW), Proof of Stake (PoS) och Hybrid Proof of Work + Proof of Stake (PoW + PoS) väljs. Studien visar att olika konsensusalgoritmer ofta delar vissa egenskaper, men de är vanligtvis byggda för att lösa problem med en annan algoritm, vilket innebär att de också har sina egna distinkta fördelar. Därför avslöjar beslutsträdet hur dessa algoritmer är logiskt kopplade och de nyckelegenskaper som blockchain konsensusalgoritmer besitter. Baserat på resultatet av denna artikel kan ytterligare forskning utföras för att inkludera fler algoritmer för att göra beslutsträdet mer heltäckande. Implementeringar av dessa algoritmer i liknande nätverksuppsättningar kan också göras för att experimentera med deras påstådda egenskaper. Beslutsträdet kan skickas till industrin för vidare feedback.

While proof and reasoning lie at the core of mathematical practice, how students learn to reason formally and build convincing proofs continues to invite reflection and discussion. To add to this discussion I investigated how three students grew in their conceptions of mathematical induction. While each of the students in the study had different experiences and grew in different ways, the grounded axes (triggering events, personal questions about mathematics, and personal questions about a particular solution) highlighted patterns in the narratives and from these patterns a theoretical perspective emerged. Reflection, both on mathematics in general and about specific problems, was central to students' growth. The personal reflections of students and triggering events influenced each other in the following way. The questions students wondered about impacted which trigger stimulated growth, while triggers caused students to rethink assumptions and reflect on mathematics or specific problems. The reflections that allowed triggers to stimulate growth along with the reflections that were results of triggering events constitute an "investigative orientation." Each narrative reflects a different investigative orientation motivated by different personal needs. These investigative orientations affected what type of knowledge was constructed.

An analysis is presented on the use of a proof-mass actuator as a regenerative force actuator for the mitigation of earthquake disturbances in civil structures. A proof-mass actuator is a machine which accelerates a mass along a linear path. Such actuators can facilitate two-way power flow. In regenerative force actuation, a bi- directional power-electronic drive is used to facilitate power flow both to and from the proof-mass actuator power supply. With proper control system design, this makes it possible to suppress a disturbance on a structure using mostly energy extracted from the disturbance itself, rather than from an external power source. In this study, three main objectives are accomplished. First, a new performance measure, called the "required energy capacity," is proposed as an assessment of the minimum size of the electric power supply necessary to facilitate the power flow required of the closed-loop system for a given disturbance. The relationship between the required energy capacity and the linear control system design, which is based on positive position feedback concepts, is developed. The dependency of the required energy capacity on hybrid realizations of the control law are discussed, and hybrid designs are found which minimize this quantity for specific disturbance characteristics. As the second objective, system identification and robust estimation methods are used to develop a stochastic approach to the performance assessment of structural control systems, which evaluates the average worst-case performance for all earthquakes "similar" to an actual data record. This technique is used to evaluate the required energy capacity for a control system design. In the third objective, a way is found to design a battery capacity which takes into account the velocity rating of the proof-mass actuator. Upon sizing this battery, two nonlinear controllers are proposed which automatically regulate the power flow in the closed-loop system to accommodate a power supply with a finite energy capacity, regardless of the disturbance size. Both controllers are based on a linear control system design. One includes a nonlinearity which limits power flow out of the battery supply. The other includes a nonlinearity which limits the magnitude of the proof-mass velocity. The latter of these is shown to yield superior performance. / Master of Science

No description available.

No description available.

No description available.

This research investigates relationships between undergraduate students' understanding of proof and how this understanding relates to their conceptions of mathematical definitions. Three students in an introductory proofs course were each interviewed three times in order to assess their proof schemes, understand how they think of specific mathematical concepts, and investigate how the students prove relationships between these concepts. This research used theoretical frameworks from both proof and definition literature. Findings show that students' ability or inability to adapt their concept images of the mathematical concepts enhanced and impeded their proof schemes, respectively. / Master of Science