{"entities":{"Q7323673":{"pageid":31355236,"ns":120,"title":"Item:Q7323673","lastrevid":105121927,"modified":"2026-09-17T13:18:23Z","type":"item","id":"Q7323673","labels":{"en":{"language":"en","value":"Formalizing the hidden number problem in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8249900"}},"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":"Q7323673$CF2551DE-D6AA-4A68-B8A8-A820CB220D9F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d6e5255df48b46edba95731d547674989d2041a5","datavalue":{"value":{"text":"Formalizing the hidden number problem in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7323673$7C541709-F116-4156-8EBF-DF3A84AFBFC2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"fd010215ee28a96708c75f6bca394c370d494f2e","datavalue":{"value":"10.4230/LIPICS.ITP.2025.23","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7323673$6C918C38-A297-475E-ADD9-E35F26E8FAF2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"21adb23456a56f8537e42b02105a36da293434b8","datavalue":{"value":{"entity-type":"item","numeric-id":6648160,"id":"Q6648160"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$41E1987E-4FF2-49C7-B4C5-A5A7C38C7B30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"307ffe20ec102c34241404c06f1e86867b54f36f","datavalue":{"value":{"entity-type":"item","numeric-id":6528973,"id":"Q6528973"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$BA8DFB0C-61BB-4CDE-BF64-F456717EB610","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c55ade6aae783b1fedb4e24cb337389bf3e9f970","datavalue":{"value":{"entity-type":"item","numeric-id":6411591,"id":"Q6411591"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$25840DF2-E8FC-497F-9A05-1903B8F04F3B","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":"Q7323673$B48D7811-2E73-4EA5-8F7B-7A8E4DD12237","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7323673$2557AF22-C1A4-41D0-B1B3-088BFDE496B1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8825151670fec9a2ec828fa97aff5577698ed37d","datavalue":{"value":"8249900","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7323673$47418EB1-8FF1-4C6F-996A-23008D618C5D","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":"Q7323673$15B7E4C6-C057-480B-94EE-D36CF42C9830","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":"Q7323673$588E24E5-FA2B-4223-AD5C-B2735493D465","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"50cfad429314e1605f6ade5a2c59b3e9f12f443e","datavalue":{"value":{"entity-type":"item","numeric-id":1076512,"id":"Q1076512"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$854B3784-BBDC-4F6D-9AD7-6477DB6E0349","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":"Q7323673$1B0995BD-CE64-4546-8444-3DA2C362C5BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba5ad8860e2dfafdd492a4ade42b23f462631c32","datavalue":{"value":{"entity-type":"item","numeric-id":5261508,"id":"Q5261508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$BD1F47D0-159D-44D7-95A3-0C1373DFF444","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9e92a532cf8cd351ed27256cc105fcf6d9ff5757","datavalue":{"value":{"entity-type":"item","numeric-id":2175214,"id":"Q2175214"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$88CC1843-B009-440E-9EEF-BBB89B1BBB39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7792214e49541058bdb02c7b5f46ab347d571c3c","datavalue":{"value":{"entity-type":"item","numeric-id":6652984,"id":"Q6652984"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$8FD740BE-C2DE-4505-94B7-D6ECB987A0B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"979cd6c6c3104eb4a0fc9da9754e43cfb5d7c398","datavalue":{"value":{"entity-type":"item","numeric-id":4474164,"id":"Q4474164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$F67F14DA-63A1-4DAF-B4CF-1F1BFA0044B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"385f593619cd541661b7cc3f1a65f4b920b87952","datavalue":{"value":{"entity-type":"item","numeric-id":4783727,"id":"Q4783727"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$67132E86-8F9C-4FE1-8FF6-A5718242C578","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f6d8d8e3740b94961f581331bc04af39441f82d5","datavalue":{"value":{"entity-type":"item","numeric-id":3452347,"id":"Q3452347"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$5B2F8C16-0436-4BCF-B062-462B42CE9CB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fcc3fb885187142d9fb312c4d7b15a3e31071141","datavalue":{"value":{"entity-type":"item","numeric-id":5222951,"id":"Q5222951"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$DD24A6CF-805D-409E-AF3E-139B5E933603","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b4ac3c8544fab6593107bdd81f87660f21dbf223","datavalue":{"value":{"entity-type":"item","numeric-id":2656908,"id":"Q2656908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$1FD28758-114C-4E5B-AC04-4DEF0DB27A84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d20e66d02039a295e781f0d9e79324de75c42d5a","datavalue":{"value":{"entity-type":"item","numeric-id":2031427,"id":"Q2031427"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$B97B3896-F62D-4355-978A-144F59013A1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"feaafaf7d43422a130e4e1ad00fa0e8894e6f7fa","datavalue":{"value":{"entity-type":"item","numeric-id":6091132,"id":"Q6091132"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$8EE05C89-AA45-46FB-9DDB-67E2A0440750","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7da1b4cde3178812a1ec356bad8b537c65d88c93","datavalue":{"value":{"entity-type":"item","numeric-id":5429155,"id":"Q5429155"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$02C69D31-EEF4-4E4C-A071-A405750A80C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"50c065a04719fb9f4818199739037adbadd1e724","datavalue":{"value":{"entity-type":"item","numeric-id":6492756,"id":"Q6492756"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$3278111E-1A4B-4472-94BC-FA862E73EC8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"55ddf8dd24ac69c2c348f029ae3e306c89fc82fe","datavalue":{"value":{"entity-type":"item","numeric-id":3933739,"id":"Q3933739"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$56CB784E-D9FA-41C1-9F3F-44C49A486CF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7efd2748f4b43f93f6c9f8888e0c86fd46d6453f","datavalue":{"value":{"entity-type":"item","numeric-id":2902914,"id":"Q2902914"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$6308BD2B-496D-4154-83C0-D092456DE527","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a18a46233e0e3dee0556474a180f2ae08e6b396","datavalue":{"value":{"entity-type":"item","numeric-id":3179350,"id":"Q3179350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$D3B19395-530D-4E76-8D7C-DCAD40B6732B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b3b6844ad04f44a473a61fbf45f93d0b535b94f","datavalue":{"value":{"entity-type":"item","numeric-id":5048983,"id":"Q5048983"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$0B3EC4FE-4CC4-45FE-B91B-3B3327E3F55D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"124f3f8eb67b7956de903343ddb0b63ba81c9a85","datavalue":{"value":{"entity-type":"item","numeric-id":2708631,"id":"Q2708631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$917AEFA1-8D87-4456-83FA-445787F5DD2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5fb37ea16ffa88ec1a679371221359d83db2eb4b","datavalue":{"value":{"entity-type":"item","numeric-id":1849602,"id":"Q1849602"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$01B2917C-E829-4790-A22F-3D25177AAA86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2eb0b883763fe53983e5f77c7d7768c1c00bef25","datavalue":{"value":{"entity-type":"item","numeric-id":1412249,"id":"Q1412249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$BA133C78-A872-4215-8C7C-FCCA6338EBC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$52AB27D7-BB23-47E2-9314-ADA59021D2AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d2ec562f2b28ca462eb534502720c0caa529145c","datavalue":{"value":{"entity-type":"item","numeric-id":2209537,"id":"Q2209537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323673$D03FAE88-D694-4F52-9E66-12D536FDCF4A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formalizing the hidden number problem in Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formalizing_the_hidden_number_problem_in_Isabelle/HOL"}}}}}