{"entities":{"Q5495946":{"pageid":7525506,"ns":120,"title":"Item:Q5495946","lastrevid":52059980,"modified":"2026-01-20T20:48:42Z","type":"item","id":"Q5495946","labels":{"en":{"language":"en","value":"SAT-enhanced Mizar proof checking"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6327284"}},"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":"Q5495946$6CB3521C-D56C-40AD-89A1-210B767856B1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f1bea89f4bddb5674b35ccee8a453890949d7c30","datavalue":{"value":{"text":"SAT-Enhanced Mizar Proof Checking","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5495946$6BB2EA81-ADCC-4C56-BBD9-C1C5D8CC490E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"59639b08615310856bdfb5499cac3ad6c354f94d","datavalue":{"value":"1304.68159","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5495946$E8F97646-EBE0-4F8F-9E29-6B2263F57E33","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0878c6654ec031dc96ba8542457d8e093937ab3f","datavalue":{"value":"10.1007/978-3-319-08434-3_37","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5495946$E3C6C009-A4E5-4F70-A2CE-E1BFB837E287","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2d21f7099afeef01813dafa96d5f9f9c05717b38","datavalue":{"value":{"entity-type":"item","numeric-id":226646,"id":"Q226646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495946$5543E950-C5D7-4979-B2C7-7DDB1B233082","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":"Q5495946$83504DBB-34DE-41E6-B66C-AB09ED780F81","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1c94d745affbb1f035e3911adf053858df897bb7","datavalue":{"value":{"time":"+2014-08-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5495946$4A7B2A20-22D3-40B6-9692-C03EB23586F3","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5495946$0E052AB5-EBBA-4CC6-82B1-79932A1EF45E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7b0f25d0fe27fa4b6efdc9d8823c33ef0d33fc23","datavalue":{"value":"6327284","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5495946$0594E685-BE5A-4E61-8857-B588EE46EA3B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"571c0e1fb7a78a4a545c4f12cd6536c1efe33bd7","datavalue":{"value":"Mizar","type":"string"},"datatype":"string"},"type":"statement","id":"Q5495946$5A975642-C692-44E9-B50A-2EDC7D11C9BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5867ec7b44aefc01672736513dfe6410a0300cd5","datavalue":{"value":"SAT","type":"string"},"datatype":"string"},"type":"statement","id":"Q5495946$B7296640-0500-4F87-896A-D94D1E7D5FEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a5907ed38d4372c65ffffb842db7415cc2c11751","datavalue":{"value":"Boolean operations","type":"string"},"datatype":"string"},"type":"statement","id":"Q5495946$0E06A211-CE67-43FD-B1A1-A6B5FE67D03B","rank":"normal"}],"P1463":[{"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":"Q5495946$33A0ADAE-5F52-4513-BC58-DAD067EA9E24","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":"Q5495946$AE83B515-E374-498F-8A84-22C63C3419AC","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":"Q5495946$6F58ED50-10A1-4587-97C4-01A6F57F86F8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ace486b3c59555e43fd0b940b5d171dcba11b6a2","datavalue":{"value":"https://doi.org/10.1007/978-3-319-08434-3_37","type":"string"},"datatype":"url"},"type":"statement","id":"Q5495946$AB60A698-D045-486A-A795-1F116D7A4D08","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6d821686b9378d920406875280016a45ce59eaf6","datavalue":{"value":"W731109","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5495946$E9DCD666-4564-437C-882E-B631E290B1F3","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"604f23db2dd4d34a2f60254ad57a8915830982b5","datavalue":{"value":{"entity-type":"item","numeric-id":5200114,"id":"Q5200114"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495946$0FC15D0B-FAC2-4B66-A025-DF9867D41218","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb15445443b7a8677c7ef043ed8530f20d54b0c3","datavalue":{"value":{"entity-type":"item","numeric-id":3100209,"id":"Q3100209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495946$63BFCEDE-3634-47E1-B8F3-1BA57426A3D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a90c65b7b8a3408028ec705f138622371d07227a","datavalue":{"value":{"entity-type":"item","numeric-id":1945910,"id":"Q1945910"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495946$B1FA4F40-9B08-45F4-94F6-B61C3E65451C","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":"Q5495946$C2613F62-600E-4A76-A3FE-CC62ABBF1257","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"887efd17320625725aeddf6391561534d8fcc309","datavalue":{"value":{"entity-type":"item","numeric-id":5428273,"id":"Q5428273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495946$B3859486-3D2F-4821-B1EB-F2107E5EC7E7","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":"Q5495946$83E8C33A-5015-4A15-91C3-2B844B13448A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"692645ba0e13e1ab798946ded35053c7569206ce","datavalue":{"value":{"entity-type":"item","numeric-id":2907348,"id":"Q2907348"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495946$14295D02-1A29-4917-A4DA-8C1815A2172D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"436d8267b8b601e92bc0ef555ffe6911eece93f5","datavalue":{"value":{"entity-type":"item","numeric-id":1945908,"id":"Q1945908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495946$0C987885-7F88-4443-96B1-15448B779FAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"990bcb4a0d41c18c68d7c9cdd2cf6abe242dc9f7","datavalue":{"value":{"entity-type":"item","numeric-id":865630,"id":"Q865630"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495946$41723B13-3A6C-4DA0-9478-D15FFFBFA536","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cc4b8a556b0ebfab4e780293fc359a3bb7afe7da","datavalue":{"value":{"entity-type":"item","numeric-id":5852118,"id":"Q5852118"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495946$DA606347-3020-436C-B7F9-76289E8F3FB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec41d91b97fe450aba006d86ee1b6e337fcab2ff","datavalue":{"value":{"entity-type":"item","numeric-id":5313068,"id":"Q5313068"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495946$243B147C-2C21-4174-B852-6D14EF5E880E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c852981cf03ba0205dbadf36200c00bb56793d8c","datavalue":{"value":{"entity-type":"item","numeric-id":3183518,"id":"Q3183518"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495946$FAE36382-82F6-4C3C-9E79-7A2248061DA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5a256449611c84a11b081fc6ab121a5b321e50f","datavalue":{"value":{"entity-type":"item","numeric-id":1945902,"id":"Q1945902"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495946$2B52BC6E-AC75-4D87-BB86-269066B0C87C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ed473c6e01919b49d2a3d56d48fd6fe4dac1c845","datavalue":{"value":{"entity-type":"item","numeric-id":1945905,"id":"Q1945905"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495946$087EAC7D-4B90-4E67-BA08-5B957ED8393C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"68cbacb60d35dbbb3c8a2da4db65e98f0f2f0898","datavalue":{"value":{"entity-type":"item","numeric-id":2848690,"id":"Q2848690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495946$87669C37-CC7F-4B99-9F50-C9517E8EBD7D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ab7e5fbdc6c2b3a12f649e72dff75f5485ad2e9c","datavalue":{"value":{"entity-type":"item","numeric-id":286803,"id":"Q286803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"75fc9b4d50276b0517a6bcfc11a18e71600ad470","datavalue":{"value":{"amount":"+0.9342390894889832","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":"Q5495946$3E6D369C-CE29-4BAD-9396-7DC07A36529D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"32781204d1db0d50f0fed8e58f21ef2e924a069d","datavalue":{"value":{"entity-type":"item","numeric-id":5327347,"id":"Q5327347"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"939275dbdf8f59fe5f2ea63a228dba1217e3bbbb","datavalue":{"value":{"amount":"+0.7526238560676575","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":"Q5495946$1D974465-6E97-46B4-8C1B-69D62D30F5F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"011f28f1bd0481f20174e5f049ee296de6638d11","datavalue":{"value":{"entity-type":"item","numeric-id":5495936,"id":"Q5495936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6c4466d55dd9ab5d4104b31e91a34a512c3dcd8a","datavalue":{"value":{"amount":"+0.7499364614486694","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":"Q5495946$19E442D5-78E8-4F4A-941E-72672F02372A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12a132e4daa2e15bd5dc269ad3507f16b279f28c","datavalue":{"value":{"entity-type":"item","numeric-id":1687744,"id":"Q1687744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"df3e2ba3bae991ebdbc29851bcc69314ed576ae6","datavalue":{"value":{"amount":"+0.7477262020111084","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":"Q5495946$1DED366B-E2BB-4AD4-AC82-BDB411A956AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eee2626a7ebeafe9534d0338c5aeb25841f2e563","datavalue":{"value":{"entity-type":"item","numeric-id":2867936,"id":"Q2867936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e7f73a4ddb163181395d869968129f1d950c9ae2","datavalue":{"value":{"amount":"+0.747573971748352","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":"Q5495946$54FE89D1-B771-48B8-96FD-C757336951C9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5495946","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5495946"}}}}}