{"entities":{"Q6860008":{"pageid":20656681,"ns":120,"title":"Item:Q6860008","lastrevid":84252230,"modified":"2026-05-14T05:36:37Z","type":"item","id":"Q6860008","labels":{"en":{"language":"en","value":"Distributed parallel build for the Isabelle archive of formal proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8158263"}},"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":"Q6860008$474C1085-13DD-43DF-BBC8-89E230DF8C97","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c627bd5b5af71e75f88b53f3acfdff9524e98fad","datavalue":{"value":{"text":"Distributed parallel build for the Isabelle archive of formal proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6860008$62A722CE-DD36-4E82-AB8D-80F3E3AB6FB2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"509a3883dd03c855e1c9f76efc2cc5784f70a422","datavalue":{"value":"10.4230/LIPICS.ITP.2024.22","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6860008$C9D69C9D-7B7F-4A52-9596-7793A4721FE3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8f64101566eab5cea5671c31f8e640732e15e1e5","datavalue":{"value":{"entity-type":"item","numeric-id":6118823,"id":"Q6118823"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860008$D39D5AC2-F81D-44A1-A286-05718350F3B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a162d67ca0f0da05fadb758011f7efa5d1e07db6","datavalue":{"value":{"entity-type":"item","numeric-id":287364,"id":"Q287364"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860008$B1BE690B-D23A-48D4-AD77-7ED27C46214D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4f115c6be43614d2596ce7cf4daadf566de48c39","datavalue":{"value":{"time":"+2026-02-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6860008$582158D7-B4E3-4797-9819-5A7882374EEA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6860008$7817F23E-E167-4B42-AAB6-EF6BB58A8BC9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d911639f5b17a00923934a514e62a1e35cc8021b","datavalue":{"value":"8158263","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6860008$7C623340-4514-493E-BAA8-E6031D25C10C","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":"Q6860008$B30226FD-1924-4730-88A4-92BDD954A342","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q6860008$A713FC52-1E30-4931-99CF-1CAA7D2E858E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7eefb2b1f5e1ddd95f5db204b23cfb4c53d0151","datavalue":{"value":"Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q6860008$2FBA7FA4-9731-48EA-A15F-610254AFDF6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3ff6db9d16a0ec84f38f8d643901e77bf8b73f45","datavalue":{"value":"archive of formal proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q6860008$BE7E4176-3E5B-4597-8202-53FB55FB5978","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b0acf809eea228676d6226d539808a9d0e7c51ac","datavalue":{"value":"theorem prover technology","type":"string"},"datatype":"string"},"type":"statement","id":"Q6860008$D20F4EEB-3D1F-4619-9779-FD7C6FA00B88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0b36d924addd0d2f364b26835d91730b673a9f92","datavalue":{"value":"distributed computing","type":"string"},"datatype":"string"},"type":"statement","id":"Q6860008$F3A5CFF8-A053-445A-B865-EB527C62F0E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"008927bb0297e12b30bc22981f475e554ea8b819","datavalue":{"value":"schedule optimization","type":"string"},"datatype":"string"},"type":"statement","id":"Q6860008$811ED0BF-65AB-4734-9F91-7A0C300EEC8E","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":"Q6860008$FEA42AB2-044B-413C-908A-AAD6C99FE952","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac15a4f126cc42b8a7da009581770d9b1cc61f1e","datavalue":{"value":{"entity-type":"item","numeric-id":835549,"id":"Q835549"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860008$3C5499DD-CADA-409D-822A-2DC6E4E0EA62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d358765945f3da138196b181ed4e6aafa5975fcd","datavalue":{"value":{"entity-type":"item","numeric-id":2945623,"id":"Q2945623"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860008$346E435F-4749-4211-AB35-21CFCE35A771","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"63d7deaf3e7bac9de0ff67356dbe46db811c5ca2","datavalue":{"value":{"entity-type":"item","numeric-id":1052820,"id":"Q1052820"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860008$D659460C-A0AE-440E-A283-744ADB930F70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8242928870aab67343ad0152eb7ca8357168f7f3","datavalue":{"value":{"entity-type":"item","numeric-id":3454108,"id":"Q3454108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860008$A637C7A8-0C42-4937-A2AC-C33BE0F25CC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aca7961f7051c4fdb1f73d6f9a35cc8c2545025d","datavalue":{"value":{"entity-type":"item","numeric-id":744638,"id":"Q744638"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860008$837E77BB-2402-40FA-86BB-B103DFF96436","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"be8a53fe134b0b70830e68dfe27608ac9174a22f","datavalue":{"value":{"entity-type":"item","numeric-id":4140712,"id":"Q4140712"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860008$A3EE9623-6ABC-4649-9E31-0BA7703CD752","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ff4c45303891235094588126dfde91b2b243515","datavalue":{"value":{"entity-type":"item","numeric-id":1752254,"id":"Q1752254"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860008$A384EAF1-1E6F-4F7E-B6AE-CEC9D7F06563","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"012cfe0b9868a734444fcc53395a019c1a146abe","datavalue":{"value":{"entity-type":"item","numeric-id":5948197,"id":"Q5948197"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860008$A343C82C-4C54-4D5A-9B91-2FA4EFE01051","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e0a521a247c004a14f53f38577ade217c87172ce","datavalue":{"value":{"entity-type":"item","numeric-id":6159378,"id":"Q6159378"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860008$6E937C23-C351-4917-8AA0-D68A831EBADA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0af0233b784a007f73cb48db94b3e7fd8f23f607","datavalue":{"value":{"entity-type":"item","numeric-id":2273894,"id":"Q2273894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860008$86F1AA29-7096-4CEB-8136-8CE28CCFDE72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"468fc18a09792dd4a050520bb89e23d01ec79224","datavalue":{"value":{"entity-type":"item","numeric-id":6643010,"id":"Q6643010"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860008$9CCFB8B8-4C1E-4BD3-96CE-7D58B873465A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66241651fffb49f9d5afc46e970eb5794adb2e24","datavalue":{"value":{"entity-type":"item","numeric-id":5327360,"id":"Q5327360"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860008$45FAB7A8-721C-425D-9057-71A8DAA16A10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"de630d14fe895ae5d892978d97f92afb82231aa0","datavalue":{"value":{"entity-type":"item","numeric-id":2879273,"id":"Q2879273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860008$10490249-CF54-413F-A59F-E4657F517DFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47407ce605e4f41d43c5a7bb242b9e72252745ab","datavalue":{"value":{"entity-type":"item","numeric-id":2892296,"id":"Q2892296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860008$5131A719-ABEF-4D75-811A-4A9A6D9D8624","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Distributed parallel build for the Isabelle archive of formal proofs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Distributed_parallel_build_for_the_Isabelle_archive_of_formal_proofs"}}}}}