{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T04:17:03Z","timestamp":1729570623297,"version":"3.28.0"},"reference-count":0,"publisher":"European Mathematical Society - EMS - Publishing House GmbH","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Port. Math."],"published-print":{"date-parts":[[2013,12,31]]},"abstract":"<jats:p>\n            We present theories of bounded arithmetic and weak analysis whose provably total functions (with appropriate graphs) are the polyspace computable functions. More precisely, inspired in Ferreira\u2019s systems \n            <jats:inline-formula>\n              <jats:tex-math>\\mathsf{PTCA}<\/jats:tex-math>\n            <\/jats:inline-formula>\n            , \n            <jats:inline-formula>\n              <jats:tex-math>\\mathsf{\\Sigma^{b}_1}\\textbf{-}\\mathsf{NIA}<\/jats:tex-math>\n            <\/jats:inline-formula>\n             and \n            <jats:inline-formula>\n              <jats:tex-math>\\mathsf{BTFA}<\/jats:tex-math>\n            <\/jats:inline-formula>\n             in the polytime framework, we propose analogue theories concerning polyspace computability. Since the techniques we employ in the characterization of \n            <jats:inline-formula>\n              <jats:tex-math>\\mathsf{PSPACE}<\/jats:tex-math>\n            <\/jats:inline-formula>\n             via formal systems (e.g. Herbrand\u2019s theorem, cut-elimination theorem and the expansion of models) are similar to the ones involved in the polytime setting, we focus on what is specific of polyspace and explains the lift from \n            <jats:inline-formula>\n              <jats:tex-math>\\mathsf{PTIME}<\/jats:tex-math>\n            <\/jats:inline-formula>\n             to \n            <jats:inline-formula>\n              <jats:tex-math>\\mathsf{PSPACE}<\/jats:tex-math>\n            <\/jats:inline-formula>\n            .\n          <\/jats:p>","DOI":"10.4171\/pm\/1936","type":"journal-article","created":{"date-parts":[[2014,3,13]],"date-time":"2014-03-13T22:45:06Z","timestamp":1394750706000},"page":"295-318","source":"Crossref","is-referenced-by-count":0,"title":["Bounded theories for polyspace computability"],"prefix":"10.4171","volume":"70","author":[{"given":"Ricardo","family":"Bianconi","sequence":"first","affiliation":[{"name":"Universidade de S\u00e3o Paulo, Brazil"}]},{"given":"Gilda","family":"Ferreira","sequence":"additional","affiliation":[{"name":"Universidade Lus\u00f3fona de Humanidades e Tecnologias, Lisboa, Portugal"}]},{"given":"Emmanuel","family":"Silva","sequence":"additional","affiliation":[{"name":"Tribunal Regional Federal da 5\u00aa Regi\u00e3o, Recife, Brazil"}]}],"member":"2673","container-title":["Portugaliae Mathematica"],"original-title":[],"link":[{"URL":"http:\/\/www.ems-ph.org\/fulltext\/10.4171\/PM\/1936","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,21]],"date-time":"2024-10-21T18:18:27Z","timestamp":1729534707000},"score":1,"resource":{"primary":{"URL":"https:\/\/ems.press\/doi\/10.4171\/pm\/1936"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,12,31]]},"references-count":0,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.4171\/pm\/1936","relation":{},"ISSN":["0032-5155","1662-2758"],"issn-type":[{"type":"print","value":"0032-5155"},{"type":"electronic","value":"1662-2758"}],"subject":[],"published":{"date-parts":[[2013,12,31]]}}}