Publication
η-conversions of IPC implemented in atomic F
| dc.contributor.author | Ferreira, Gilda | |
| dc.date.accessioned | 2018-02-09T10:20:06Z | |
| dc.date.available | 2018-05-31T00:30:12Z | |
| dc.date.issued | 2017 | |
| dc.description.abstract | It 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. | pt_PT |
| dc.description.version | info:eu-repo/semantics/publishedVersion | pt_PT |
| dc.identifier.citation | Gilda Ferreira - η-conversions of IPC implemented in atomic F. "Logic Journal of the IGPL" [Em linha]. ISSN 1367-0751 (Print) 1368-9894 (Online). Vol. 25, nº 2 (2017), p. 115–130 | pt_PT |
| dc.identifier.doi | 10.1093/jigpal/jzw035 | pt_PT |
| dc.identifier.issn | 1367-0751 (Print) | |
| dc.identifier.uri | http://hdl.handle.net/10400.2/7091 | |
| dc.language.iso | eng | pt_PT |
| dc.peerreviewed | yes | pt_PT |
| dc.publisher | Oxford University Press | pt_PT |
| dc.relation | Teoria da demonstração: abordagem lógico-computacional | |
| dc.relation.publisherversion | https://academic.oup.com/jigpal/article-abstract/25/2/115/2892209?redirectedFrom=fulltext | pt_PT |
| dc.rights.uri | http://creativecommons.org/licenses/by/4.0/ | pt_PT |
| dc.subject | Mathematical logic | pt_PT |
| dc.subject | Eta-conversions | pt_PT |
| dc.subject | Predicative polymorphism | pt_PT |
| dc.subject | Intuitionistic propositional calculus | pt_PT |
| dc.subject | Strong normalization | pt_PT |
| dc.subject | Natural deduction | pt_PT |
| dc.title | η-conversions of IPC implemented in atomic F | pt_PT |
| dc.type | journal article | |
| dspace.entity.type | Publication | |
| oaire.awardTitle | Teoria da demonstração: abordagem lógico-computacional | |
| oaire.awardURI | info:eu-repo/grantAgreement/FCT/5876/UID%2FMAT%2F04561%2F2013/PT | |
| oaire.awardURI | info:eu-repo/grantAgreement/FCT//SFRH%2FBPD%2F93278%2F2013/PT | |
| oaire.citation.endPage | 130 | pt_PT |
| oaire.citation.issue | 2 | pt_PT |
| oaire.citation.startPage | 115 | pt_PT |
| oaire.citation.title | Logic Journal of the IGPL | pt_PT |
| oaire.citation.volume | 25 | pt_PT |
| oaire.fundingStream | 5876 | |
| person.familyName | Ferreira | |
| person.givenName | Gilda | |
| person.identifier.ciencia-id | 0B1A-81E7-88B1 | |
| person.identifier.orcid | 0000-0003-1447-9764 | |
| person.identifier.rid | H-9953-2013 | |
| person.identifier.scopus-author-id | 14037466100 | |
| project.funder.identifier | http://doi.org/10.13039/501100001871 | |
| project.funder.identifier | http://doi.org/10.13039/501100001871 | |
| project.funder.name | Fundação para a Ciência e a Tecnologia | |
| project.funder.name | Fundação para a Ciência e a Tecnologia | |
| rcaap.embargofct | A indicação da revista é: "Post-print in Institutional repositories or Central repositories after 12 months embargo" | pt_PT |
| rcaap.rights | openAccess | pt_PT |
| rcaap.type | article | pt_PT |
| relation.isAuthorOfPublication | fd3a6c7d-42b2-4434-834f-fb161900c938 | |
| relation.isAuthorOfPublication.latestForDiscovery | fd3a6c7d-42b2-4434-834f-fb161900c938 | |
| relation.isProjectOfPublication | 790cb869-ff08-40ad-8026-fa89e1020bc0 | |
| relation.isProjectOfPublication | dab4f1a3-08b3-4ccc-8509-1aa421dd896c | |
| relation.isProjectOfPublication.latestForDiscovery | dab4f1a3-08b3-4ccc-8509-1aa421dd896c |