Normalization of S-terms is decidable

DOI10.1007/BFB0052367MaRDI QIDQ3838766zbMATH OpenFDO

Authors Johannes Waldmann

Publication date 11 October 1998

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0052367

zbMATH Keywords

combinator \({\mathbf S}\)combinatory logicdecision procedurenormal formproperties of \({\mathbf S}\)-termsrational tree languages

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Combinatory logic and lambda calculus (03B40)

Recommendations

• A short proof of the decidability of normalization in recursive program schemes
• A simple proof of the undecidability of strong normalisation
• The normalization theorem for extended natural deduction
• Decidability of S1S and S2S
• scientific article; zbMATH DE number 1354101
• Normalization theorems for full first order classical natural deduction
• A formalization of Sambins's normalization for GL
• scientific article; zbMATH DE number 4128369
• Characterising strongly normalising intuitionistic terms
• scientific article; zbMATH DE number 874672

Cited in

(4)

• The combinator S
• scientific article; zbMATH DE number 4085616 (Why is no real title available?)
• scientific article; zbMATH DE number 1216018 (Why is no real title available?)
• A short proof of the decidability of normalization in recursive program schemes

This page was built for publication: Normalization of S-terms is decidable

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3838766)