η-conversions of IPC implemented in atomic F

Registro completo de metadados
MetadadosDescriçãoIdioma
Autor(es): dc.creatorFerreira, Gilda-
Data de aceite: dc.date.accessioned2019-08-21T17:13:21Z-
Data de disponibilização: dc.date.available2019-08-21T17:13:21Z-
Data de envio: dc.date.issued2018-02-09-
Data de envio: dc.date.issued2018-05-31-
Data de envio: dc.date.issued2017-
Fonte completa do material: dc.identifierhttp://hdl.handle.net/10400.2/7091-
Fonte: dc.identifier.urihttp://educapes.capes.gov.br/handle/10400.2/7091-
Descrição: dc.descriptionIt is known that the β-conversions of the full intuitionistic propositional calculus (IPC) translate into βη-conversions of the atomic polymorphic calculus Fat. Since Fat enjoys the property of strong normalization for βη-conversions, an alternative proof of strong normalization for IPC considering β-conversions can be derived. In the present article, we improve the previous result by analysing the translation of the η-conversions of the latter calculus into a technical variant of the former system (the atomic polymorphic calculus Fat^∧_at). In fact, from the strong normalization of Fat^∧_at we can derive the strong normalization of the full intuitionistic propositional calculus considering all the standard (β and η) conversions.-
Descrição: dc.descriptioninfo:eu-repo/semantics/publishedVersion-
Idioma: dc.languageen-
Publicador: dc.publisherOxford University Press-
Relação: dc.relationinfo:eu-repo/grantAgreement/FCT/5876/147209/PT-
Relação: dc.relationinfo:eu-repo/grantAgreement/FCT/SFRH/SFRH%2FBPD%2F93278%2F2013/PT-
Relação: dc.relationhttps://academic.oup.com/jigpal/article-abstract/25/2/115/2892209?redirectedFrom=fulltext-
Direitos: dc.rightsopenAccess-
Direitos: dc.rightshttp://creativecommons.org/licenses/by/4.0/-
Palavras-chave: dc.subjectMathematical logic-
Palavras-chave: dc.subjectEta-conversions-
Palavras-chave: dc.subjectPredicative polymorphism-
Palavras-chave: dc.subjectIntuitionistic propositional calculus-
Palavras-chave: dc.subjectStrong normalization-
Palavras-chave: dc.subjectNatural deduction-
Título: dc.titleη-conversions of IPC implemented in atomic F-
Tipo de arquivo: dc.typelivro digital-
Aparece nas coleções:Repositório Aberto - Universidade Aberta (Portugal)

Não existem arquivos associados a este item.