Publication
The Russell-Prawitz embedding and the atomization of universal instantiation
| dc.contributor.author | Espírito Santo, José | |
| dc.contributor.author | Ferreira, Gilda | |
| dc.date.accessioned | 2021-02-15T13:37:44Z | |
| dc.date.available | 2022-02-01T01:30:29Z | |
| dc.date.issued | 2020 | |
| dc.description.abstract | Given the recent interest in the fragment of system F where universal instantiation is restricted to atomic formulas, a fragment nowadays named system Fat, we study directly in system F new conversions whose purpose is to enforce that restriction. We show some benefits of these new atomization conversions: (1) They help achieving strict simulation of proof reduction by means of the Russell-Prawitz embedding of IPC into system F; (2) They are not stronger than a certain “dinaturality” conversion known to generate a consistent equality of proofs; (3) They provide the bridge between the Russell-Prawitz embedding and another translation, due to the authors, of IPC directly into system Fat; (4) They give means for explaining why the Russell-Prawitz translation achieves strict simulation whereas the translation into Fat does not. | pt_PT |
| dc.description.version | info:eu-repo/semantics/publishedVersion | pt_PT |
| dc.identifier.doi | 10.1093/jigpal/jzaa025 | pt_PT |
| dc.identifier.eissn | 1368-9894 | |
| dc.identifier.issn | 1367-0751 | |
| dc.identifier.uri | http://hdl.handle.net/10400.2/10493 | |
| dc.language.iso | eng | pt_PT |
| dc.peerreviewed | yes | pt_PT |
| dc.publisher | Oxford Academic | pt_PT |
| dc.relation | Center of Mathematics of the University of Minho | |
| dc.relation | Center of Mathematics of the University of Minho | |
| dc.relation | Center for Mathematics, Fundamental Applications and Operations Research | |
| dc.relation | LARGE-SCALE INFORMATICS SYSTEMS LABORATORY | |
| dc.subject | Intuitionistic propositional calculus | pt_PT |
| dc.subject | System F | pt_PT |
| dc.subject | Predicative polymorphism | pt_PT |
| dc.subject | Russell-Prawitz translation | pt_PT |
| dc.subject | Proof reduction | pt_PT |
| dc.title | The Russell-Prawitz embedding and the atomization of universal instantiation | pt_PT |
| dc.type | journal article | |
| dspace.entity.type | Publication | |
| oaire.awardTitle | Center of Mathematics of the University of Minho | |
| oaire.awardTitle | Center of Mathematics of the University of Minho | |
| oaire.awardTitle | Center for Mathematics, Fundamental Applications and Operations Research | |
| oaire.awardTitle | LARGE-SCALE INFORMATICS SYSTEMS LABORATORY | |
| oaire.awardURI | info:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/UIDB%2F00013%2F2020/PT | |
| oaire.awardURI | info:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/UIDP%2F00013%2F2020/PT | |
| oaire.awardURI | info:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/UID%2FMAT%2F04561%2F2019/PT | |
| oaire.awardURI | info:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/UID%2FCEC%2F00408%2F2019/PT | |
| oaire.citation.title | Logic Journal of The IGPL | pt_PT |
| oaire.fundingStream | 6817 - DCRRNI ID | |
| oaire.fundingStream | 6817 - DCRRNI ID | |
| oaire.fundingStream | 6817 - DCRRNI ID | |
| oaire.fundingStream | 6817 - DCRRNI ID | |
| person.familyName | Soares do Espírito Santo | |
| person.familyName | Ferreira | |
| person.givenName | José Carlos | |
| person.givenName | Gilda | |
| person.identifier.ciencia-id | A610-7A79-73AF | |
| person.identifier.ciencia-id | 0B1A-81E7-88B1 | |
| person.identifier.orcid | 0000-0002-6348-5653 | |
| 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.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 | |
| 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 versão em papel ainda não foi publicada. Neste momento o artigo está publicado apenas na forma online (online first). | pt_PT |
| rcaap.rights | openAccess | pt_PT |
| rcaap.type | article | pt_PT |
| relation.isAuthorOfPublication | 9994be17-d473-4de8-919c-cedfd920a1f6 | |
| relation.isAuthorOfPublication | fd3a6c7d-42b2-4434-834f-fb161900c938 | |
| relation.isAuthorOfPublication.latestForDiscovery | fd3a6c7d-42b2-4434-834f-fb161900c938 | |
| relation.isProjectOfPublication | 0382e7ad-5e57-45d3-a699-dc9da1ef20a5 | |
| relation.isProjectOfPublication | 544a3395-0e02-42f6-a557-31e9d9ad4979 | |
| relation.isProjectOfPublication | dbac8869-ac01-4776-917d-7757322034bb | |
| relation.isProjectOfPublication | e888b4af-8eff-4efb-826c-fd87c5facd97 | |
| relation.isProjectOfPublication.latestForDiscovery | 0382e7ad-5e57-45d3-a699-dc9da1ef20a5 |
Files
Original bundle
1 - 1 of 1