In this essay the heuristic method of proofs and refutations, as pre- sented in the book Proofs and refutations by Imre Lakatos, is reviewed and discussed. Some background is given of heuristic methodology in contrast to the deductivist method and then Euler’s polyhedron for- mula is presented. Examples of both local and global mathematical monsters are introduced and handled through the application of the historical progression of Cauchy’s proof of Euler’s polyhedron formula. This leads to show the method of lemma-incorporation as the superior approach. The method is presented in the light of Lakatos’ heuristic philosophy, followed by criticism to his method. It is suggested to use Lakatos’ method as an addition to today’s formal mathematics to increase creativity and expand mathematical theorems further. The conclusion is drawn that Lakatos’ method of proofs and refutations is not prefect, but should utilize the existing criticism to be perfected through its own practice.

Security is a major concern is today's online world. As online activities become increasingly sensitive, service providers rely on security protocols to ensure confidentiality, integrity and authentication of their users and data. Greater assurance is provided when these protocols are verified to be correct. Strand Spaces is a method to formally analyze security protocols. The arguments are based on the messages being transmitted and received while assuming that the underlying cryptographic primitives are secure. This thesis demonstrates that the protocols Luau, pwdArmor and Kiwi are secure using Strand Spaces methodology.

Abstract Not Provided. / Thesis / Master of Science (MSc)

Industrial programs written on Programmable Logic Controllers (PLCs) have become an essential component of many modern industries, including automotive, aerospace, manufacturing, infrastructure, and even amusement parks. As these safety-critical systems become larger and more complex, ensuring their continuous error-free operation has become a significant and important challenge. Formal methods are a potential solution to this issue but have traditionally required substantial time and expertise to deploy. This usability issue is compounded by the fact that PLCs are highly proprietary and have substantial licensing costs, making it difficult to learn about or deploy formal methods on them. This thesis presents the OPPP (Open-source Proving of PLC Programs) system as a solution to this usability issue. The OPPP system allows the end-to-end creation and verification of PLC programs from within the development environment. The system is created with an emphasis on being easy to use, with formal constraints presented in English phrases that require no special knowledge to understand. The system uses entirely open-source components, including modified versions of both the OpenPLC development environment and the PLCverif verification platform. The OPPP system is then demonstrated to formalize the requirements of two college-level introductory PLC programming problems. It is further demonstrated to correctly find errors in and verify the correctness of a known good and known bad solution to each problem.

No description available.

The immutability, validity and confidentiality of an audit log is crucial when operating over sensitive data to comply to standard data regulations (e.g., HIPAA). Despite its critical needs, state-of-the-art privacy-preserving audit log schemes (e.g., Ghostor (NSDI '20), Calypso (VLDB '19)) do not fully obtain a high level of privacy, integrity, and immutability simultaneously, in which certain information (e.g., user identities) is still leaked in the log. In this work, we propose Harpocrates, a new privacy-preserving and immutable audit log scheme. Harpocrates permits data store, share, and access operations to be recorded in the audit log without leaking sensitive information (e.g., data identifier, user identity), while permitting the validity of data operations to be publicly verifiable. Harpocrates makes use of blockchain techniques to achieve immutability and avoid a single point of failure, while cryptographic zero-knowledge proofs are harnessed for confidentiality and public verifiability. We analyze the security of our proposed technique and prove that it achieves non-malleability and indistinguishability. We fully implemented Harpocrates and evaluated its performance on a real blockchain system (i.e., Hyperledger Fabric) deployed on a commodity platform (i.e., Amazon EC2). Experimental results demonstrated that Harpocrates is highly scalable and achieves practical performance. / Master of Science / Audit logs are an essential part of data storage systems as they allow to check if the system is working as intended. They are usually maintained on a server, a server with ill intentions can easily modify records of the log and make it appear that the system is working correctly. To store these records in an un-modifiable manner, prior works have leveraged special audit log storing mechanisms for e.g., blockchain due to its immutable nature. However, these works do not focus on the privacy of the records which is a crucial aspect for conforming to certain data regulations like HIPAA. In our work, we propose Harpocrates, an immutable and privacy-preserving audit log platform that supports recording operations (share/access) on sensitive data. Harpocrates leverages blockchain to achieve immutability of the audit log. Harpocrates use specific cryptographic primitives to achieve public verifiability and confidentiality of the audit log. Real world deployment of Harpocrates shows that it is practical and achieves strong security guarantees.

This thesis is a single case study of the introduction and evaluation of new resources and new technologies in higher education; in which e-Proof was chosen as a single case. E-proofs are a multimedia representation of proofs, were created by Alcock (2009), and aimed to help undergraduates to read proofs for better proof comprehension. My thesis aimed to investigate whether the impact of reading such technology-based resource, e-Proofs, on undergraduates proof comprehension was better compared to reading written textbook proofs and if so, then why (or why not). To evaluate the effectiveness of e-Proofs, I used both qualitative and quantitative methods. First I measured undergraduates satisfaction, which is a most common research practice in evaluation studies, by using self-reporting methods such as web-based survey and interviews. A web-based survey and focus-group interviews showed that undergraduates liked to have e-Proofs and they believed that e-Proofs had positive impact on their proof comprehension. However, their positive views on e-Proofs did not evidence the educational impact of e-Proofs. I conducted an interview with Alcock for better understanding of her intentions of creating e-Proof and her expectations from it. Next, I conducted the first experiment which compared the impact of reading an e-Proof with a written textbook proof on undergraduates proof comprehension. Their comprehension was measured with an open-ended comprehension test twice immediately after reading the proof and after two weeks. I found that the immediate impact of reading an e-Proof and a textbook proof were essentially the same, however the long term impact of reading an e-Proof was worse than reading a textbook proof (for both high and low achieving undergraduates). This leads to the second experiment in which I investigated how undergraduates read e-Proofs and textbook proofs. In the second experiment, participants eye-movements were recorded while read- ing proofs, to explore their reading comprehension processes. This eye-tracking experiment showed that undergraduates had a sense of understanding of how to read a proof without any additional help. Rather, additional help allowed them to take a back seat and to devote less cognitive effort than they would otherwise. Moreover, e-Proofs altered undergraduates reading behaviours in a way which can harm learning. In sum, this thesis contributes knowledge into the area of reading and compre- hending proofs at undergraduate level and presents a methodology for evaluation studies of new pedagogical tools.

Este trabalho pretende levantar questões relativas ao uso e aos efeitos provocados pela utilização de estratégias argumentativas no discurso. Para exemplificar a importância de tais estratégias na construção da significação no uso da linguagem, elegemos como objeto de análise um discurso em especial, o pedagógico, e, dentro dele, optamos pelo estudo das avaliações no ensino superior, especificamente, das provas escritas, representantes do poder da linguagem no processo ensino/aprendizagem e do conflito existente na relação professor-aluno. A partir deste recorte metodológico, repensaremos, em especial, as figuras de argumentação e retórica, estratégias discursivas inesperadas - causam o efeito de surpresa no discurso - e privilegiadas, na medida em que permitem analisar não apenas o fazer persuasivo do enunciador, bem como a construção do ethos dos sujeitos envolvidos na situação comunicativa. Acreditamos que em todos os tipos de discurso a linguagem pode ser utilizada não apenas para convencer um interlocutor, mas para persuadi-lo. Tal fato nos leva a buscar no discurso do aluno quais são as estratégias utilizadas para este fim, e a tentar identificá-las dentro de um quadro teórico e metodológico discursivo. Para tanto, empreendemos um retorno às origens histórico-pedagógicas da avaliação, recorremos à Retórica Aristotélica e às Neo-Retóricas, à Teoria Semiótica de Greimas, à Teoria dos Gêneros do Discurso de Bakhtin, e a estudos sociossemióticos e discursivos que privilegiam questões como a construção da identidade individual e social dos sujeitos por meio do discurso e os aspectos interacionais envolvidos nas relações sociais. / The proposal of this work is to produce questions about the use of argumentatives strategies in the discourse, as well as questions about the effect of this use. To analyze the importance of these strategies during the construction of the meaning, we choose a special type of discourse, the pedagogical discourse, and inside of it, we have decided to analyze the proofs in the university, more specifically, the written proofs, because they are representative of the language´s power in the education and learning process and of the existing conflict between professor and students. From this method, we will analyze, in special, the argument and rhetoric figures and the unexpected and privileged discoursive strategies - because they cause surprise in the discourse and allow to analyze the construction of the ethos of the involved people in the communication situation. We believe that the language can be used to persuade an interlocutor and to convince him, not importing the type of discourse used. This fact makes us to search in the students´ discourse the used strategies and trying to identify them into inside of a theoretical, methodologic and discoursive frame. With this objective, we made a visit to the historical and pedagogical origins of the proofs, we appeal to the Aristotelian Rhetoric and the Neo-Rhetorical, to the Greimas´ Semiotics Theory and the Bakhtin´s work, and to the sociossemiotic and discoursive studies that privilege questions, as the construction, through the discourse, of the individual and social identity of the people, and aspects that are involved in the social relations.

[pt] Na antologia que M.E. Szabo realizara dos trabalhos de Gentzen e publicara em 1969 se transcrevem, em um apêndice, algumas passagens apresentadas por Bernays ao editor pertencentes a uma primeira prova de consistência para a Aritmética de Peano realizada por Gentzen que não tinha sido publicada até então. À diferença das outras provas de consistência realizadas por Gentzen e já conhecidas na década de trinta, esta prova não utiliza o procedimento de indução transfinita até e0. Ao contrário, baseia-se na definição de um processo de redução de seqüentes que se associa sistematicamente a todo seqüente derivável permitindo reconhecê-lo como verdadeiro. Nós reconstruímos essa prova realizando algumas variações e estudamos o modo pelo qual a técnica principal utilizada (a definição do processo de redução de seqüentes) pode ser vista em relação a resultados da lógica clássica de primeira ordem tais como provas de completude. A parte central da nossa dissertação é a realização de uma versão desta prova de consistência para um sistema formal para a Aritmética de Heyting. / [en] In the antology of Gentzens works made by M.E.Szabo and published in 1969, we find out in an appendix, some passages presented by Bernays to the editor. These texts belong to a first proof of Peanos Arithmetic consistency that Gentzen did not publish. In a different way from the other proofs of consistency made by Gentzen and already known in the thirties, this proof does not use the procedure of transfinite induction up to e0. On the contrary, it is based on the definition of a reduction process for sequents that is systematically associated to every derivable sequent allowing us to recognize it as a true sequent. We reconstructed this proof making some variations and we studied how the main technique used (the definition of the reduction process) could be seen in relation with other results of first order logic like proofs of completness. The main part of our dissertation is another version of this consistency proof for a formal system for Heyting Arithmetic.

O avanço das tecnologias vem sendo impulsionado por ferramentas como internet móvel, touchscreen, wirelles, dentre outras, possibilitando que o manuseio com auxílio destes dispositivos seja cada vez mais fácil e intuitivo, não necessitando de um tutorial ou mesmo de uma explicação completa por parte dos usuários para acessá-los. Desta forma, qualquer pessoa que tenha computador, celular, smartphone ou tablet conectado à internet, poderá produzir um vídeo, um texto ou uma imagem e compartilhá-los na rede. Os meios de comunicação e informação tornam-se maiores e menores ao mesmo tempo. Por meio de uma única ferramenta portátil, que comporta diversas mídias é possível que os conteúdos educacionais, e não somente conteúdos, mas informações, revistas, artigos possam ser acessados a qualquer tempo e em qualquer lugar. Diante deste novo paradigma, estar atento à forma com que as tecnologias estão sendo utilizadas pelas crianças, e como elas vêm percebendo este mundo digital se faz necessário. A presente pesquisa tem por objetivo observar e verificar como as crianças de 7 meses a 7 anos de idade estão se apropriando das tecnologias digitais, bem como percebem os atrativos oferecidos por elas. Adotou-se como aporte teórico a Epistemologia Genética de Piaget e suas principais obras sobre o desenvolvimento infantil, para melhor compreender os processos de desenvolvimento da inteligência da criança. Para tanto, a metodologia utilizada foi a aplicação de provas Piagetianas e, posteriormente, a realização desta mesma prova com o uso de recurso tecnológico. Durante estas atividades, foi utilizado o Método Clínico, já a análise das observações e interações das crianças, foi fundamentada a partir de obras de Piaget em que o desenvolvimento da inteligência infantil era abordada. Durante a pesquisa, foi possível observar o nítido interesse das crianças pelos aparelhos e pelas tecnologias digitais. As tecnologias digitais possibilitaram que as crianças realizassem constatações mais aprofundadas do que nas provas Piagetianas, pois os recursos tecnológicos apresentados envolveram diferentes sentidos, bem como proporcionaram que elas descobrissem coisas sem terem que fazer um esforço tão grande como quando trabalham com objetos concretos. O mundo virtual mostrou-se mais atrativo, porque possibilitou às crianças ter a oportunidade de aprender de modo não-formal, e sim fazendo e descobrindo sem seguir uma sequência definida. / The advancement of technologies has been driven by tools such as mobile internet, touchscreen, wirelles, among others, making it easier and more intuitive to handle these devices without requiring a tutorial or even a full explanation for the users to access them. Anyone with a computer, cell phone, smartphone or tablet connected to the internet can produce a video, text or image and share them on the web. Media and information become larger and smaller at the same time. With a single portable tool that contains several media, it is possible that educational content, educational content, general information, magazines, articles can be accessed anytime, anywhere. Facing this new paradigm, being aware of how technologies are being used by children and how they are perceiving this digital world becomes necessary. The present research aims to observe and verify how children from 7 months to 7 years of age are appropriating digital technologies as well as perceiving the attractions offered by them. It was adopted as a theoretical contribution the Piaget's Genetic Epistemology and his main works on child development, in order to better understand the processes of child intelligence development. For this, the methodology used was the application of Piagetian tests and, later, the accomplishment of this same test with the use of technological resources. During these activities, the Clinical Method was used. The analysis of the observations and children‟s interactions was based on works of Piaget in which the development of the child intelligence was approached. During the research, it was possible to observe the clear interest of the children by the devices and the digital technologies. Digital technologies made it possible for children to make more in-depth findings than in Piagetian tests because the technological features presented involved different senses as well as allowing them to discover things without having to make as much effort as when working with concrete objects. The virtual world proved to be more attractive because it enabled children to have the opportunity to learn in a non-formal way, but by doing and discovering without following a definite sequence.