{"entities":{"Q929293":{"pageid":931141,"ns":120,"title":"Item:Q929293","lastrevid":65418726,"modified":"2026-04-12T02:27:56Z","type":"item","id":"Q929293","labels":{"en":{"language":"en","value":"Feasible operations on proofs: the logic of proofs for bounded arithmetic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5288692"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q929293$DC91322D-E06A-466E-9B31-6F0ACBB836A2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"52ebf50e604124f14a71698f78c5b7fce630bfc2","datavalue":{"value":{"text":"Feasible operations on proofs: the logic of proofs for bounded arithmetic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q929293$026D905B-0A05-4B3F-BC91-546D86416A2D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"feb163faa85700d91f8028964144c9867a17bbf0","datavalue":{"value":"1144.03038","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q929293$56979C94-6AA1-4365-A67A-F09D5454BFD1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2276ddb76dea48fbdc911cd5585d15c440430f83","datavalue":{"value":{"entity-type":"item","numeric-id":636277,"id":"Q636277"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q929293$D5D59A64-A42B-4FC3-89D8-9547253527F8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b559743f011d61696dff04b2ecd3408df2541e49","datavalue":{"value":{"entity-type":"item","numeric-id":169698,"id":"Q169698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q929293$1E43503D-8AB8-4E57-A692-38EA76C0130D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7de2b287d5038562d8981ffcfcc154e35a5a9390","datavalue":{"value":{"time":"+2008-06-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q929293$C25556EA-6030-415C-937F-3CED461400F3","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"06ae4ad30b6d486b8f9c31f5ef0f0093a5e31b08","datavalue":{"value":"The logic of proofs (LP), introduced by \\textit{S. Artemov} [Technical Report MSI 95-29, Cornell University (1995)], is a constructive variant of provability logic which has explicit proof terms instead of the provability operator. It has found applications in epistemic logics, where proof terms can be reinterpreted as terms providing explicit justification for knowledge of a formula. In this paper, the author adapts Artemov's arithmetical completeness proof for LP to show completeness with respect to arithmetical interpretations in Buss's bounded arithmetical theory \\(S^1_2\\). In particular, LP is complete with respect to semantics where proof terms represent feasible (polynomial-time computable) functions.","type":"string"},"datatype":"string"},"type":"statement","id":"Q929293$3B6BBB14-E1BC-47B6-A678-F7EA06CA9255","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"bf05c748b19f894b0cb445a65a1da1ca24dbc809","datavalue":{"value":{"entity-type":"item","numeric-id":331053,"id":"Q331053"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q929293$A79E3E7A-0AF0-4040-8C5C-40D9AF6CD189","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"b638c7935436ccffba7a737e2b57436cbbd2533c","datavalue":{"value":"03F45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q929293$7C19478B-CA37-4A61-8A94-AC8F67CB5D38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q929293$B1914D46-E079-48B7-8C33-5EC265BD6882","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"19e8b53914fe36a939b2f687be46776db2609217","datavalue":{"value":"03B42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q929293$3C07C13C-BEC5-47BD-8E68-DF55F85D44FC","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0fdf1f33ea7a43afff35d867a9109b6eb8295614","datavalue":{"value":"5288692","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q929293$00AE6838-0913-4B2F-A4A1-889CE3EF91E9","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7e2e21a984526b8024b04acd04fd80cbaaf58f4b","datavalue":{"value":"logic of proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q929293$7BBB8566-4062-40E9-85DD-1B958FF738D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cba2903ab2dafc050042cd489ae05396ebe51a19","datavalue":{"value":"bounded arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q929293$E604AF19-E08B-437D-859C-885ABF672239","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4ff02888b791812ddffc3fccfc663496a3736af7","datavalue":{"value":"arithmetical completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q929293$2BB8F9C6-5D0C-42AE-8B15-351BBBE901E2","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q929293$6AA606B1-7AA1-4CF7-9428-979734A52065","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"9870c49cc1165b8d5a57ebd6f7b60e3f9fb81510","datavalue":{"value":"https://doi.org/10.1007/s00224-007-9058-x","type":"string"},"datatype":"url"},"type":"statement","id":"Q929293$80CB8643-0E60-4BFA-B056-081828013804","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a0c3453b423ffbabf860e4afe5cb614b234b9ac0","datavalue":{"value":"W1991386049","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q929293$06EB2CDC-5DD8-4E8F-BEF1-CF459B125FDB","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6015f5a7506db6339797c5e813961394d9eedd0f","datavalue":{"value":{"entity-type":"item","numeric-id":5434494,"id":"Q5434494"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q929293$7BCCD360-85F2-4CA5-9AFC-08B81C59F679","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e1a6ebb360b6bfc3a111b832b5231ca5c9153b7","datavalue":{"value":{"entity-type":"item","numeric-id":2732527,"id":"Q2732527"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q929293$B1513478-2911-4E99-B69D-63BF923EE8A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb0a6de88765b522b9206a93da55a47345cc7d63","datavalue":{"value":{"entity-type":"item","numeric-id":3613333,"id":"Q3613333"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q929293$5D823CFA-1F22-4542-8E61-B2735335873C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"07b1da72ca3738ae54c799ee3ad672846f73e0c6","datavalue":{"value":{"entity-type":"item","numeric-id":3371155,"id":"Q3371155"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q929293$0AAF535D-A3FA-47E5-B132-1BF503B9F23E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d1540adaa2892b49b62abc6e74327970633e8f1c","datavalue":{"value":{"entity-type":"item","numeric-id":685071,"id":"Q685071"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q929293$B54013E7-C193-481F-84A6-FE58EDA5BD20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"035feb3d68e7fcb8cc1f5afc2267fb8cc293e0bf","datavalue":{"value":{"entity-type":"item","numeric-id":3794177,"id":"Q3794177"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q929293$530B55BC-2C33-4E5E-B2D4-34FC8A472A2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4c01f874757bf3c0b7654209141eb027042a1cbe","datavalue":{"value":{"entity-type":"item","numeric-id":3600565,"id":"Q3600565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q929293$232792C0-859C-49C8-BA0A-A35AFF0C8DC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fa34ae3e34f6a863a9f8db67c2bfb8bb6401943","datavalue":{"value":{"entity-type":"item","numeric-id":4856172,"id":"Q4856172"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q929293$8F51016F-EE2B-4DC8-AA08-0D9C51CD24DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"17618ddb1fd34bf255fc52b39503d1e91d300018","datavalue":{"value":{"entity-type":"item","numeric-id":5654035,"id":"Q5654035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q929293$63F6602B-BE0C-48BC-884C-A3822A1A0BF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65af634f8ea04e9717486b98f2f6b61acf5b154f","datavalue":{"value":{"entity-type":"item","numeric-id":1235695,"id":"Q1235695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q929293$EA18CBDD-EEAB-4335-A302-BA00899EC456","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"28224aa63384841437b2438c34da2645e3ea0438","datavalue":{"value":"10.1007/S00224-007-9058-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q929293$87904146-CCB4-464D-A28F-08A0CF747FDE","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5b8e6d90fa6a0f290bed41d32d30a6d3dee01de5","datavalue":{"value":{"entity-type":"item","numeric-id":3434694,"id":"Q3434694"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7d8f6246a302aa6cf3dd55ace1eb2322cd5023ab","datavalue":{"value":{"amount":"+0.9366273283958436","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q929293$125810F2-9C53-4FB6-9560-29FF37FE41A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"69f0206eee7ec92afebd05ca513872623e5a8e30","datavalue":{"value":{"entity-type":"item","numeric-id":703832,"id":"Q703832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b34679aa4d1cc94ee22fef0511e30d96ade313ac","datavalue":{"value":{"amount":"+0.8283188939094543","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q929293$344D3CDD-F903-41F4-B36C-321CF4017113","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bade1c4d4b8c83dc9273b03a9c5e330219392210","datavalue":{"value":{"entity-type":"item","numeric-id":5957921,"id":"Q5957921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"908ba5ed5e32c0b07ce4f9c5407ebe32ec608040","datavalue":{"value":{"amount":"+0.8115875124931335","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q929293$E463C1D6-3FA7-475C-95B6-1491EF659616","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1179604e13f068b59eb285e9dea483e3dd0a9e00","datavalue":{"value":{"entity-type":"item","numeric-id":5232011,"id":"Q5232011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"499a22a3705954e54c9e5d8966438836b7964e03","datavalue":{"value":{"amount":"+0.8115555047988892","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q929293$CA2D888D-B48A-443F-B99C-A0542DB68B48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"986be28e8c168a03f87b25d873f399ff65adf993","datavalue":{"value":{"entity-type":"item","numeric-id":1625591,"id":"Q1625591"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8c0ae1c4a1a988ec3f91ab96a805671f8bd95e0e","datavalue":{"value":{"amount":"+0.8101202845573425","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q929293$656816AC-AA8C-4385-845F-5E1FA159B43C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Feasible operations on proofs: the logic of proofs for bounded arithmetic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Feasible_operations_on_proofs:_the_logic_of_proofs_for_bounded_arithmetic"}}}}}