{"entities":{"Q2817297":{"pageid":2828035,"ns":120,"title":"Item:Q2817297","lastrevid":79428389,"modified":"2026-05-06T13:53:10Z","type":"item","id":"Q2817297","labels":{"en":{"language":"en","value":"Extracting Higher-Order Goals from the Mizar Mathematical Library"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6620490"}},"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":"Q2817297$08B37085-2CC4-4BA9-A396-088949187306","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c8735f9636cba092f1cb2332a189246300e97d9a","datavalue":{"value":{"text":"Extracting Higher-Order Goals from the Mizar Mathematical Library","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2817297$406C520E-1C54-46D1-978F-7824AA272778","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4a92fdaebc018a2db2671cb59a348ef783456e06","datavalue":{"value":"1344.68203","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817297$A61B35A5-8CE9-4B90-A624-FB838F189DC3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1a0c3bcb2f8d9af4d20c2c38144eddd2d212920b","datavalue":{"value":"10.1007/978-3-319-42547-4_8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817297$BE565858-63C0-4B7C-900C-ECEDEF235DD7","rank":"normal"}],"P16":[{"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":"Q2817297$6CE026AC-20F9-45C3-A35E-96AF8E0CE298","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"12a1f3f19dead339cd86bffa0b34dbb56772c8d8","datavalue":{"value":{"entity-type":"item","numeric-id":438560,"id":"Q438560"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817297$E6F3379E-6925-4224-80D2-41C178BCA309","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817297$8ABC3D64-CFF2-4EAF-9893-408128B72ADB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"85d9f70abb070df81833000bc59244d6fec26f1f","datavalue":{"value":{"time":"+2016-08-30T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2817297$4F1D5F25-A8A2-42D6-8434-5F1C78EEB41C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"efed738c6c62c43d596c0f74144953d2c1cc86f6","datavalue":{"value":"https://arxiv.org/abs/1605.06996","type":"string"},"datatype":"url"},"type":"statement","id":"Q2817297$5EFFE00D-860A-44BC-B29B-D019819F4EF2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817297$17569DC3-EF72-40B7-98CA-6EF125091DAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"0c6e71133293256880be082f6af9aa793c57d433","datavalue":{"value":"68T30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817297$C9EE465A-A17A-4581-B82A-3FE497622D10","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9d6eeef4a98477a50e96231a26e1a32b804f0520","datavalue":{"value":"6620490","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817297$226FE349-717C-4742-922F-11AC929164C0","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3a96a510fd7a7846523150dd8bb125ef8f415fa","datavalue":{"value":"formalized mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q2817297$40BB77FE-3F3A-42A9-B5E2-EFA05B7C7457","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b36a4092864d39bf9c99c5936b3d1261e44b9950","datavalue":{"value":"set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2817297$FD252AE0-2198-4DCA-ABB9-168E3AB031DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2817297$D2380AD0-F913-4333-A15B-A3DE58F4036B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2817297$9A91F8E7-F948-4D4A-822A-69813A1BCEDB","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"effe99d4b547ffcbc07915d8ced5dc197768f166","datavalue":{"value":{"entity-type":"item","numeric-id":15028,"id":"Q15028"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817297$D67613F1-C2DD-4CA9-9579-2553FAF3678D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817297$5D4E1BA0-340C-4744-AC42-534FB8024C4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"491e4169c914222bc349264f15b36cbf2c3ef446","datavalue":{"value":{"entity-type":"item","numeric-id":18920,"id":"Q18920"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817297$21BDEB57-AEC3-4507-BB88-C59C6811ECDF","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":"Q2817297$C2EDE13C-778D-4EA5-959C-2A595DB54090","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8617a61c90a632f23d3851deb94e1069d2479a78","datavalue":{"value":{"entity-type":"item","numeric-id":13268,"id":"Q13268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817297$306CF488-B5D4-46E5-B5F3-1FAE5EC35353","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":"Q2817297$1FA698A2-53A0-4115-B16D-154709DB9CE9","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":"Q2817297$B48618D4-3CEB-4507-BE12-1A599B81E97C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f831de5cb89874ccad2fa802a2051623531f60f1","datavalue":{"value":"W2401700265","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817297$CB7B6FA3-0358-4E44-A08F-D922671B3025","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a44f29a5847ba65ecb038e53a168893c35ebafbc","datavalue":{"value":{"entity-type":"item","numeric-id":287283,"id":"Q287283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817297$31DEC96E-DF3F-4B57-9404-12A79AC37DDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"981b322b800f12891beed18d9218a5203bf47bb6","datavalue":{"value":{"entity-type":"item","numeric-id":2351156,"id":"Q2351156"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817297$E2D696B0-71CF-431C-B29A-386CC32A33C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ca7e027091589776f78a6d7ad8457e805c17b28","datavalue":{"value":{"entity-type":"item","numeric-id":5777498,"id":"Q5777498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817297$170CB41A-B341-4444-9EBB-6E195A8B51AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb1bab11b75e766c233c3a1b9a3682b90b0e288d","datavalue":{"value":{"entity-type":"item","numeric-id":3075247,"id":"Q3075247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817297$59438C05-A545-4861-93EC-E9E730B87AF1","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":"Q2817297$CF04EFDA-A54C-4DAA-8370-ADCAFE1E0986","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea4ee858c8544ddaa2b36ea8b7a73636ae5df893","datavalue":{"value":{"entity-type":"item","numeric-id":3075241,"id":"Q3075241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817297$43776C44-66FB-4E3E-BC1A-9923AEC40A1A","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":"Q2817297$C8604D7B-7D85-4B3F-92B3-894E3054FE39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fbe0bfb57e9a97e56fde1afbd62d0dd2171c33df","datavalue":{"value":{"entity-type":"item","numeric-id":4413895,"id":"Q4413895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817297$D0754ACA-B684-4976-B91B-709D57254A93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6dbaa83286082fe9f22efc1424c5503085916666","datavalue":{"value":{"entity-type":"item","numeric-id":556682,"id":"Q556682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817297$BD4F3B08-4528-4676-A851-4A7A627FFD58","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e4374daf952f95be8e2d6a4ef5e2444e3d0d7712","datavalue":{"value":{"entity-type":"item","numeric-id":1663215,"id":"Q1663215"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ea763337fcee4eb45fd6686cdbf1fbbef74d9c3b","datavalue":{"value":{"amount":"+0.8175516","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":"Q2817297$4715F38A-44AA-4F36-A73E-F03F21962109","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"67a3d5521b29996331a45ad34eb7677199d8821a","datavalue":{"value":{"entity-type":"item","numeric-id":3817652,"id":"Q3817652"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"26d7370125efba33e39227ef174888c74e760559","datavalue":{"value":{"amount":"+0.809951","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":"Q2817297$C9FBEA57-C52B-4495-B80F-D58E08503631","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f4eef3238e053673e5f2138d4ee0ca8244d61e34","datavalue":{"value":{"entity-type":"item","numeric-id":5478219,"id":"Q5478219"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"960b542da3996a3dcfbf2d46304ab851e8434961","datavalue":{"value":{"amount":"+0.8046999","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":"Q2817297$46B983AA-3ECB-4774-8B2E-060A09A9CFFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bfef95c0cb096f65c22795035488c2b360de8b40","datavalue":{"value":{"entity-type":"item","numeric-id":2128826,"id":"Q2128826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9ea26ee27f66d81ca0a6319a600935668d1c828a","datavalue":{"value":{"amount":"+0.80380636","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":"Q2817297$65A2A06F-A3AF-40CF-AC92-D5660B73C86E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e0a3e291f1f17745f7efdf0798b5008ce6b5f5c7","datavalue":{"value":{"entity-type":"item","numeric-id":3582702,"id":"Q3582702"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3f30303c790bc31f5cf92bcfc59dbb39e62391f4","datavalue":{"value":{"amount":"+0.8036494","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":"Q2817297$A74B2E1E-87D3-44E9-B629-B9FE452A9AEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0271ffbb32b0fdb034b4f062bb270688ee9018cb","datavalue":{"value":{"entity-type":"item","numeric-id":2907308,"id":"Q2907308"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e318b60821fc4c28eaa262d7fca6bba9ff9be7f1","datavalue":{"value":{"amount":"+0.80035776","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":"Q2817297$8D7DD583-6B67-4906-B44A-C3E17F97C4F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e98a1ac5e1e0750982163e99ad44cc64592a91c9","datavalue":{"value":{"entity-type":"item","numeric-id":5313078,"id":"Q5313078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8b40302905ea2ab73f6a5fe9c180bb6843ae0c7a","datavalue":{"value":{"amount":"+0.79858637","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":"Q2817297$CFCB844D-1F07-4CE6-AB7A-2ECFFF5F8E69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"20697fb65b6ee9dff2d0ffd90078477d2a09c589","datavalue":{"value":{"entity-type":"item","numeric-id":1273761,"id":"Q1273761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0e2f6b9f08f609d1b366bf2316c515571ee8de37","datavalue":{"value":{"amount":"+0.7934014","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":"Q2817297$59419EE7-7FB4-4320-BDAF-C8F8B1C654C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3db6d199add8d33f3d913b30a13b7b56d2fd080f","datavalue":{"value":{"entity-type":"item","numeric-id":5200124,"id":"Q5200124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6e4f5ac1d2c42dfb476fa45c2101440807c30e40","datavalue":{"value":{"amount":"+0.7926756","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":"Q2817297$3FD757AA-7226-4623-AF34-09E894245DCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5d6e7ff84088819a25ed793fb074d2a2fc79df09","datavalue":{"value":{"entity-type":"item","numeric-id":2576573,"id":"Q2576573"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"10112c97a03b998528a7a83d356c36545d053b9d","datavalue":{"value":{"amount":"+0.7916769","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":"Q2817297$024828CB-262B-48C2-AEE3-503864352AD0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Extracting Higher-Order Goals from the Mizar Mathematical Library","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Extracting_Higher-Order_Goals_from_the_Mizar_Mathematical_Library"}}}}}