{"entities":{"Q286803":{"pageid":288570,"ns":120,"title":"Item:Q286803","lastrevid":56653254,"modified":"2026-03-18T10:18:09Z","type":"item","id":"Q286803","labels":{"en":{"language":"en","value":"Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6585260"}},"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":"Q286803$F79AE58C-B0EA-4633-9E3F-E83B8BAC3CD0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d00fba5f31315b07ed58daacf3abfbfb37445191","datavalue":{"value":{"text":"Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q286803$9E34FD5C-A306-4FCC-AA22-E46F6C61CB5C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e9295878b850cedba0c2b96a9c8fd4b8b764d3f7","datavalue":{"value":"1356.68197","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286803$63B88DB8-22F8-4452-BF9A-BBEDBA8E2A80","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":"Q286803$7A8A3DBE-8F81-4F5E-A6F8-9B2FE6633BA7","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286803$29B20E5F-7976-41F6-BF45-6F31E3ED182B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b626bb78b3e93b3076e6958296f7f25e2e74c3ab","datavalue":{"value":{"time":"+2016-05-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q286803$BE94CC3C-19B4-41C7-BF8B-91B1DA5DAD7D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286803$C4B299BA-9747-46FB-8EF0-A59F3EED1991","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f6a6a94f8b391816e235b1d0ac2106e156bd1e60","datavalue":{"value":"6585260","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286803$8A5A8480-5563-4647-B21F-616D60F23DE7","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"571c0e1fb7a78a4a545c4f12cd6536c1efe33bd7","datavalue":{"value":"Mizar","type":"string"},"datatype":"string"},"type":"statement","id":"Q286803$E314CF8C-730D-4779-9FD5-3679B094C4E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"543c7d0ffd0c52aa92a423848e3694a5bcbfca1e","datavalue":{"value":"SAT solvers","type":"string"},"datatype":"string"},"type":"statement","id":"Q286803$43381359-D4DA-429F-9D41-E352129D16A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q286803$D1C01A61-B92E-4B79-98ED-ECDC5205A449","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a5907ed38d4372c65ffffb842db7415cc2c11751","datavalue":{"value":"Boolean operations","type":"string"},"datatype":"string"},"type":"statement","id":"Q286803$72E1EDA6-1A45-4A15-B34A-4F8E94034F67","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"fcdc2096af312acf049bf0e86081e35578a1e139","datavalue":{"value":"Q59407645","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286803$0B41583B-F280-4062-BEE1-29EDD23ED720","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":"Q286803$43CBD876-129A-48D4-B99E-77DF271AB9C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8449db7d9aaa28101ba7b0de8e98d9c446365070","datavalue":{"value":{"entity-type":"item","numeric-id":13332,"id":"Q13332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286803$4BCECF97-3044-490B-A3DD-45F0B56E98C0","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":"Q286803$44A7149C-6C18-40FE-9480-B957F3F655E9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f856f8117b9c521431b6b021a4407e9c63213841","datavalue":{"value":"https://doi.org/10.1007/s10817-015-9332-6","type":"string"},"datatype":"url"},"type":"statement","id":"Q286803$3C7ECE40-CE05-4982-B3C7-9C08EC9AD34A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"719ec984c6d37874d3bf03d20f2cc95c24950d08","datavalue":{"value":"W2146945204","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286803$9EA9BA7F-6D61-4AA1-9A4F-5944D6EF1313","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":"Q286803$262211EA-6968-4479-B14B-5041D09160F2","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":"Q286803$20DC8055-B80A-4D8D-AEED-5B4F013F2C9B","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":"Q286803$9C7ADFA3-750E-4790-A1FF-913E5606DD53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"37ee76102b0711d762453c86d361aa67599071c0","datavalue":{"value":{"entity-type":"item","numeric-id":5411648,"id":"Q5411648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286803$913DA02E-C155-4302-9BAE-2A986BF45F98","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":"Q286803$93D4F01F-2612-44D5-85B5-3B3683FD7B81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7489ea30e71537d01eea3d2bdcb704e187c3f139","datavalue":{"value":{"entity-type":"item","numeric-id":5898511,"id":"Q5898511"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286803$791AB92B-1E1B-4C0A-A01B-A5C18573ABC8","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":"Q286803$084DD0CC-A567-4807-AD20-CA8BBA175EA0","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":"Q286803$4FF40A38-2630-4D9C-85EB-E22EBB728DF6","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":"Q286803$2A942CEB-8ECA-4780-880B-8BAE074F6833","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":"Q286803$9EC2EB48-134C-4C69-9FB9-82C01B4F008D","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":"Q286803$1B18AC2A-16CC-4800-BD33-1958266CBE99","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":"Q286803$33B1BD75-80DF-49A3-9B71-FF48CC95BD06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3e3646434a793683f3ce5f6c7fec296d0992d7ea","datavalue":{"value":{"entity-type":"item","numeric-id":5495946,"id":"Q5495946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286803$04AE8709-E952-49A8-9E9C-FBE1D769628E","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":"Q286803$6859716B-3040-447A-8EB5-90EB825E00BE","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":"Q286803$E21D5019-E035-4F1E-B65E-429447D07146","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd2efa9cc52b9c7802bc3fd73236ab4bbd639fe4","datavalue":{"value":{"entity-type":"item","numeric-id":2921120,"id":"Q2921120"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286803$D16B5595-00FE-4E99-A72E-DE2FEC0D8ED7","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":"Q286803$02B94957-4CDB-479A-A92E-523CA7317263","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":"Q286803$2E918A68-2AD6-486F-A075-1FB840966268","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":"Q286803$5E4CF26A-6CDA-428C-A9B6-C3C9248204B2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"17c8e4f0ab3b0a31636839b3f4e8ced7336c8ec2","datavalue":{"value":"10.1007/S10817-015-9332-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286803$ABE48D7F-0207-4357-86C6-768DD38CFE94","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"812901582798120cd938d3432542fdfbb3946dd1","datavalue":{"value":"journals/jar/Naumowicz15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286803$D3EE7DA9-A3DF-4522-8EF6-2A16C4CEF419","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"27373e9765b2c26bba3a2e86e765725edb6a01aa","datavalue":{"value":{"entity-type":"item","numeric-id":5495946,"id":"Q5495946"},"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":"Q286803$201CC22B-ABFC-40EA-8812-5C6BF09E2EDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a6b2a937bce5baa1e44f54c9029c4c73e58425d9","datavalue":{"value":{"entity-type":"item","numeric-id":5325885,"id":"Q5325885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ab16ecd9cc2e5184706dfbcf0f78a53526fecd50","datavalue":{"value":{"amount":"+0.7289717197418213","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":"Q286803$93511139-7B28-46E6-BF8B-A73F8FA98FD4","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":"4eec52ec1afdac5509790756bc4027576a8aaecf","datavalue":{"value":{"amount":"+0.7275530099868774","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":"Q286803$57C5CA66-FAA0-4A7C-BE8E-FB6A455DEF00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3667c1f3900d5b4fe1d73bc643a4514133908e4d","datavalue":{"value":{"entity-type":"item","numeric-id":2848690,"id":"Q2848690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e559919137d55e697bafb325985c8d7fa431559e","datavalue":{"value":{"amount":"+0.7275115847587585","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":"Q286803$4924BAC6-1C7C-44CD-B1BC-F88FC867DF4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"650fb4121216a624ee646be9799d3418d3867838","datavalue":{"value":{"entity-type":"item","numeric-id":4571125,"id":"Q4571125"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"43e5fdfa7339b17ac71cdf0cfc364b227f95567a","datavalue":{"value":{"amount":"+0.7259222269058228","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":"Q286803$6A4197E9-2032-4C3F-A36B-B098AB2D274D","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286803$38A6CEB9-7CAD-40BD-A092-6EEEAE52982B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:286803","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:286803"}}}}}