No description available.

No description available.

We present SetPad, a new application prototype that lets computer science students explore discrete math problems by sketching set expressions using pen-based input. Students can manipulate the expressions interactively with the tool via pen or multi-touch interface. Likewise, discrete mathematics instructors can use SetPad to display and work through set problems via a projector to better demonstrate the solutions to the students. We discuss the implementation and feature set of the application, as well as results from both an informal perceived usefulness evaluation for students taking a computer science foundation exam in addition to a formal user study measuring the effectiveness of the tool when solving set proof problems. The results indicate that SetPad was well received, allows for efficient solutions to proof problems, and has the potential to have a positive impact when used as as an individual student application or an instructional tool.

We discuss explanations in Description Logics (DLs), a family of logics used for knowledge representation. Initial work on explaining consequences for DLs had focused on justifications, which are minimal subsets of axioms that entail the consequence. More recently, it was proposed that proofs can provide more detailed information about why a consequence follows. Moreover, several measures have been proposed to estimate the comprehensibility of justifications and proofs, for example, their size or the complexity of logical expressions. In this paper, we analyze the connection between these measures, e.g. whether small justifications necessarily give rise to small proofs. We use a dataset of DL proofs that was constructed last year based on the ontologies of the OWL Reasoner Evaluation 2015. We find that, in general, less complex justifications indeed correspond to less complex proofs, and discuss some exceptions to this rule.

We present an Ethash-based blockchain relay that utilizes Off-Chain Computation (OCC) to validate block headers on-chain. Current work compromises on fundamental ideas of the blockchain concept: they either require a centralized entity, require a centralized Trusted Third Party (TTP) or are built on economic assumptions. That way, they try to circumvent the on-chain cost-heavy Ethash computation. We utilize Zero Knowledge Proofs (ZKPs) to outsource the Ethash validation to an Off-Chain Computation Framework (OCCF) and only verify the validity of the OCC on-chain. The required dataset for the Ethash validation is inserted into a merkle tree for computational feasibility. Additionally, we validate multiple block headers in batches to further minimize on-chain costs. The on-chain costs of our batch validation mechanism are minimal and constant since only the proof of an OCC is verified on-chain. Through merkle proofs we enable the efficient inclusion of intermediary block headers for any submitted batch. The OCC is feasible on average consumer hardware specifications. Our prototype verifies 5 block headers in a single proof using the ZoKrates framework. Compared to current approaches we only use 3.3% of the gas costs resulting in a highly scalable alternative that is trustless, distributed and has no economic assumptions. For future work, we propose to distribute the computational overhead of computing Ethash inside a ZKP through an off-chain distribution module. This is because we rely on the concurrent execution of the OCC by at least 36 active participants to catch up with the current state of the relay’s blockchain. / Vi presenterar ett Ethash-baserat blockchain-relä som använder sig av Off-Chain Computation (OCC) att validera blockhuvuden i kedjan. Nuvarande arbete kompromissar med grundläggande idéer om blockchain-konceptet: de kräver antingen en centraliserad enhet, kräver en centraliserad Trusted Third Party (TTP) eller bygger på ekonomiska antaganden. På så sätt försöker de kringgå den kostnadstunga Ethash-beräkningen på kedjan. Vi använda Zero Knowledge Proof (ZKP) för att lägga ut Ethash-valideringen på en Off-Chain Computation Framework (OCCF) och verifiera endast giltigheten av OCC på kedjan. Den nödvändiga datamängden för Ethash-valideringen är infogas i ett merkleträd för beräkningsmöjlighet. Dessutom validerar vi flera blockhuvuden i omgångar för att ytterligare minimera kostnader i kedjan. På-kedjan kostnaderna för vår batchvalideringsmekanism är minimala och konstanta eftersom endast bevis på en OCC verifieras i kedjan. Genom merkle proofs möjliggör vi det effektiva inkludering av mellanliggande blockrubriker för alla inlämnade partier. OCC är genomförbart i genomsnitt konsumenthårdvaruspecifikationer. Vår prototyp verifierar 5 blockhuvuden i ett enda bevis med hjälp av ZoKrates-ramverket. Jämfört med nuvarande tillvägagångssätt vi använder bara 3,3% av gaskostnaderna vilket resulterar i ett mycket skalbart alternativ dvs förtroendelös, distribuerad och har inga ekonomiska antaganden. För framtida arbete, föreslår vi för att distribuera beräkningsoverheaden för beräkning av Ethash inuti en ZKP genom en distributionsmodul utanför kedjan. Detta beror på att vi skulle förlita oss på det samtidiga utförandet av OCC med minst 36 aktiva deltagare för att komma ikapp med det aktuella tillståndet för reläets blockkedja.

<p>Proofs are notoriously difficult. While the challenges students face when working on proofs are well-documented, more research is needed on what students do when working on proofs, especially in the context of linear algebra. My research focuses on student work on proofs in linear algebra through the lens of Tall's worlds of mathematics: the embodied world, the symbolic world, and the formal world. The embodied world consists of graphs, diagrams, and their properties. The symbolic world contains operations, formulas, and calculations. The formal world consists of axioms, formal definitions, and formal proofs. I conducted task-based interviews with linear algebra students in which they determined if given proofs were valid and then constructed their own proofs for different statements. In different interviews, I encouraged participants to use different worlds of mathematics. Through this study, I hoped to gain some understanding of how approaches to proof constructions and validations within the different worlds of mathematics affect students' personal proof constructions and validations. I also sought to understand what participants viewed as challenging or helpful about each world of mathematics with regards to proofs.</p> <p><br></p> <p>I found that participants often chose a world of mathematics based on the given topic rather than their preferred world or my encouragement to use a given world. Encouraging participants to use the embodied world resulted in their using generic examples. Encouraging participants to use the symbolic or formal worlds had little effect, likely due to participants' views of the symbolic and formal worlds which differed from my views of the symbolic and formal worlds. Participants said the embodied world was helpful for developing understanding, but felt limited by its specificity. A challenge of the symbolic world was the level of precision needed and the large number of variables. Participants viewed the formal world as helpful for proofs and its generality, but logic was a challenge. Reflecting on the study, participants said that the three-world framework was helpful for organizing their thoughts when working on problems.</p>

Le but de cette thèse est de spécifier et prouver des programmes avec pointeurs, tels que des programmes C, en utilisant des techniques de raffinement. L’approche proposée permet de faire un compromis entre les techniques complexes qui existent dans la littérature et ce qui est utilisable dans l’industrie, en conciliant légèreté des annotations et restrictions sur les alias. Nous définissons, dans un premier temps, un langage d’étude, qui s’inspire du langage C, et dans lequel le seul type de données mutable possible est le type des structures, auquel on accède uniquement à travers des pointeurs. Afin de structurer nos programmes, nous munissons notre langage d’une notion de module et des concepts issus de la théorie du raffinement tels que les variables abstraites que nous formalisons par des champs modèle, et les invariants de collage. Ceci nous permet d’écrire des programmes structurés en composants. L’introduction des invariants de données dans notre langage soulève des problématiques liées au partage de pointeurs. En effet, en cas d’alias, on risque de ne plus pouvoir garantir la validité de l’invariant de données d’une structure. Nous interdisons, alors l’aliasing (le partage de référence) dans notre langage. Pour contrôler les accès à la mémoire, nous définissons un système de type, basé sur la notion de régions. Cette contribution s’inspire de la théorie du raffinement et a pour but, de rendre les programmes les plus modulaires possible et leurs preuves les plus automatiques possible. Nous définissons, sur ce langage, un mécanisme de génération d’obligations de preuve en proposant un calcul de plus faible précondition incorporant du raffinement. Nous prouvons ensuite, la correction de ce mécanisme de génération d’obligations de preuve par une méthode originale, fondée sur la notion de sémantique bloquante, qui s’apparente à une preuve de type soundness et qui consiste donc, à prouver la préservation puis le progrès de ce calcul. Nous étendons, dans un deuxième temps, notre langage en levant partiellement la restriction liée au partage de références. Nous permettons, notamment, le partage de références lorsqu’aucun invariant de données n’est associé au type structure référencé. De plus, nous introduisons le type des tableaux, ainsi que les variables globales et l’affectation qui ne font pas partie du langage noyau. Pour chacune des extensions citées ci-dessus, nous étendons la définition et la preuve de correction du calcul de plus faible précondition en conséquence. Nous proposons enfin, une implantation de cette approche sous forme d’un greffon de Frama-C (http://frama-c.com/). Nous expérimentons notre implantation sur des exemples de modules implantant des structures de données complexes, en particulier des défis issus du challenge VACID0 (http://vacid. codeplex.com/), à savoir les tableaux creux (Sparse Array) et les tas binaires. / The purpose of this thesis is to specify and prove programs with pointers, such as C programs, using refinement techniques. The proposed approach allows a compromise between the complexe methods that exist in the literature and what is used in industry, reconciling lightness annotations and restrictions on the alias. We define, firstly, a language study, based on the C language, in which the only type of mutable data allowed is the type of structures, which can be accessed only through pointers. In order to structure our programs, we bring our language with a module notion and concepts issue from a refinement theory such as abstract variables that we formalize by model fields and gluing invariants. This allows us to write programs structured by components. Introducing invariants in our language raises issues related to aliasing. Indeed, in presence of alias, we might not be able to guarantee the validity of the invariant data structure. We forbid then the aliasing in our language. To control memory access, we define a type system based on the concept of regions. This contribution is based on the theory and refinement. It aims to make programs as modular as possible and proofs as automatic as possible. We define on this language, a mechanism for generation of proof obligations by proposing a weakest precondition calculus incorporating refinement. Next we prove the correction of this proof obligations generation mechnaism by an original method based on the concept of blocking semantic, which is similar to a proof of type soundness, and consists therefore, to proove the preservation and the progress of the defined calculus. Secondly, we extend our language by, partially, lifting the restrictions related to aliasing. We allow, in particular, sharing when no invariant is associated to the referenced data structure. In addition, we introduce the type of arrays, global variables, and assignment that are not part of the core language. For each of the extensions mentioned above, we extend the definition and correctness proof of the weakest precondition calculus accordingly. Finally, we propose an implementation of this approach as a Frama-C plugin(http ://frama-c.com/). We experimente our implantation on examples of modules implementing complex data structures, especially the challenges from the challenge VACID0 (http ://vacid. Codeplex.com /), namely sparse srrays and binary heaps.

Made available in DSpace on 2016-04-27T16:57:23Z (GMT). No. of bitstreams: 1 Ednaldo Jose Leandro.pdf: 2692205 bytes, checksum: 44f6a076945d6ba25a67751c3c128be8 (MD5) Previous issue date: 2012-11-09 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / Through a study conducted with five teachers of municipal schools of São Paulo, a survey was carried out which knowledge is mobilized by them, when the focus is on mathematical proofs in elementary school. The text portrays the motivations and obstacles encountered by teachers in developing classroom issues related to mathematical proofs, as well as its functions and typologies aimed. For the development of the research, we used the case study and theoretical reference, the following works: Tardif, on teacher knowledge, the types and functions of mathematical proofs of Balacheff and de Villiers, respectively. The following instruments were used to collect data: direct observation, field notes, interviews, and survey activities. The results point to the mobilization of some knowledge, namely: Curriculum, Experiential and Disciplinary. It was also found that teachers perceive the development of mathematical proofs as a process, considering them an important element to make students develop the habit of presenting justifications for their elaborations. Knowing to do an exam was pointed as a skill to be acquired relevant not only for mathematics, but also for the life of apprentice after school, besides being an opportunity to realize the structure, beauty and connections of mathematical ideas. The productions of mathematical proofs, prepared by students, are identified by teachers as being predominantly pragmatic, at this level of education, and used to explain the function and hence to convince / Por meio de um levantamento realizado junto a cinco professores da rede municipal de ensino de São Paulo, realizou-se um estudo sobre saberes mobilizados por eles, quando o foco são as provas matemáticas no Ensino Fundamental. O texto retrata as motivações e os obstáculos encontrados pelos docentes ao desenvolverem em sala de aula assuntos relacionados às provas matemáticas, bem como suas funções e tipologias almejadas. Para o desenvolvimento da pesquisa, utilizou-se o estudo de caso e, como referencial teórico, os seguintes trabalhos: Tardif, sobre os saberes docentes; as tipologias e funções das provas matemáticas, de Balacheff e de Villiers, respectivamente. Foram utilizados os seguintes instrumentos para a coleta de dados: observação direta, anotações de campo, entrevistas, atividades e questionário. Os resultados obtidos apontam para a mobilização de alguns saberes, quais sejam: Curriculares, Experienciais e Disciplinares. Constatou-se ainda que os professores percebem a elaboração das provas matemáticas como um processo, considerando-as um importante elemento para fazer os alunos desenvolverem o hábito de apresentar justificativas para suas elaborações. Saber realizar uma prova foi apontado como uma habilidade relevante a ser adquirida não só para a matemática, como também para a vida do aprendiz após a escola, além de ser uma oportunidade para perceberem a estrutura, a beleza e as conexões das ideias matemáticas. As produções das provas matemáticas, elaboradas pelos discentes, são identificadas pelos professores como sendo predominantemente pragmáticas, nesse nível de ensino, e utilizadas com a função de explicar e, consequentemente, de convencer

Made available in DSpace on 2016-04-27T16:57:48Z (GMT). No. of bitstreams: 1 EDM - Silviane Rigolon Luis.pdf: 17965286 bytes, checksum: bdfb61396b23d026c568f6ff49b68f22 (MD5) Previous issue date: 2006-10-16 / Secretaria da Educação do Estado de São Paulo / The aim of this research is to investigate how the concept of similar figures can be presented in a significant and motivate way to the students attending the first grade of Brazilian high school system, so that the proof can be an integrant part of this process. We tried to answer the research questions: How is the transition from concrete geometry to space-graphic geometry within the context of similar figures? How does the passing of empirical validations to the deductive occurs in this context? For this, using the Didactic Engineering methodology, we developed a didactic sequence composed by three blocks, in the first and second ones; we worked with empirical validations, using concrete materials in a computerized environment and in the third one with deductive validations using paper and pencil. In our research we used the theoretical presuppositions of Parsysz to the Geometry teaching, where he emphasizes four stages of the development of geometric thought; The Balacheff s ideas about proofs validations processes, are distinguished the pragmatic proofs and the intellectual proof and with the ideas from Freudenthal that proposes for the teaching of the demonstration a local organization. The results of the experimentation aim to evidences of the concrete geometry with the manipulation of many objects stimulated the students in the investigation process and discover regularities that lead them to the idea of similarity concept as well, contributing to the acknowledgement of implicit properties in the figures presented by the dynamism of the Cabri-Géomètre software. Besides, the work done with the empiric validations was important for the students learn the concept of similarity, awakening them to the importance of justify their results and preparing them to the process of deducting validations, given that in this process we can observe an evolution in the structures of the presented proofs / O objetivo desta pesquisa é investigar como o conceito de figuras semelhantes pode ser apresentado de maneira significativa e motivadora a alunos da 1ª série do Ensino Médio, de modo que a prova seja parte integrante desse processo. Procuramos responder às questões de pesquisa: Como se dá a transição da geometria concreta para a espaço-gráfica no contexto das figuras semelhantes? Como ocorre a passagem das validações empíricas para as dedutivas nesse contexto? Para isto, por meio da metodologia da Engenharia Didática, desenvolvemos uma seqüência didática formada por três blocos, sendo que no primeiro e segundo trabalhamos com validações empíricas, utilizando materiais concretos e um ambiente informatizado e, no terceiro bloco com validações dedutivas, utilizando o papel e lápis. Empregamos em nossa pesquisa, os pressupostos teóricos de Parsysz para o ensino da Geometria, onde ele destaca quatro etapas do desenvolvimento do pensamento geométrico; as idéias de Balacheff sobre processos de validações de provas, destacando-se as provas pragmáticas e a prova intelectual e com as idéias de Freudenthal que propõe para o ensino da demonstração uma organização local. Os resultados da experimentação apontam indícios que a geometria concreta com a manipulação de vários objetos estimulou os alunos no processo de investigação e a descobrir regularidades que os levassem à idéia do conceito de semelhança, contribuindo assim, no reconhecimento de propriedades implícitas nas figuras dadas pelo dinamismo do software Cabri-Géomètre. Além disso, o trabalho feito com as validações empíricas foi importante para que os alunos se apropriassem do conceito de semelhança, despertando neles a importância de justificar os seus resultados e preparando-os para o processo das validações dedutivas, sendo que neste processo observa-se uma evolução na estrutura das provas apresentadas

This thesis consists of an introduction and five papers concerning different numerical and mathematical aspects of viscous shocks. Hyperbolic conservation laws are used to model wave motion and advect- ive transport in a variety of physical applications. Solutions of hyperbolic conservation laws may become discontinuous, even in cases where initial and boundary data are smooth. Shock waves is one important type of discontinu- ity. It is also interesting to study the corresponding slightly viscous system, i.e., the system obtained when a small viscous term is added to the hyper- bolic system of equations. By a viscous shock we denote a thin transition layer which appears in the solution of the slightly viscous system instead of a shock in the corresponding purely hyperbolic problem. A slightly viscous system, a so called modified equation, is often used to model numerical solutions of hyperbolic conservation laws and their beha- vior in the vicinity of shocks. Computations presented elsewhere show that numerical solutions of hyperbolic conservation laws obtained by higher order accurate shock capturing methods in many cases are only first order accurate downstream of shocks. We use a modified equation to model numerical solu- tions obtained by a generic second order shock capturing scheme for a time dependent system in one space dimension. We present analysis that show how the first order error term is related to the viscous terms and show that it is possible to eliminate the first order downstream error by choosing a special viscosity term. This is verified in computations. We also extend the analysis to a stationary problem in two space dimensions. Though the technique of modified equation is widely used, rather little is known about when (for what methods etc.) it is applicable. The use of a modified equation as a model for a numerical solution is only relevant if the numerical solution behaves as a continuous function. We have experimentally investigated a range of high resolution shock capturing methods. Our experiments indicate that for many of the methods there is a continuous shock profile. For some of the methods, however, this not the case. In general the behavior in the shock region is very complicated. Systems of hyperbolic conservation laws with solutions containing shock waves, and corresponding slightly viscous equations, are examples where the available theoretical results on existence and uniqueness of solutions are very limited, though it is often straightforward to find approximate numerical solu- tions. We present a computer-assisted technique to prove existence of solu- tions of non-linear boundary value ODEs, which is based on using an approx- imate, numerical solution. The technique is applied to stationary solutions of the viscous Burgers' equation.We also study a corresponding method suggested by Yamamoto in SIAM J. Numer. Anal. 35(5)1998, and apply also this method to the viscous Burgers' equation.