No description available.

No description available.

Thesis (M.S.)--Rochester Institute of Technology, 1994. / Typescript. Includes bibliographical references (leaf [27A]).

This study examines how undergraduate students use hand gestures to offload cognitive demands on their working memory (WM) when they are engaged in three major proving activities: reading, presenting, and constructing proofs of mathematical conjectures. Existing research literature on the role of gesturing in cognitive offloading has been limited to the context of elementary mathematics but has shown promise for extension to the college level. My framework weaves together theoretical constructs from mathematics education and cognitive psychology: gestures, WM, and mathematical proofs. Piagetian and embodied perspectives allow for the integration of these constructs through positioning bodily activity at the core of human cognition. This framework is operationalized through the methodology for measuring cognitive demands of proofs, which is used to identify the set of mental schemes that are activated simultaneously, as well as the places of potential cognitive overload. The data examined in this dissertation includes individual clinical interviews with six undergraduate students enrolled in different sections of the Introduction to Proofs course in Fall 2021 and Spring 2022. Each student participated in seven interviews: two WM assessments, three proofs-based interviews, a stimulated recall interview (SRI), and post-interview assessments. In total, 42 interviews were conducted. The participants' hand gesturing and mathematical reasoning were qualitatively analyzed. Ultimately, students' reflections during SRIs helped me triangulate the initial data findings. The findings suggest that, in absence of other forms of offloading, hand gesturing may become a convenient, powerful, although not an exclusive offloading mechanism: several participants employed alternative mental strategies in overcoming the cognitive overload they experienced. To better understand what constitutes the essence of cognitive offloading via hand gesturing, I propose a typology of offloading gestures. This typology differs from the existing classification schemes by capturing the cognitive nuances of hand gestures rather than reflecting their mechanical characteristics or the underlying mathematical content. Employing the emerged typology, I then show that cognitive offloading takes different forms when students read or construct proofs, and when they present proofs to the interviewer. Finally, I report on some WM-related issues in presenting and constructing proofs that can be attributed to the potential side effects of mathematical chunking. The dissertation concludes with a discussion of the limitations and practical implications of this project, as well as foreshadowing the avenues for future research. / Doctor of Philosophy / In this study, I examined how undergraduate students can rely on their hand gesturing to reduce the cognitive complexity of mathematical proofs. Specifically, I studied gestures produced by students when they are engaged in various kinds of proving activities: reading for comprehension, reading for validation, presenting, and constructing proofs of mathematical conjectures. During the experiments, the participants were not given pencils/paper, calculators, or any other and other figurative materials. Therefore, they had to rely on their imagination, working memory, and hand gestures to make progress on the tasks. Results suggest that students' hand gestures have a beneficial effect in navigating cognitive challenges associated with mathematical proofs. Moreover, I show that this effect takes different forms depending on the proving activity in which the student engages. Finally, I report on some memory-related issues in presenting and constructing proofs. The dissertation concludes with a discussion of the limitations and practical implications of this project, as well as foreshadowing the avenues for future research.

Satisfiability (SAT) solvers are commonly used for a variety of applications, including hardware verification, software verification, theorem proving, debugging, and hard combinatorial problems. These applications rely on the efficiency and correctness of SAT solvers. When a problem is determined to be unsatisfiable, how can one be confident that a SAT solver has fully exhausted the search space? Traditionally, unsatisfiability results have been expressed using resolution or clausal proof systems. Resolution-based proofs contain perfect reconstruction information, but these proofs are extremely large and difficult to emit from a solver. Clausal proofs rely on rediscovery of inferences using a limited number of techniques, which typically takes several orders of magnitude longer than the solving time. Moreover, neither of these proof systems has been able to express contemporary solving techniques such as bounded variable addition. This combination of issues has left SAT solver authors unmotivated to produce proofs of unsatisfiability. The work from this dissertation focuses on validating satisfiability solver output in the unsatisfiability case. We developed a new clausal proof format called DRAT that facilitates compact proofs that are easier to emit and capable of expressing all contemporary solving and preprocessing techniques. Furthermore, we implemented a validation utility called DRAT-trim that is able to validate proofs in a time similar to that of the discovery time. The DRAT format has seen widespread adoption in the SAT community and the DRAT-trim utility was used to validate the results of the 2014 SAT Competition. DRAT-trim uses many advanced techniques to realize its performance gains, so why should the results of DRAT-trim be trusted? Mechanical verification enables users to model programs and algorithms and then prove their correctness with a proof assistant, such as ACL2. We designed a new modeling technique for ACL2 that combines efficient model execution with an agile and convenient theory. Finally, we used this new technique to construct a fast, mechanically-verified validation tool for proofs of unsatisfiability. This research allows SAT solver authors and users to have greater confidence in their results and applications by ensuring the validity of unsatisfiability results. / text

This thesis is on the automation of diagrammatic proofs, a novel approach to mechanised mathematical reasoning. Theorems in automated theorem proving are usually proved by formal logical proofs. However, there are some conjectures which humans can prove by the use of geometric operations on diagrams that somehow represent these conjectures, so called diagrammatic proofs. Insight is often more clearly perceived in these diagrammatic proofs than in the algebraic proofs. We are investigating and automating such diagrammatic reasoning about mathematical theorems. Concrete rather than general diagrams are used to prove ground instances of a universally quantified theorem. The diagrammatic proof in constructed by applying geometric operations to the diagram. These operations are in the inference steps of the proof. A general schematic proof is extracted from the ground instances of a proof. it is represented as a recursive program that consists of a general number of applications of geometric operations. When gien a particular diagram, a schematic proof generates a proof for that diagram. To verify that the schematic proof produces a correct proof of the conjecture for each ground instance we check its correctness in a theory of diagrams. We use the constructive omega-rule and schematic proofs to make a translation from concrete instances to a general argument about the diagrammatic proof. The realisation of our ideas is a diagrammatic reasoning system DIAMOND. DIAMOND allows a user to interactively construct instances of a diagrammatic proof. It then automatically abstracts these into a general schematic proof and checks the correctness of this proof using an inductive theorem prover.

Combinatorial techniques can frequently provide satisfying “explanations” of various mathematical phenomena. In this thesis, we seek to explain a number of well known number theoretic congruences using combinatorial methods. Many of the results we prove involve the Fibonacci sequence and its generalizations.

Interactive theorem proving provides a general approach to modeling and verification of both finite-state and infinite-state systems but requires significant human efforts to deal with many tedious proofs. On the other hand, model-checking is limited to some application domain with small finite-state space. A natural thought for this problem is to integrate these two approaches. To keep the consistency of the integration and ensure the correctness of verification, we suggest to use type theory based theorem provers (e.g. Lego) as the platform for the integration and build a model-checker to do parts of the verification automatically. We formalise a verification system of both CCS and an imperative language in the proof development system Lego which can be used to verify both finite-state and infinite-state problems. Then a model-checker, LegoMC, is implemented to generate Lego proof terras for finite-state problems automatically. Therefore people can use Lego to verify a general problem with some of its finite sub-problems verified by LegoMC. On the other hand, this integration extends the power of model-checking to verify more complicated and infinite-state models as well. The development of automatic techniques and the integration of different reasoning methods would directly benefit the verification community. It is expected that further extension and development of this verification environment would be able to handle real life systems. On the other hand, the research gives us some experiences about how to automate proofs in interactive theorem provers and therefore will improve the usability and applicability of the theorem proving technology.

In this thesis we follow two directions: Zero Knowledge Protocols and the Discrete Logarithm Problem. In each direction we present the necessary background and we give a new approach for some parts of the existing protocols. / The new parts are dedicated to the soundness property of the Schnorr Identification Scheme and to the security of the sum+-Protocol. Since both directions are very well-known and studied in the field of cryptography, they are presented with many details so that the new results are easy to follow. / In writing this thesis we have tried to present the material in a specific order and in a manner easy to read even by beginners in cryptography.

The Grundlagen der Geometrie brought Euclid’s ancient axioms up to the standards of modern logic, anticipating a completely mechanical verification of their theorems. There are five groups of axioms, each focused on a logical feature of Euclidean geometry. The first two groups give us ordered geometry, a highly limited setting where there is no talk of measure or angle. From these, we mechanically verify the Polygonal Jordan Curve Theorem, a result of much generality given the setting, and subtle enough to warrant a full verification. Along the way, we describe and implement a general-purpose algebraic language for proof search, which we use to automate arguments from the first axiom group. We then follow Hilbert through the preliminary definitions and theorems that lead up to his statement of the Polygonal Jordan Curve Theorem. These, once formalised and verified, give us a final piece of automation. Suitably armed, we can then tackle the main theorem.