Equational reasoning via partial reflection

J.H. Geuvers, F. Wiedijk, J. Zwanenburg

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    9 Citations (Scopus)

    Abstract

    We modify the reflection method to enable it to deal with partial functions like division. The idea behind reflection is to program a tactic for a theorem prover not in the implementation language but in the object language of the theorem prover itself. The main ingredients of the reflection method are a syntactic encoding of a class of problems, an interpretation function (mapping the encoding to the problem) and a decision function, written on the encodings. Together with a correctness proof of the decision function, this gives a fast method for solving problems. The contribution of this work lies in the extension of the reflection method to deal with equations in algebraic structures where some functions may be partial. The primary example here is the theory of fields. For the reflection method, this yields the problem that the interpretation function is not total. In this paper we show how this can be overcome by defining the interpretation as a relation. We give the precise details, both in mathematical terms and in Coq syntax. It has been used to program our own tactic ‘Rational’, for verifying equations between field elements.
    Original languageEnglish
    Title of host publicationTheorem Proving in Higher Order Logics (Proceedings 13th International Conference, TPHOLs 2000, Portland OR, USA, August 14-18, 2000)
    EditorsM. Aagaard, J. Harrison
    PublisherSpringer
    Pages162-178
    ISBN (Print)3-540-67863-8
    DOIs
    Publication statusPublished - 2000

    Publication series

    NameLecture Notes in Computer Science
    Volume1869
    ISSN (Print)0302-9743

    Fingerprint

    Dive into the research topics of 'Equational reasoning via partial reflection'. Together they form a unique fingerprint.

    Cite this