{"entities":{"Q7323672":{"pageid":31355230,"ns":120,"title":"Item:Q7323672","lastrevid":105121924,"modified":"2026-09-17T13:18:20Z","type":"item","id":"Q7323672","labels":{"en":{"language":"en","value":"Formalizing splitting in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8249899"}},"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":"Q7323672$51985981-D847-4642-A219-AE7C758CF7A9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"68a72654f1ac5602761f903f9c65bf9d86a6d68a","datavalue":{"value":{"text":"Formalizing splitting in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7323672$D9C8A3E9-A71D-4AA9-9AA8-A52FBE42DC46","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d15858982423f0406ca36de3e4e1f762bb351f4b","datavalue":{"value":"10.4230/LIPICS.ITP.2025.22","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7323672$6D751DA2-352C-46D0-8C19-9D301AEAD2C6","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"32043f1942b4d64b0fd16dd525fc3da0c0f84a0e","datavalue":{"value":{"entity-type":"item","numeric-id":7323671,"id":"Q7323671"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323672$499F869E-B620-4A0D-9D66-98D3FB76BB81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d43863aee12a51cd57725fb5bd62fec5b80c43f0","datavalue":{"value":{"entity-type":"item","numeric-id":7034871,"id":"Q7034871"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323672$202485FF-050E-4098-BBE3-0BC2FA93F71A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ca512d58059d63156835648800422b2988de4fc6","datavalue":{"value":{"entity-type":"item","numeric-id":2051562,"id":"Q2051562"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323672$71993B5B-6404-4104-8294-8C7F6D798BFE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"327bdfdabaae2e8cbc884e8efa23d5004f5f8802","datavalue":{"value":{"time":"+2026-09-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7323672$5DDCE16E-F90A-4A64-9751-1AF9A1AC1D2C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7323672$93DE90AA-A7B7-4F2B-9A5C-2FA266FA6B93","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"df18a505443fb7d98d1eff86ccd57dd144403ca0","datavalue":{"value":"8249899","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7323672$83C29A99-041F-4041-A907-430CF7B99D5A","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":"Q7323672$FCF4675C-B9DD-4622-A950-413249474146","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":"Q7323672$0624ECBF-F628-49C8-9D3D-95CC18C9AA8B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b1137cf78c4cad0e217f70ec321f2a593915490","datavalue":{"value":{"entity-type":"item","numeric-id":2751353,"id":"Q2751353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323672$33A86C87-D0CE-4B75-9B8A-45F23E587031","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4738798d9702e646d9743f53f948745583da971","datavalue":{"value":{"entity-type":"item","numeric-id":2352487,"id":"Q2352487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323672$7211F55D-A5CC-48D7-9959-109242A79DF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4342eaf993d8aed1454efafe9d939daad5b5ce67","datavalue":{"value":{"entity-type":"item","numeric-id":6860021,"id":"Q6860021"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323672$17C7D83E-D64A-492E-98AD-8F7654D50229","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df86a0ed10db66a7e1f365b05afe861b77934d95","datavalue":{"value":{"entity-type":"item","numeric-id":6103590,"id":"Q6103590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323672$DBFB1D82-D002-4AF1-B590-81B7D56D93BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e7f4e131abd397423f508ff6cb02fd16c492dec","datavalue":{"value":{"entity-type":"item","numeric-id":1037396,"id":"Q1037396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323672$F0160E23-A563-43F4-AE5F-BE6768650322","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"205fc50b5519f69b83835852ede0d50684c7d19b","datavalue":{"value":{"entity-type":"item","numeric-id":4247076,"id":"Q4247076"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323672$6A2EB6A2-3D2A-4492-896C-692FCF610E3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b659b1f6009ab3df1cf8432adfeb1aaf4fe4f69d","datavalue":{"value":{"entity-type":"item","numeric-id":6060676,"id":"Q6060676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323672$70382FCD-1C39-4A62-9CAC-B8D5D60BA269","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f14878b4342799995051ac9bc54cd21c98efc98","datavalue":{"value":{"entity-type":"item","numeric-id":2751359,"id":"Q2751359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323672$CC080609-EBDF-4F6B-96BF-D971581B2F50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"516924fffc5ccd06ddf357b776bed9baac4d2e69","datavalue":{"value":{"entity-type":"item","numeric-id":2324227,"id":"Q2324227"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323672$EA32AAE2-6CFC-4A14-8114-855E9CF7BB27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"443687e1644d765aff7a815618637b8d7305da63","datavalue":{"value":{"entity-type":"item","numeric-id":5919011,"id":"Q5919011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323672$A32E6235-6D0B-42D9-ABDF-435AF92942FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4aa6750f3149d248c4e232f6fdbdc36d7bc86e39","datavalue":{"value":{"entity-type":"item","numeric-id":2920991,"id":"Q2920991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323672$EE13E553-D9C9-4D23-B803-FFC22E53649F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"460b4ac3d5fcbf54c94d3ace4c894ddc3cc814e6","datavalue":{"value":{"entity-type":"item","numeric-id":5918575,"id":"Q5918575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323672$0D3C3D46-BBA4-4DDD-A3BE-29406379D47B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb8dea5b3d9f1a9e1ad9c6c58ae5add84db3e036","datavalue":{"value":{"entity-type":"item","numeric-id":5970776,"id":"Q5970776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323672$3465D61A-10F0-4E55-98F4-63AD6043DE12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6b597c365a014dac51aeaa5fe82706f0bdc23791","datavalue":{"value":{"entity-type":"item","numeric-id":5759817,"id":"Q5759817"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323672$0E4D7D97-5A3C-4896-B87B-334E6D494CA1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formalizing splitting in Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formalizing_splitting_in_Isabelle/HOL"}}}}}