{"entities":{"Q2142080":{"pageid":2152823,"ns":120,"title":"Item:Q2142080","lastrevid":43592617,"modified":"2025-10-28T01:34:14Z","type":"item","id":"Q2142080","labels":{"en":{"language":"en","value":"Learning theorem proving components"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7532521"}},"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":"Q2142080$D52A703D-DAD9-4DE0-8168-6036F02740F9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9d1f9e741345fc58fcc791b901815741a14b9111","datavalue":{"value":{"text":"Learning theorem proving components","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2142080$5C168D49-86BD-480F-9EC6-4326BB542135","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9855ed229df39c4779aced87ac0226eb011e9da4","datavalue":{"value":"10.1007/978-3-030-86059-2_16","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2142080$E55484F5-1463-4971-9EE4-CFE31CA8B5FD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9d0e84ccf37fdb7305408634c4906ddced0fd802","datavalue":{"value":{"entity-type":"item","numeric-id":831934,"id":"Q831934"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$024B87B2-CABE-4BC8-80BF-188FCCEB9958","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"87dc4de4518b8db4a5efca79e388ac462c23bd10","datavalue":{"value":{"entity-type":"item","numeric-id":831935,"id":"Q831935"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$4B7179AE-4303-4685-BB66-56F20C6175F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8f262ccff1e45e707e9f2a40bf03c6342da98b7f","datavalue":{"value":{"entity-type":"item","numeric-id":831936,"id":"Q831936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$215C4E0E-0DCE-40E5-BEF6-0324A2BF2A03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dc204e2e78d924e815f2b640ec35c8c2356ad41f","datavalue":{"value":{"entity-type":"item","numeric-id":286786,"id":"Q286786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$6123FC73-226C-4BC0-B647-21AF974CD4DA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"12ef1e2e38c147b52c379a6993b1283d5267f8ef","datavalue":{"value":{"time":"+2022-05-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":"Q2142080$2E557FAE-F155-4C6B-B7B0-6C35E3B289C2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"419326dfe5fc4042553e7b3a89533146c4f0f28b","datavalue":{"value":"https://arxiv.org/abs/2107.10034","type":"string"},"datatype":"url"},"type":"statement","id":"Q2142080$2AE0B0F4-CD65-4694-9F9B-57331BBC558B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2142080$5345D6AF-6927-4B66-AC6C-E395D3A0CA86","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"42b109197fd99ab6d2226fb9ca2c576f1b28ad4e","datavalue":{"value":"7532521","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2142080$95BB7508-54E7-4462-85B8-75A660CF0CCD","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2142080$23F2AB25-D5A2-4C8B-9583-56382653781B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e0afe30fcd4cd25e8e8273c02ad48a97b4a0e001","datavalue":{"value":"machine learning","type":"string"},"datatype":"string"},"type":"statement","id":"Q2142080$89BB56B2-B471-4C5E-8E30-2CD065795133","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b0efe91da4df536f9ec53a9f276b6c2c113d29db","datavalue":{"value":"neural networks","type":"string"},"datatype":"string"},"type":"statement","id":"Q2142080$585F96C3-A64E-4E6F-873E-4E98627AFE5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"50e4e06d9e28eb2b5161a8b77486cae9897ae53d","datavalue":{"value":"decision trees","type":"string"},"datatype":"string"},"type":"statement","id":"Q2142080$673C0338-1B67-4F21-AF97-ED018A2595BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"115347500453a4ec7b19b9ba408e07f0aad14001","datavalue":{"value":"saturation-style proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2142080$02C161AE-2431-4DCC-BBB6-9B9956330C25","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ef7d8d889002a63e0639b409be5044891abe09bd","datavalue":{"value":{"entity-type":"item","numeric-id":25570,"id":"Q25570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$CA287757-B0CC-4506-9E9D-24EE3A35EB43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1e7b4d238eeafa5b21b1ef85a0d6b8900bfdc422","datavalue":{"value":{"entity-type":"item","numeric-id":15442,"id":"Q15442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$75DC7D87-7A08-499F-A209-63D7281F4BF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e46473070f3c81a2b3e6d8305bbf4ff6145b7c3e","datavalue":{"value":{"entity-type":"item","numeric-id":30553,"id":"Q30553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$B76B1B5F-ECB7-4656-B63B-E05DD10C5E97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2207b0b201a95a431b254bcb1c01d869b9f41774","datavalue":{"value":{"entity-type":"item","numeric-id":18972,"id":"Q18972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$DFCB0A10-E568-4AE2-B7ED-7EC7D1575F84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"90f139681161cf03fca3b88a13657b8b8fd37862","datavalue":{"value":{"entity-type":"item","numeric-id":25180,"id":"Q25180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$FCC4B20C-6114-41C1-87B9-050DEF0163F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"af7e320eaa043645fcae501eca102305f45924c7","datavalue":{"value":{"entity-type":"item","numeric-id":40341,"id":"Q40341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$41476A06-8845-47E2-8775-83A7C71A23DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"33061b9a75e57d93e8912d2c2b716b27d6bd52ab","datavalue":{"value":{"entity-type":"item","numeric-id":40369,"id":"Q40369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$8C913328-3D23-4AFA-80CE-50898E0EC797","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7be44aca757f3adf49e3de3f5c22cd533ea232ed","datavalue":{"value":{"entity-type":"item","numeric-id":14023,"id":"Q14023"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$D1D33B77-2635-49D0-9085-01D53FD142DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"484f589bd857c6ecd5604196ba88033adb11a795","datavalue":{"value":{"entity-type":"item","numeric-id":15128,"id":"Q15128"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$35706696-9938-4F8E-9D4C-F016259D4C01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b443b776731e3bc75eb79b752e7ef8c4cee2d97a","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$FD7819E7-6738-4C68-9E2E-22E1309067BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"82659ddd3b24a7f3c51a78eb5f25cc1e5d64df69","datavalue":{"value":{"entity-type":"item","numeric-id":17116,"id":"Q17116"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$F82188C7-791F-4209-8A8A-2B044D5E97A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1017108dce3983431546a14c274f65bc4aaae70b","datavalue":{"value":{"entity-type":"item","numeric-id":22154,"id":"Q22154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$E39C4B3E-AD87-4DEB-B3AB-145344773EB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9a2b0f9c4dd33c49f5265570edd12928048b0f2b","datavalue":{"value":{"entity-type":"item","numeric-id":27042,"id":"Q27042"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$C5F3DCC4-4A49-4F31-BB08-4D19F9F7BC30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"30c23680895c6c05b43b4be92074136c496750ec","datavalue":{"value":{"entity-type":"item","numeric-id":28682,"id":"Q28682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$C80AF4E9-5315-42D1-8942-A94537280C60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bf8fe40ec0751f683b8f31fdc6f7f38f8aa07409","datavalue":{"value":{"entity-type":"item","numeric-id":13328,"id":"Q13328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$9B8A59FE-36AD-47DF-95EF-5ADB3E74E8AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"dfaab4e4b81d1d345c01e1ea50dfc6f386089d8e","datavalue":{"value":{"entity-type":"item","numeric-id":18424,"id":"Q18424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$41B9B8FC-F0A2-45AA-BDDC-3A9DA27CA362","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":"Q2142080$8C992F7D-99BE-43FB-81BC-C62A144A7A2F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"41dbcafa968492981d374ba5cd241be4e70c0ebd","datavalue":{"value":"W3203136261","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2142080$DE27F1EA-6C51-4BD6-83D8-B3DE7A6C3E40","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a602a31ec5858953936704adacfb1f5bdcaed350","datavalue":{"value":{"entity-type":"item","numeric-id":972422,"id":"Q972422"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$90B0879D-2E6C-449C-B2D1-A8E726CA3BC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"29b0802dd9ffb89108bee25aa26120dffc46ad60","datavalue":{"value":{"entity-type":"item","numeric-id":2352489,"id":"Q2352489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$0FD5BCB1-EB4E-4362-8A8F-DC19983C2414","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ee178f7541c5d2ed1d6ee17e1e99ce6d2d8a20c","datavalue":{"value":{"entity-type":"item","numeric-id":5195271,"id":"Q5195271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$66927524-9F1B-450F-AE45-18159A759BCB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14a5c4940466d35f592e34f0c53a75faf97010cb","datavalue":{"value":{"entity-type":"item","numeric-id":5239436,"id":"Q5239436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$A0D24F78-BB31-42F8-BC59-53E5CF7F9E29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"23ae3186b750126567f78f8fbe4fd7d86109b7ac","datavalue":{"value":{"entity-type":"item","numeric-id":2305414,"id":"Q2305414"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$BA42AC80-0326-47C7-B0F0-5CDDCB31F054","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8bcc0d9e316dce27c0fcac4c4807f958b607a05c","datavalue":{"value":{"entity-type":"item","numeric-id":3043788,"id":"Q3043788"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$699CAA32-087D-4AB4-8888-686DC25A8DE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0df01f1f257aa4e0eda78a40444b30a121e95f5c","datavalue":{"value":{"entity-type":"item","numeric-id":4645730,"id":"Q4645730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$01C039D3-916C-4189-93F4-CAEFC3C4733F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"72ac173876e3ad53e523042bc23f91ca926212b5","datavalue":{"value":{"entity-type":"item","numeric-id":4197923,"id":"Q4197923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$48E1DAC0-6396-4C0C-8471-F75E39131B06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2cf2a467582e2ce551e8d6f09e937481123bd1d1","datavalue":{"value":{"entity-type":"item","numeric-id":5049022,"id":"Q5049022"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$85262848-83FF-4C4E-968F-E13DDC18C2C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88c40879f272ef5a6502ebde32e9a28415541bfd","datavalue":{"value":{"entity-type":"item","numeric-id":2817300,"id":"Q2817300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$79D3AAA6-5C00-4DC9-8584-F689FDBF615A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e74d3fce405174a77b93de2a6b609361e3b5e6c0","datavalue":{"value":{"entity-type":"item","numeric-id":2364687,"id":"Q2364687"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$CACB8A45-BC76-4764-88CD-15D86353004B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1183268b2373a892adc793bed6d4a85aecfed77f","datavalue":{"value":{"entity-type":"item","numeric-id":5145434,"id":"Q5145434"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$3C5C8853-3C1E-483D-B1A2-CF73381F80CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e14549321cbae3c57ae9ce6a9266b4af3d64fd4f","datavalue":{"value":{"entity-type":"item","numeric-id":286800,"id":"Q286800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$81827F69-A21F-4EA0-9870-574A27B05F6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42182537caf540a6b7314fdf96f3b68cb2793047","datavalue":{"value":{"entity-type":"item","numeric-id":4913865,"id":"Q4913865"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$04423C31-F202-4258-AE76-F87E3DE1C8BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c977752b01a4ec3d5ec723ab218362634b1da110","datavalue":{"value":{"entity-type":"item","numeric-id":5302898,"id":"Q5302898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$F4443482-6EF6-4D6A-880C-CF12E2A05213","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42c115dcfc03ba15799910de9e502a35693681ed","datavalue":{"value":{"entity-type":"item","numeric-id":4999300,"id":"Q4999300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$9B779DC8-801D-4B50-8B02-945C3F1BD387","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"69e114146a9d2d5e6b8c252e3e4a144fcee5ae9e","datavalue":{"value":{"entity-type":"item","numeric-id":1404981,"id":"Q1404981"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$FD1E01DE-D0DE-4311-B825-8E7138028D92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"847e3dcf8d17a4bf2ebc16dc465d8fb6ca2c9cf1","datavalue":{"value":{"entity-type":"item","numeric-id":4032144,"id":"Q4032144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$4B6B165F-423C-43BE-B011-13B79242EB61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"82adbe1fadc7a8a128bd8045765b97ddec9a4402","datavalue":{"value":{"entity-type":"item","numeric-id":5290112,"id":"Q5290112"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$2B5D741A-8065-48B9-9EB7-AF30C44F7AA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93fc8985b7898988b7d52edb5c0cd61c1b917df6","datavalue":{"value":{"entity-type":"item","numeric-id":3150301,"id":"Q3150301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$AD398B6E-0A07-411F-9DB5-A5206CC5A4A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f44b125cf3594b01960f6a5396e298346e4cfbbd","datavalue":{"value":{"entity-type":"item","numeric-id":2870167,"id":"Q2870167"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$AA786BCD-B601-49AC-81C2-30B3CEB0D38A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bbf7b4ce3ab96d4236a4c36e2f89589530011a89","datavalue":{"value":{"entity-type":"item","numeric-id":877826,"id":"Q877826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$2743EE84-C46A-4B7D-9CEC-3F7D935D783B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3087f1a7eb9309c1646d3032c16c6ac9f3d28d8c","datavalue":{"value":{"entity-type":"item","numeric-id":1923820,"id":"Q1923820"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$5DD8B686-9C33-4944-9BC4-6889D9595734","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"30c8a00cceb8775f7b63d56fa6e1a8b46f80e32d","datavalue":{"value":{"entity-type":"item","numeric-id":6488580,"id":"Q6488580"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142080$6EC22DD5-CBA1-401E-8028-5B67B9BCD7A0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2142080","badges":[]}}}}}