{"entities":{"Q841684":{"pageid":843532,"ns":120,"title":"Item:Q841684","lastrevid":64743153,"modified":"2026-04-11T21:56:12Z","type":"item","id":"Q841684","labels":{"en":{"language":"en","value":"ATP-based cross-verification of Mizar proofs: method, systems, and first experiments"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5604863"}},"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":"Q841684$8095C536-7A3E-4396-8CC5-C1701CA5619D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f1d072a943db537b8ee940db04311837c95fdcf1","datavalue":{"value":{"text":"ATP-based cross-verification of Mizar proofs: method, systems, and first experiments","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q841684$934C1D8F-6692-43F8-8BAF-30E363EE2123","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3019fa09c57cc57ec6c0927813de3b7c95b6e121","datavalue":{"value":"1178.68532","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q841684$0D4E6190-D9E0-433A-B50D-0E8D545A5D16","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":"Q841684$D7112B19-3B1B-4956-B636-40DE247AF4FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6c6d707c999cc6d62a42a2f34c4e05c6ede74383","datavalue":{"value":{"entity-type":"item","numeric-id":679254,"id":"Q679254"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q841684$BD700BA3-C293-4A85-B1F0-25EF3FA458BF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e5cf57799e8c41ecba181c21bc95047b71cb3443","datavalue":{"value":{"entity-type":"item","numeric-id":294368,"id":"Q294368"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q841684$C6065DC3-080D-480B-A22A-3BE57B3EAE2C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"451aedfc73897067ccbcfa807e7fb1e08f2a62a1","datavalue":{"value":{"time":"+2009-09-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q841684$F648C3B5-14D1-40B9-987E-DAC60F019A9A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q841684$6129EB9E-3361-4928-A9FF-813039164799","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q841684$3611F875-FC83-473E-9339-495017DF7BCF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"675bb99443c23ace1be4429d494f48fb73ca12ab","datavalue":{"value":"5604863","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q841684$C2B5EA49-45B4-44F5-9203-1BECC899499A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3a96a510fd7a7846523150dd8bb125ef8f415fa","datavalue":{"value":"formalized mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q841684$E9440942-DF3C-475F-A0EF-B6B1557CAD13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ca1042868ff4f694776e4b2c62ec66638c4ef91","datavalue":{"value":"automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q841684$753D77C9-1E69-4391-B4C1-F7B2794F3300","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q841684$5199ECE0-092F-4A8A-B250-F66581737320","rank":"normal"}],"P1463":[{"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":"Q841684$A48CBAF0-C6A1-4205-9795-D6DED1856230","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":"Q841684$71A2A105-C395-4721-AC92-AB7C3AF14F22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c6f90a2f4d38316e0bb5a27c4b90cf6cce495aa0","datavalue":{"value":{"entity-type":"item","numeric-id":16295,"id":"Q16295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q841684$761E1C29-3777-4CC7-8CA4-629E8BAAB207","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q841684$A63D3E73-8E17-4FDE-81C8-50F49F352BF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b222922e2b373ab7fb2b7a049f9de07c755ee255","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q841684$1141CC8C-3DCB-4B19-883A-4C499EE2BAFC","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":"Q841684$D6B7E434-577B-45F1-A7CC-64BF996F82BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"233bd03fc74bc4c01e6f828569e5eb13f94bb747","datavalue":{"value":{"entity-type":"item","numeric-id":22242,"id":"Q22242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q841684$70B969EC-22BF-4C78-8D18-B7923FFCA0AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"62af2c5e450adf37bd9acb47c5a55b60b68447ea","datavalue":{"value":{"entity-type":"item","numeric-id":22241,"id":"Q22241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q841684$11D4C46E-214C-4169-8CB4-5E147DF98C55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"133e2e5701b3435e4a72bb2a6345ff9894f7c6da","datavalue":{"value":{"entity-type":"item","numeric-id":22369,"id":"Q22369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q841684$CDC59D31-7B83-4E41-B2B0-6E1A332EC13C","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":"Q841684$A5C51782-CE56-4A9B-80E8-13DDDDAA2A01","rank":"normal"},{"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":"Q841684$05216E45-D99F-497D-B577-CF1F27DFD828","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":"Q841684$7F9837A3-C645-4EA5-80E6-D9B791B9ECA3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"850fd357eaaa71d89dc31a68d3fbb401f601c505","datavalue":{"value":"https://doi.org/10.1007/s11786-008-0053-7","type":"string"},"datatype":"url"},"type":"statement","id":"Q841684$68C3DC81-8BDA-4668-A774-0D38FB0E522A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e1629382ec1164698f4c557f167ea78f0d927ba0","datavalue":{"value":"W2066619351","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q841684$D99BC1B3-77AD-4608-B675-6B6CEA13A09C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"56d0f9259a7d5be6c864abda0d4e62a667cf4d03","datavalue":{"value":"10.1007/S11786-008-0053-7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q841684$CF045725-782B-4FD5-805D-A2E3A91675EC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dc7d0d0e673a89709ca9dd925911f5841e040887","datavalue":{"value":{"entity-type":"item","numeric-id":3498492,"id":"Q3498492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"948560fd111632d494d2a31c82da731c0c41a6bb","datavalue":{"value":{"amount":"+0.9281593561172484","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":"Q841684$14FC6CA4-6BED-4584-8421-AD9C89969F87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b1dfeb4f58629a3de8f2170811c634bc1408f23d","datavalue":{"value":{"entity-type":"item","numeric-id":1945905,"id":"Q1945905"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a3d489c27d33ed3e85da086dc493817a77945d96","datavalue":{"value":{"amount":"+0.8198281526565552","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":"Q841684$D4CA6095-0AD8-49E2-BCD9-1DA574411441","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"63c88c73eb0f33863fc007467a9962367e1e0911","datavalue":{"value":{"entity-type":"item","numeric-id":877826,"id":"Q877826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"70bf343b7dfeef8c75548065f38e3e83619f8110","datavalue":{"value":{"amount":"+0.8115426898002625","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":"Q841684$A219D031-2826-4754-BCFF-B800863F4285","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3b168262f9e1b4514313a24dfabf8223d2ad31a3","datavalue":{"value":{"entity-type":"item","numeric-id":556682,"id":"Q556682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6babc1841056f4484915ecf39eb056ee7884c059","datavalue":{"value":{"amount":"+0.7992802262306213","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":"Q841684$AD3E35D0-8CF8-4F1F-B92B-0D00445C4058","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c6b4440e24c330497025549da4d4dc8ba9f23acd","datavalue":{"value":{"entity-type":"item","numeric-id":5747877,"id":"Q5747877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4da0ea52c81f12d3daf33be18047e7f801a810a3","datavalue":{"value":{"amount":"+0.7856107354164124","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":"Q841684$2AA03666-A52A-4754-8EA1-2D34EE23DA4F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"ATP-based cross-verification of Mizar proofs: method, systems, and first experiments","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/ATP-based_cross-verification_of_Mizar_proofs:_method,_systems,_and_first_experiments"}}}}}