Proof normalization of structured algebraic specifications is convergent

Martin Wirsing; John N Crossley; Hannes Peterreins

doi:10.1007/3-540-48483-3_21

Proof normalization of structured algebraic specifications is convergent

Martin Wirsing, John N Crossley, Hannes Peterreins

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

4 Citations (Scopus)

Abstract

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 language	English
Title of host publication	Recent Trends in Algebraic Development Techniques
Subtitle of host publication	13th International Workshop, WADT’98 Lisbon, Portugal, April 2-4, 1998 Selected Papers
Editors	Jose Luiz Fiadeiro
Place of Publication	Berlin Germany
Publisher	Springer
Pages	326-340
Number of pages	15
ISBN (Print)	3540662464
DOIs	https://doi.org/10.1007/3-540-48483-3_21
Publication status	Published - 1999
Event	International Workshop on Algebraic Development Techniques 1998 - Lisbon, Portugal Duration: 2 Apr 1998 → 4 Apr 1998 Conference number: 13th https://link-springer-com.ezproxy.lib.monash.edu.au/book/10.1007/3-540-48483-3 (Proceedings)

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	1589
ISSN (Print)	0302-9743

Conference

Conference	International Workshop on Algebraic Development Techniques 1998
Abbreviated title	WADT 1998
Country/Territory	Portugal
City	Lisbon
Period	2/04/98 → 4/04/98
Internet address	https://link-springer-com.ezproxy.lib.monash.edu.au/book/10.1007/3-540-48483-3 (Proceedings)

Access to Document

10.1007/3-540-48483-3_21

Cite this

Wirsing, M., Crossley, J. N., & Peterreins, H. (1999). Proof normalization of structured algebraic specifications is convergent. In J. L. Fiadeiro (Ed.), Recent Trends in Algebraic Development Techniques: 13th International Workshop, WADT’98 Lisbon, Portugal, April 2-4, 1998 Selected Papers (pp. 326-340). (Lecture Notes in Computer Science; Vol. 1589). Springer. https://doi.org/10.1007/3-540-48483-3_21

Wirsing, Martin ; Crossley, John N ; Peterreins, Hannes. / Proof normalization of structured algebraic specifications is convergent. Recent Trends in Algebraic Development Techniques: 13th International Workshop, WADT’98 Lisbon, Portugal, April 2-4, 1998 Selected Papers. editor / Jose Luiz Fiadeiro. Berlin Germany : Springer, 1999. pp. 326-340 (Lecture Notes in Computer Science).

@inproceedings{ea44036386654c14a54a8d90f3a87a7c,

title = "Proof normalization of structured algebraic specifications is convergent",

abstract = "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.",

author = "Martin Wirsing and Crossley, {John N} and Hannes Peterreins",

year = "1999",

doi = "10.1007/3-540-48483-3_21",

language = "English",

isbn = "3540662464",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "326--340",

editor = "Fiadeiro, {Jose Luiz}",

booktitle = "Recent Trends in Algebraic Development Techniques",

note = "International Workshop on Algebraic Development Techniques 1998, WADT 1998 ; Conference date: 02-04-1998 Through 04-04-1998",

url = "https://link-springer-com.ezproxy.lib.monash.edu.au/book/10.1007/3-540-48483-3",

}

Wirsing, M, Crossley, JN & Peterreins, H 1999, Proof normalization of structured algebraic specifications is convergent. in JL Fiadeiro (ed.), Recent Trends in Algebraic Development Techniques: 13th International Workshop, WADT’98 Lisbon, Portugal, April 2-4, 1998 Selected Papers. Lecture Notes in Computer Science, vol. 1589, Springer, Berlin Germany, pp. 326-340, International Workshop on Algebraic Development Techniques 1998, Lisbon, Portugal, 2/04/98. https://doi.org/10.1007/3-540-48483-3_21

Proof normalization of structured algebraic specifications is convergent. / Wirsing, Martin; Crossley, John N; Peterreins, Hannes.
Recent Trends in Algebraic Development Techniques: 13th International Workshop, WADT’98 Lisbon, Portugal, April 2-4, 1998 Selected Papers. ed. / Jose Luiz Fiadeiro. Berlin Germany: Springer, 1999. p. 326-340 (Lecture Notes in Computer Science; Vol. 1589).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

TY - GEN

T1 - Proof normalization of structured algebraic specifications is convergent

AU - Wirsing, Martin

AU - Crossley, John N

AU - Peterreins, Hannes

N1 - Conference code: 13th

PY - 1999

Y1 - 1999

N2 - 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.

AB - 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.

U2 - 10.1007/3-540-48483-3_21

DO - 10.1007/3-540-48483-3_21

M3 - Conference Paper

SN - 3540662464

T3 - Lecture Notes in Computer Science

SP - 326

EP - 340

BT - Recent Trends in Algebraic Development Techniques

A2 - Fiadeiro, Jose Luiz

PB - Springer

CY - Berlin Germany

T2 - International Workshop on Algebraic Development Techniques 1998

Y2 - 2 April 1998 through 4 April 1998

ER -

Wirsing M, Crossley JN, Peterreins H. Proof normalization of structured algebraic specifications is convergent. In Fiadeiro JL, editor, Recent Trends in Algebraic Development Techniques: 13th International Workshop, WADT’98 Lisbon, Portugal, April 2-4, 1998 Selected Papers. Berlin Germany: Springer. 1999. p. 326-340. (Lecture Notes in Computer Science). doi: 10.1007/3-540-48483-3_21