Proof normalization of structured algebraic specifications is convergent

Martin Wirsing, John N Crossley, Hannes Peterreins

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

    4 Citations (Scopus)


    In this paper we present a new natural deduction calculus for structured algebraic specifications and study proof transformations including cut elimination. As underlying language we choose an ASL-like kernel language which includes operators for composing specifications, renaming the signature and exporting a subsignature of a specification. To get a natural deduction calculus for structured specifications we combine a natural deduction calculus for first-order predicate logic with the proof rules for structured specifications. The main results are soundness and completeness of the calculus and convergence of the associated system of proof term reductions which extends a typed l-calculus by appropriate structural reductions.
    Original languageEnglish
    Title of host publicationRecent Trends in Algebraic Development Techniques
    Subtitle of host publication13th International Workshop, WADT’98 Lisbon, Portugal, April 2-4, 1998 Selected Papers
    EditorsJose Luiz Fiadeiro
    Place of PublicationBerlin Germany
    Number of pages15
    ISBN (Print)3540662464
    Publication statusPublished - 1999
    EventInternational Workshop on Algebraic Development Techniques 1998 - Lisbon, Portugal
    Duration: 2 Apr 19984 Apr 1998
    Conference number: 13th (Proceedings)

    Publication series

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


    ConferenceInternational Workshop on Algebraic Development Techniques 1998
    Abbreviated titleWADT 1998
    Internet address

    Cite this