This thesis presents an investigation into the structure of proof in non-standard analysis using proof-planning. The theory of non-standard analysis, developed by Robinson in the 1960s, offers a more algebraic way of looking at proof in analysis. Proof-planning is a technique for reasoning about proof at the meta-level. In this thesis, we use it to encapsulate the patterns of reasoning that occur in non-standard analysis proofs. We first introduce in detail the mathematical theory and the proof-planning architecture. We then present our research methodology, describe the formal framework, which includes an axiomatisation, and develop suitable evaluation criteria. We then present our development of proof-plans for theorems involving limits, continuity and differentiation. We then explain how proof-planning applies to theorems which combine induction and non-standard analysis. Finally we give a detailed evaluation of the results obtained by combining the two attractive approaches of proof-planning and non-standard analysis, and draw conclusions from the work.

This paper introduces Denotational Proof Languages (DPLs). DPLs are languages for presenting, discovering, and checking formal proofs. In particular, in this paper we discus type-alpha DPLs---a simple class of DPLs for which termination is guaranteed and proof checking can be performed in time linear in the size of the proof. Type-alpha DPLs allow for lucid proof presentation and for efficient proof checking, but not for proof search. Type-omega DPLs allow for search as well as simple presentation and checking, but termination is no longer guaranteed and proof checking may diverge. We do not study type-omega DPLs here. We start by listing some common characteristics of DPLs. We then illustrate with a particularly simple example: a toy type-alpha DPL called PAR, for deducing parities. We present the abstract syntax of PAR, followed by two different kinds of formal semantics: evaluation and denotational. We then relate the two semantics and show how proof checking becomes tantamount to evaluation. We proceed to develop the proof theory of PAR, formulating and studying certain key notions such as observational equivalence that pervade all DPLs. We then present NDL, a type-alpha DPL for classical zero-order natural deduction. Our presentation of NDL mirrors that of PAR, showing how every basic concept that was introduced in PAR resurfaces in NDL. We present sample proofs of several well-known tautologies of propositional logic that demonstrate our thesis that DPL proofs are readable, writable, and concise. Next we contrast DPLs to typed logics based on the Curry-Howard isomorphism, and discuss the distinction between pure and augmented DPLs. Finally we consider the issue of implementing DPLs, presenting an implementation of PAR in SML and one in Athena, and end with some concluding remarks.

This paper presents an algorithm for simplifying NDL deductions. An array of simplifying transformations are rigorously defined. They are shown to be terminating, and to respect the formal semantis of the language. We also show that the transformations never increase the size or complexity of a deduction---in the worst case, they produce deductions of the same size and complexity as the original. We present several examples of proofs containing various types of "detours", and explain how our procedure eliminates them, resulting in smaller and cleaner deductions. All of the given transformations are fully implemented in SML-NJ. The complete code listing is presented, along with explanatory comments. Finally, although the transformations given here are defined for NDL, we point out that they can be applied to any type-alpha DPL that satisfies a few simple conditions.

In this thesis, I designed and implemented a virtual machine (VM) for a monomorphic variant of Athena, a type-omega denotational proof language (DPL). This machine attempts to maintain the minimum state required to evaluate Athena phrases. This thesis also includes the design and implementation of a compiler for monomorphic Athena that compiles to the VM. Finally, it includes details on my implementation of a read-eval-print loop that glues together the VM core and the compiler to provide a full, user-accessible interface to monomorphic Athena. The Athena VM provides the same basis for DPLs that the SECD machine does for pure, functional programming and the Warren Abstract Machine does for Prolog.

This thesis aims to describe how students encounter proof in a community of mathematical practice at a mathematics department and how they are drawn to share mathematicians’ views and knowledge of proof. Considering the department as a community of practice where the joint enterprise is learning mathematics in a broad sense made it possible to perceive the newcomers as active participants in the practice. The combination of a socio-cultural perspective, Lave and Wenger’s and Wenger’s social practice theories and theories about proof offers a fresh framework in understanding and describing the diversity of the culture involving such a complex notion as proof. Proof is examined from historical, philosophical and didactical points of view and considered as reification and as an artefact from a socio-cultural perspective. The metaphor of transparency of artefacts that refers to the intricate dilemma about how much to focus on different aspects of proof at a meta-level and how much to work with proof without focusing on it, both from teacher and student perspectives, is a fundamental aspect in the data analysis. The data consists of transcripts of interviews with mathematicians and students as well as survey responses of university entrants, protocols of observations of lectures, textbooks and other instructional material. Both qualitative and quantitative methods were applied in the data analysis. A theoretical model with three different teaching styles with respect to proof could be constructed from the data. The students related positively to proof when they entered the practice. Though the mathematicians had no explicit intention of dealing so much with proof in the basic course, students felt that they were confronted with proof from the very beginning of their studies. Proof was there as a mysterious artefact and a lot of aspects of proof remained invisible as experienced by students when they struggled to find out what proof is and to understand its role and meaning in the practice. The first oral examination in proof seems to be significant in drawing students to the practice of proof.

The goal of this thesis is to find provably correct methods for detecting conflicts between XACML rules. A conflict occurs when one rule permits a request and another denies that same request. As XACML deals with access control, we can help prevent unwanted access by verifying that it contains rules that do not have unintended conflicts. In order to help with this, we propose an algorithm to find these conflicts then use the Coq Proof Assistant to prove correctness of this algorithm. The algorithm takes a rule set specified in XACML and returns a list of pairs of indices denoting which rules conflict. It is then up to the policy writer to see if the conflicts are intended, or if they need modifying. Since we will prove that this algorithm is sound and complete, we can be assured that the list we obtain is complete and only contains true conflicts.

The use of stars as a radiation source for ground-based ozone remote-sensing instruments is explored and an automated prototype instrument that measures absorption due to atmospheric ozone in stellar spectra has been designed, implemented and tested. <p> This work represents the proof-of-concept development of a low-cost, low dispersion slitless imaging spectrometer that measures Chappuis-band absorption in stellar spectra. The work presented here progresses from the initial concept to a functional calibrated prototype that is capable of nightly automated observations of visible-band spectra from mid-magnitude stars. The design and calibration of the prototype and subsequent data collection and analysis are presented. <p>A slitless imaging spectrometer has been developed and integrated with a commercial self-pointing telescope and an astronomical imager. A relative intensity calibration and the development of a dynamic wavelength calibration scheme, necessitated by the slitless nature of the instrument, is presented. The calibrated prototype has been used to collect several data sets of stellar spectra, and it is shown that the instrument can detect Chappuis absorption in stellar spectra. Several issues with both the concept and design that must be addressed in further development of the prototype are identified.

We explore the relationships between the computational problem of recognizing expander graphs, and the problem of efficiently approximating proof length in the well-known system of \emph{resolution}. This program builds upon known connections between graph expansion and resolution lower bounds. A proof system $P$ is \emph{(quasi-)automatizable} if there is a search algorithm which finds a $P$-proof of a given formula $f$ in time (quasi)polynomial in the length of a shortest $P$-proof of $f$. It is open whether resolution is (quasi-)automatizable. We prove several conditional non-automatizability results for resolution modulo new conjectures concerning the complexity of identifying bipartite expander graphs. Our reductions use a natural family of formulas and exploit the well-known relationships between expansion and length of resolution proofs. Our hardness assumptions are unsupported; we survey known results as progress towards establishing their plausibility. The major contribution is a conditional hardness result for the quasi-automatizability of resolution.

We explore the relationships between the computational problem of recognizing expander graphs, and the problem of efficiently approximating proof length in the well-known system of \emph{resolution}. This program builds upon known connections between graph expansion and resolution lower bounds. A proof system $P$ is \emph{(quasi-)automatizable} if there is a search algorithm which finds a $P$-proof of a given formula $f$ in time (quasi)polynomial in the length of a shortest $P$-proof of $f$. It is open whether resolution is (quasi-)automatizable. We prove several conditional non-automatizability results for resolution modulo new conjectures concerning the complexity of identifying bipartite expander graphs. Our reductions use a natural family of formulas and exploit the well-known relationships between expansion and length of resolution proofs. Our hardness assumptions are unsupported; we survey known results as progress towards establishing their plausibility. The major contribution is a conditional hardness result for the quasi-automatizability of resolution.

The goal of this thesis is to find provably correct methods for detecting conflicts between XACML rules. A conflict occurs when one rule permits a request and another denies that same request. As XACML deals with access control, we can help prevent unwanted access by verifying that it contains rules that do not have unintended conflicts. In order to help with this, we propose an algorithm to find these conflicts then use the Coq Proof Assistant to prove correctness of this algorithm. The algorithm takes a rule set specified in XACML and returns a list of pairs of indices denoting which rules conflict. It is then up to the policy writer to see if the conflicts are intended, or if they need modifying. Since we will prove that this algorithm is sound and complete, we can be assured that the list we obtain is complete and only contains true conflicts.