{"entities":{"Q5168887":{"pageid":7198459,"ns":120,"title":"Item:Q5168887","lastrevid":41530599,"modified":"2025-05-05T05:08:27Z","type":"item","id":"Q5168887","labels":{"en":{"language":"en","value":"Proof-producing synthesis of ML from higher-order logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6318864"}},"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":"Q5168887$E52AA140-35F3-4B74-9461-FF3F35FD14AC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f22df23be3e30b5224412fa06d3d486e09b475e6","datavalue":{"value":{"text":"Proof-producing synthesis of ML from higher-order logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5168887$279E828A-770D-4EEB-8773-55C77C662B09","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9382a652898bdef07a0ef23f73dc7249ec75e1a1","datavalue":{"value":"1291.68364","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5168887$894F0072-4187-49C1-87B5-50E37EAC71B4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"da631b776cd1975cf72aa7ca79bfefadbe330c46","datavalue":{"value":"10.1145/2364527.2364545","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5168887$83930C28-A68C-4B3F-A076-1DA0F4939885","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c330e55e5dc72ba4e46dcf35457734e0df28701e","datavalue":{"value":{"entity-type":"item","numeric-id":286789,"id":"Q286789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5168887$6A5A3729-C26A-4F52-BB0F-BD94670B234C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"57155b56d8fbcd7c5881cc6580886a49385bb630","datavalue":{"value":{"entity-type":"item","numeric-id":287360,"id":"Q287360"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5168887$29BCEDBB-1F7B-4582-A2FB-F3B8B6D20D28","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"124eb001557b71c36d00fbe6c3c8f1624c5e49b8","datavalue":{"value":{"entity-type":"item","numeric-id":5168876,"id":"Q5168876"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5168887$F86A2F81-359E-4C5F-A4FC-C87D83BDF15A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5670447523ca0c92d2715e5586c267824127db6a","datavalue":{"value":{"time":"+2014-07-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5168887$E098B614-E561-48D5-BDDB-F23E4E2B0C21","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5168887$CB9A621E-F535-4222-B7BF-0FB375D01484","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5168887$E15004D3-B934-46BA-8A08-FDCDE7DCD7CE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ee594cbf8aa274128ac920e03d00a9771cd1dc5f","datavalue":{"value":"6318864","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5168887$E24D9E32-2C47-4629-9B02-57F8E381612A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5168887$6B223BCF-5335-484B-AA91-0243C50EC9C9","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5168887$D886D482-89AC-4321-A449-C02803678F42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5168887$D9FB9889-849C-4191-9F4A-0E2B44D4ABFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3385954e206fa4a5bbcdde66dd867f18c8df62c","datavalue":{"value":{"entity-type":"item","numeric-id":25202,"id":"Q25202"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5168887$3102221C-2BEA-40CF-8CF8-979A5229719E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"067e00213990a6f2431e78667be3f10443c92f4f","datavalue":{"value":{"entity-type":"item","numeric-id":16052,"id":"Q16052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5168887$2B93EC70-18A5-41D8-8C72-BE3478E3CA13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b0996c451b14a06853df9996b5aeda4f0ca33756","datavalue":{"value":{"entity-type":"item","numeric-id":21900,"id":"Q21900"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5168887$8F902DB6-A0F9-4FBA-BD18-192D61DBFFBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5168887$1C62BB49-F902-4477-B34D-9BE4D16D5A86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e079f4640d565f0ca1930fd327c2c7e8d634508","datavalue":{"value":{"entity-type":"item","numeric-id":21954,"id":"Q21954"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5168887$5A70B562-61BE-4BA3-882A-F691BDE8FAC6","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":"Q5168887$317730BF-81C4-4BE1-AA0B-3BB5958C6FA0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"243742fe8aad15d9f6f916d282a1ec4037df616f","datavalue":{"value":"https://doi.org/10.1145/2364527.2364545","type":"string"},"datatype":"url"},"type":"statement","id":"Q5168887$F80EEAC0-8A82-4C3F-BE46-1359CF5F95F2","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"70ae246ada9e89cf6f58a3c18d536c2fac075755","datavalue":{"value":"W2014904806","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5168887$17137E60-0FD3-4764-815C-52A639FB5A6D","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"330b0da8a246360524e867102971d6a4d411e606","datavalue":{"value":"Q130892422","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5168887$0582EEFF-45F6-453A-A67C-1862584AAA5C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f111eac5ad767c0299626bb8fc33167280082866","datavalue":{"value":{"entity-type":"item","numeric-id":2875232,"id":"Q2875232"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"455e9474b1b91e14d717b9987325ae93204f9651","datavalue":{"value":{"amount":"+0.9328683","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5168887$74739ED2-FF21-4A9D-8E81-5F1DFE0B68B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8139328ea45d0f5f4bbb53ec8e07615b518a5b98","datavalue":{"value":{"entity-type":"item","numeric-id":3578399,"id":"Q3578399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e4585b11bdeab3a4fe8b7852a50b7ad38c662b1e","datavalue":{"value":{"amount":"+0.89473176","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5168887$EA7CC745-FE90-4193-BB4F-7C8840D62ACB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"51c43955591539e50976eb74d7dbd4932e5ad95b","datavalue":{"value":{"entity-type":"item","numeric-id":5756497,"id":"Q5756497"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6da22f5c81f248a64f9ef89f6f3b61fe0299192b","datavalue":{"value":{"amount":"+0.89384663","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5168887$7819AEC8-925C-4B9D-B7EF-C4ED99644967","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"779aa4f2e95d3d3e046cbe92464281ba0bd157d8","datavalue":{"value":{"entity-type":"item","numeric-id":2767046,"id":"Q2767046"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce18e06470b980c61a96d832eb89267c512ee5e2","datavalue":{"value":{"amount":"+0.8933061","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5168887$E39E32E5-230C-4559-B419-1969AFD079C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ef2474b32099b78c48d4ab881bafa7e7510e12fa","datavalue":{"value":{"entity-type":"item","numeric-id":1863751,"id":"Q1863751"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1633bdbf08163c6cf49fd04753d79bd4339f6a3e","datavalue":{"value":{"amount":"+0.88904035","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5168887$8579C41F-C879-4E97-804E-069192839157","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"116ae40af25df1caab31ce7865056cc8623f9e19","datavalue":{"value":{"entity-type":"item","numeric-id":3789101,"id":"Q3789101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8b99f2ccc11b6db6daecd562d9ea2faa53d0087b","datavalue":{"value":{"amount":"+0.8849426","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5168887$EB1440B6-82E6-43DE-A69B-AA69A261949A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"63a46bd3760e1b0c1fcd3d657458ac5072d228b4","datavalue":{"value":{"entity-type":"item","numeric-id":6040535,"id":"Q6040535"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9489494ec5c89f64e88b3bf7807eb3a3109b2da4","datavalue":{"value":{"amount":"+0.879012","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5168887$BBF09AC5-953A-4CB5-95E4-D8D27AEE66CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"613cfc2da30320cd624d30ebde6646a607d9e907","datavalue":{"value":{"entity-type":"item","numeric-id":4812964,"id":"Q4812964"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"56b6ab470f99fc9513a47e6b8c08e250f7be592d","datavalue":{"value":{"amount":"+0.87249863","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5168887$F12EDD8C-A68A-46DF-9392-FC15502A8B8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9556bf7f6ed0e05daee465305db68b6b32bd1c8c","datavalue":{"value":{"entity-type":"item","numeric-id":2208292,"id":"Q2208292"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"44817c64842ce6a073a5af58c8b8e55ac42a262e","datavalue":{"value":{"amount":"+0.8723388","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5168887$0D5D11EF-9603-413B-85E3-FD7DB5CF7C1D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5168887","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5168887"}}}}}