{"entities":{"Q1814133":{"pageid":1824875,"ns":120,"title":"Item:Q1814133","lastrevid":73017888,"modified":"2026-04-14T09:25:14Z","type":"item","id":"Q1814133","labels":{"en":{"language":"en","value":"A unification-theoretic method for investigating the \\(k\\)-provability problem"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 10156"}},"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":"Q1814133$51D84008-9F2E-41CA-87D5-C88F30A19922","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7d7fb86cd96181ab3edf6c7dae6f558ca2e23b63","datavalue":{"value":{"text":"A unification-theoretic method for investigating the \\(k\\)-provability problem","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1814133$6E0652BB-E3D4-4873-86D6-DC762AD5FFE8","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"44be62ba08eba8f460f23d0f9dd72b6a3187e447","datavalue":{"value":"0735.03001","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1814133$8C8DD74B-9A70-4A63-9CEE-69D6E2090D6B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e3a5526603abcb4423f4f8eb3613254d9dd2b2d1","datavalue":{"value":"10.1016/0168-0072(91)90015-E","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1814133$B31C06B9-E906-4AE6-B26C-A82DABCFC91A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"596956d13d65318c3063740527340bc624646ab6","datavalue":{"value":{"entity-type":"item","numeric-id":174773,"id":"Q174773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$6980619A-FAE2-448B-B1F2-79E7405E40AB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$127ECCEE-BF6C-4B25-AE94-F0220D909497","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d3f790682a6be4cc1f3210e15eebe1d6cc5ffbc2","datavalue":{"value":{"time":"+1992-06-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1814133$FA96BC45-1179-438C-AD7A-E9FB3C62B1DB","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"1f34cd612caee44a215afbdd912fcef6b194b139","datavalue":{"value":"The \\(k\\)-provability problem for first-order axiomatic systems with a finite number of axiom schemata and a finite number of rules of inference is investigated. The \\(k\\)-provability problem is to determine, given a natural number \\(k\\) and a formula \\(F\\), whether or not there is a proof of \\(F\\) containing at most \\(k\\) lines.   In order to make this notion precise, the notion of a Parikh system is introduced. The author notes that almost all first-order axiomatic systems that are to be found in the literature (including Peano arithmetic) can be formulated as Parikh systems.   Various ways of classifying Parikh systems are proposed. Also, three different ways of formulating first-order logics --- two of which lead to Parikh systems with decidable \\(k\\)-provability problems --- are presented.   The major part of the paper is devoted to develop a method for investigating the \\(k\\)-provability problem that utilizes techniques and concepts from unification theory.   By solving various subproblems of the unification problem (which is undecidable), the author solves the \\(k\\)-provability problem for a variety of Parikh systems including several formulations of Peano arithmetic.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1814133$0020C218-2787-49A8-9D41-F6F17AD3C9FD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1814133$8A6D68A0-4F50-4D4F-B440-6D6164E703FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1814133$0A5A79BF-DEAD-4B31-AE01-CCBD6A85DD22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1814133$F03A6B37-4D9F-4E45-B53D-CC733E7CA497","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9f5ed62109405ac6514bd78fce15113cefc1467c","datavalue":{"value":"10156","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1814133$2F91794C-7F0D-4702-94EB-EBDF8A9BF513","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b2cf531807d1424e6515228822fe70f93a61e21d","datavalue":{"value":"axiomatic theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1814133$B2D16CF7-CA4C-4F51-AB83-DD74CD4C3F2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"822c4bdd2e4938617ffaa67c9f5be65f0720d831","datavalue":{"value":"k-provability problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1814133$C6821F7E-51B5-4DB6-BEE3-5AF6A8AF4A39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"05f15f0054508841c2584e56689e703731d2cc3a","datavalue":{"value":"first-order axiomatic systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1814133$6CA14680-CFD0-450B-9190-6FA8D581C935","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3f1ca8a369abdbc20d59b41090e652fbc53ba766","datavalue":{"value":"Parikh system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1814133$809DC7AB-97AF-4D61-AB9D-309064D9E215","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0425b5870c27baf41770aff2d288003d57be5b2d","datavalue":{"value":"subproblems of the unification problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1814133$9B0552F9-5B4C-4B52-B9BA-286E92353B4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7090cb2b2cefa03cee6b50a67ca057c086ad0f00","datavalue":{"value":"Peano arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1814133$E3A8F312-6079-4C9A-9786-0AEF91AF5082","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"05f3dff3edc7d97b14af7ecb326f488fb3fee31b","datavalue":{"value":{"entity-type":"item","numeric-id":583186,"id":"Q583186"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$283C0F43-4DA0-4D63-A2FB-7D1D6A3C3A6C","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":"Q1814133$9E7010F9-F908-48DC-BE2F-4F5DFC413E36","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"49508253f586991686167e53d90ae970b902e6b3","datavalue":{"value":{"entity-type":"item","numeric-id":1176199,"id":"Q1176199"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$AA7E5578-5DC1-427F-BC85-84251D97FA58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"175c1c6339231426570e05a46d3193da46e70701","datavalue":{"value":{"entity-type":"item","numeric-id":4401926,"id":"Q4401926"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$CA92B2D0-1919-48CB-83F3-38DB670974C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"54ba8f7244e4159964661fb024ab4457cffcc5e2","datavalue":{"value":{"entity-type":"item","numeric-id":5619080,"id":"Q5619080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$1A18FDBD-06C0-41FD-AD41-CF8DB7FB6DB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ca4f823ca2e82e86e612699cdb65f38c133999d","datavalue":{"value":{"entity-type":"item","numeric-id":4052071,"id":"Q4052071"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$B587B1F3-0D39-430E-96DF-F2E76ABB9286","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9b757d362e566e6bb8567869560a0af0408a0e3","datavalue":{"value":{"entity-type":"item","numeric-id":1109019,"id":"Q1109019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$6BEAA6D8-E03F-4E1C-A3A5-CCE095EF3FFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4bdba4af064cab5f0d5d2b05f43f44c0bd28a3bc","datavalue":{"value":{"entity-type":"item","numeric-id":807609,"id":"Q807609"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$03A60127-2A16-4485-85BA-B7DF5F55E843","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f3b8a8bbc08f166f4f946f3a032d3d7074f3fd6b","datavalue":{"value":{"entity-type":"item","numeric-id":1353977,"id":"Q1353977"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$6C64524B-90FD-427A-A3C8-4CCAA3A5D5E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7021c91f6a866e16b579f74b23aa54446a0c8938","datavalue":{"value":{"entity-type":"item","numeric-id":1150586,"id":"Q1150586"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$EB256618-08C0-4F60-9D3C-0AE49217C626","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a36780cb372ebe85c36f61a428142fe662be788","datavalue":{"value":{"entity-type":"item","numeric-id":3833654,"id":"Q3833654"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$6049BE06-9EBD-412B-BD28-8FAC35C23671","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba07dc7b075f512a5958344bc2487ab01c3f5b2f","datavalue":{"value":{"entity-type":"item","numeric-id":3786479,"id":"Q3786479"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$203D1AFF-3886-4773-90A8-DA6547A1E7C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"422e983d36cfecec9b58e1c37d6c18b89433801d","datavalue":{"value":{"entity-type":"item","numeric-id":1119576,"id":"Q1119576"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$65FC55A1-6116-4059-AA1B-E4F1CD1B7C04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22b880d3c8511f1d53c27d1537b521daf74193b4","datavalue":{"value":{"entity-type":"item","numeric-id":1102280,"id":"Q1102280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$F3D3903B-E164-420E-BE5B-435DFD413A18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65c8c8ed706a86d97db05d5b778c49fb79be8a30","datavalue":{"value":{"entity-type":"item","numeric-id":1144013,"id":"Q1144013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$FA0ED916-1F7A-4D71-90C6-40E40C3AD946","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8f84ad1f60a1f20714136e8ae5050c52673864db","datavalue":{"value":{"entity-type":"item","numeric-id":3778747,"id":"Q3778747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$DF511B62-D810-4E7D-AEED-9D6D327F75F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f70c7f0070211df81086d4c25b73a9ca61d45c1","datavalue":{"value":{"entity-type":"item","numeric-id":5686023,"id":"Q5686023"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$DD7770D9-C710-41AE-8F29-46CFDAEAD2D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d1b4998bdaf1a6b4855ad6d2b807b069f618a518","datavalue":{"value":{"entity-type":"item","numeric-id":4041554,"id":"Q4041554"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$F9A708FF-F116-4CBF-95A2-4C29BA473C13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$32BE5177-555B-40AD-B5E5-A86BB3AB8CF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9732b89c1ec3dfa5b9fdbcbf606dc155ea9b940","datavalue":{"value":{"entity-type":"item","numeric-id":1124375,"id":"Q1124375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$808C90DB-9E4C-4E20-ABA5-95FA2A5BDDD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"761227e28ec3092e559c7874757d0ce5e8b995d8","datavalue":{"value":{"entity-type":"item","numeric-id":4198749,"id":"Q4198749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$5B5B2672-07BD-486F-B4CF-640596463D0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d12bc73d12578e158c35548a9be50fc15f22baf","datavalue":{"value":{"entity-type":"item","numeric-id":5552146,"id":"Q5552146"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1814133$5C9FF015-88CD-43CF-AF47-2A789AD7C357","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8bb001512014a8546eb723f44ac77c4be954100a","datavalue":{"value":{"entity-type":"item","numeric-id":1176199,"id":"Q1176199"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"28a3f8726c76c365c2b54ef15c1dd8f6d7b0774d","datavalue":{"value":{"amount":"+0.857811450958252","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":"Q1814133$7BB42C4D-B7E0-47F8-9670-E6BA2B767C7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"57e6943612077152e63bbf51245bd888ad98d266","datavalue":{"value":{"entity-type":"item","numeric-id":1353977,"id":"Q1353977"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b84388c2eee5b559772ef8e8212cafe1c02180ba","datavalue":{"value":{"amount":"+0.7790402770042419","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":"Q1814133$7B78B806-0EFE-4317-B12F-A8626CFFC9A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"76521ef0b9a9547a8f59938bbd29b120175a7950","datavalue":{"value":{"entity-type":"item","numeric-id":1150586,"id":"Q1150586"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4c07bceb29d1c90d6f3a764069dee29282ac6229","datavalue":{"value":{"amount":"+0.759415328502655","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":"Q1814133$2FAD28C0-18E2-4CEC-B855-645F76C25D5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"52afda677e64159b16b4cdc4cb0de749df927f07","datavalue":{"value":{"entity-type":"item","numeric-id":4323033,"id":"Q4323033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"223c97544cf1f545e99da9eb536f25082afd7688","datavalue":{"value":{"amount":"+0.7147651314735413","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":"Q1814133$94923C87-D593-4584-8494-328A5042ED39","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A unification-theoretic method for investigating the \\(k\\)-provability problem","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_unification-theoretic_method_for_investigating_the_%5C(k%5C)-provability_problem"}}}}}