Thesis (M. Ed.)--University of Hong Kong, 1996. / Includes bibliographical references (leaf 93-96).

Thesis (M.Ed.)--University of Hong Kong, 1996. / Includes bibliographical references (leaves 93-96). Also available in print.

No description available.

Thesis (M. Ed.)--University of Hong Kong, 2001. / Includes bibliographical references (leaves 56-57).

Thesis (M.Ed.)--University of Hong Kong, 2001. / Includes bibliographical references (leaves 56-57). Also available in print.

This thesis develops techniques and ideas on proof search. Proof search is used with one of two meanings. Proof search can be thought of either as the search for a yes/no answer to a query (theorem proving), or as the search for all proofs of a formula (proof enumeration). This thesis is an investigation into issues in proof search in both these senses for some non-classical logics. Gentzen systems are well suited for use in proof search in both senses. The rules of Gentzen sequent calculi are such that implementations can be directed by the top level syntax of sequents, unlike other logical calculi such as natural deduction. All the calculi for proof search in this thesis are Gentzen sequent calculi. In Chapter 2, permutation of inference rules for Intuitionistic Linear Logic is studied. A focusing calculus, ILLF, in the style of Andreoli ([And92]) is developed. This calculus allows only one proof in each equivalence class of proofs equivalent up to permutations of inferences. The issue here is both theorem proving and proof enumeration. For certain logics, normal natural deductions provide a proof-theoretic semantics. Proof enumeration is then the enumeration of all these deductions. Herbelin's cut- free LJT ([Her95], here called MJ) is a Gentzen system for intuitionistic logic allowing derivations that correspond in a 1-1 way to the normal natural deductions of intuitionistic logic. This calculus is therefore well suited to proof enumeration. Such calculi are called 'permutation-free' calculi. In Chapter 3, MJ is extended to a calculus for an intuitionistic modal logic (due to Curry) called Lax Logic. We call this calculus PFLAX. The proof theory of MJ is extended to PFLAX. Chapter 4 presents work on theorem proving for propositional logics using a history mechanism for loop-checking. This mechanism is a refinement of one developed by Heuerding et al ([HSZ96]). It is applied to two calculi for intuitionistic logic and also to two modal logics; Lax Logic and intuitionistic S4. The calculi for intuitionistic logic are compared both theoretically and experimentally with other decision procedures for the logic. Chapter 5 is a short investigation of embedding intuitionistic logic in Intuitionistic Linear Logic. A new embedding of intuitionistic logic in Intuitionistic Linear Logic is given. For the hereditary Harrop fragment of intuitionistic logic, this embedding induces the calculus MJ for intuitionistic logic. In Chapter 6 a 'permutation-free' calculus is given for Intuitionistic Linear Logic. Again, its proof-theoretic properties are investigated. The calculus is proved to be sound and complete with respect to a proof-theoretic semantics and (weak) cut- elimination is proved. Logic programming can be thought of as proof enumeration in constructive logics. All the proof enumeration calculi in this thesis have been developed with logic programming in mind. We discuss at the appropriate points the relationship between the calculi developed here and logic programming. Appendix A contains presentations of the logical calculi used and Appendix B contains the sets of benchmark formulae used in Chapter 4.

The subject of the study is a theory of positive and negative inquiry with emphasis in mathematics. The purposes of this study are to examine the historical development of systematic inquiry in mathematics, to identify the nature of positive and negative inquiry, to propose and develop an interrelated set of propositions regarding positive and negative inquiry, and to relate the proposition of the theory to certain basic concepts of trigonometry.

Whilst results from Structural Proof Theory can be couched in many formalisms, it is the sequent calculus which is the most amenable of the formalisms to metamathematical treatment. Constructive syntactic proofs are filled with bureaucratic details; rarely are all cases of a proof completed in the literature. Two intermediate results can be used to drastically reduce the amount of effort needed in proofs of Cut admissibility: Weakening and Invertibility. Indeed, whereas there are proofs of Cut admissibility which do not use Invertibility, Weakening is almost always necessary. Use of these results simply shifts the bureaucracy, however; Weakening and Invertibility, whilst more easy to prove, are still not trivial. We give a framework under which sequent calculi can be codified and analysed, which then allows us to prove various results: for a calculus to admit Weakening and for a rule to be invertible in a calculus. For the latter, even though many calculi are investigated, the general condition is simple and easily verified. The results have been applied to G3ip, G3cp, G3s, G3-LC and G4ip. Invertibility is important in another respect; that of proof-search. Should all rules in a calculus be invertible, then terminating root-first proof search gives a decision procedure for formulae without the need for back-tracking. To this end, we present some results about the manipulation of rule sets. It is shown that the transformations do not affect the expressiveness of the calculus, yet may render more rules invertible. These results can guide the design of efficient calculi. When using interactive proof assistants, every case of a proof, however complex, must be addressed and proved before one can declare the result formalised. To do this in a human readable way adds a further layer of complexity; most proof assistants give output which is only legible to a skilled user of that proof assistant. We give human-readable formalisations of Cut admissibility for G3cp and G3ip, Contraction admissibility for G4ip and Craig's Interpolation Theorem for G3i using the Isar vernacular of Isabelle. We also formalise the new invertibility results, in part using the package for reasoning about first-order languages, Nominal Isabelle. Examples are given showing the effectiveness of the formalisation. The formal proof of invertibility using the new methods is drastically shorter than the traditional, direct method.

We introduce subatomic logic, a new methodology where by looking inside of atoms we are able to represent a wide variety of proof systems in such a way that every rule is an instance of a single, regular, linear rule scheme. We show the generality of the subatomic approach by presenting how it can be applied to several different systems with very different expressivity. In this thesis we use subatomic logic to study two normalisation procedures: cut-elimination and decomposition. In particular, we study cut-elimination by characterising a whole class of substructural logics and giving a generalised cut-elimination procedure for them, and we study decomposition by providing generalised rewriting rules for derivations that we can then apply to decompose derivations and to eliminate cycles.

M.Ed. / Recently there has been renewed interest in proof and proving in schools worldwide. However, many school students and even teachers of mathematics have only superficial ideas on the nature of proof. Proof is considered the heart of mathematics as individuals explore, make conjectures and try to convince themselves and others about the truth or falsity of their conjectures. There are basically two categories of deductive proof, namely proof by direct argument and indirect proofs. The aim of this study was to examine the structural features common to most of the mathematical proofs for formalised mathematical systems, with the emphasis on indirect proof techniques. The main question was to investigate which mathematical activities and logical principles at secondary school level are necessary for students to become proficient with proof writing. A great deal of specialised language is associated with reasoning. Such words as axiom, theorem, proof, and conjecture are just some of the terms that students must understand as they engage in the proof-making task. The formal aspect of mathematics at secondary school is extremely important. It is inevitable that students become involved with hypothetical arguments. They use among others, proofs by contradiction. Furthermore, necessary and sufficient conditions are related to theorems and their converses. It is therefore apparent that the study of logic is necessary already at secondary school level in order to practise mathematics satisfactorily. An analysis of the mathematics syllabus of the Department of Education has indicated that students should use indirect techniques of proof. According to this syllabus students should be familiar with logical arguments. The conclusion which is reached, gives evidence that students’ background in logic is completely lacking and inadequate. As a result they cannot cope adequately with argumentation and this causes a poor perception of what mathematics entails. Although proof writing can never be reduced to a mechanical process, considerable anxiety and uncertainty can be eliminated from the process if students are exposed to the principles of elementary logic and techniques. Mathematics educators and education researchers have reported students’ difficulties with mathematical proof and point out the conflict between the nature of this essential mathematical activity and current approaches to teaching it. This recent interest has led to an increased effort to teach proof in innovative ways.