The faithfulness of atomic polymorphism

Registro completo de metadados
MetadadosDescriçãoIdioma
Autor(es): dc.creatorFerreira, Fernando-
Autor(es): dc.creatorFerreira, Gilda-
Data de aceite: dc.date.accessioned2022-02-15T14:07:54Z-
Data de disponibilização: dc.date.available2022-02-15T14:07:54Z-
Data de envio: dc.date.issued2021-02-14-
Data de envio: dc.date.issued2021-02-14-
Data de envio: dc.date.issued2014-
Fonte completa do material: dc.identifierhttp://hdl.handle.net/10400.2/10489-
Fonte: dc.identifier.urihttp://educapes.capes.gov.br/handle/10400.2/10489-
Descrição: dc.descriptionIt is known that the full intuitionistic propositional calculus can be embedded into the atomic polymorphic system Fat, a calculus with only two connectives: the conditional and the second-order universal quantifier. The embedding uses a translation of formulas due to Prawitz and relies on the so-called property of instantiation overflow. In this paper, we show that the previous embedding is faithful i.e., if a translated formula is derivable in Fat, then the original formula is already derivable in the propositional calculus.-
Descrição: dc.descriptioninfo:eu-repo/semantics/publishedVersion-
Idioma: dc.languageen-
Publicador: dc.publisherLodz University Press-
Relação: dc.relationPEstOE/MAT/UI0209/2011-
Relação: dc.relationinfo:eu-repo/grantAgreement/FCT/SFRH/SFRH%2FBPD%2F34527%2F2006/PT-
Direitos: dc.rightsopenAccess-
Palavras-chave: dc.subjectPredicative polymorphism-
Palavras-chave: dc.subjectFaithfulness-
Palavras-chave: dc.subjectNatural deduction-
Palavras-chave: dc.subjectKripke models-
Palavras-chave: dc.subjectIntuitionistic propositional calculus-
Título: dc.titleThe faithfulness of atomic polymorphism-
Tipo de arquivo: dc.typelivro digital-
Aparece nas coleções:Repositório Aberto - Universidade Aberta (Portugal)

Não existem arquivos associados a este item.