{"entities":{"Q5875427":{"pageid":7904978,"ns":120,"title":"Item:Q5875427","lastrevid":40873681,"modified":"2025-04-12T05:19:31Z","type":"item","id":"Q5875427","labels":{},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7649968"}},"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":"Q5875427$43920B69-998C-424B-AE7F-91C65513D5F9","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"70fcffa0591fe57559947b402bc1be17765c0d39","datavalue":{"value":{"entity-type":"item","numeric-id":2055890,"id":"Q2055890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$56337376-ACFE-4CF3-A79F-6588B598E24E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8dc9f7061148c184d156fce1cd302b98949f36de","datavalue":{"value":{"entity-type":"item","numeric-id":1687767,"id":"Q1687767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$D7EDD1D5-6ED4-4CEA-A0DB-7F3DB1B28501","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6695abe38664d65c38747de7b5fe54d9caa92dea","datavalue":{"value":{"time":"+2023-02-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5875427$49C5CE95-BDB5-47CE-90CF-788FCBF9E827","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e0c5eb4efafbbd3a9eed39b5ca00a3c80c048bcb","datavalue":{"value":"https://arxiv.org/abs/1904.10570","type":"string"},"datatype":"url"},"type":"statement","id":"Q5875427$F140697B-F836-46BB-B565-1DB907F45888","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875427$F0A855A7-9953-40A4-8A79-26A4F232EE1A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4da3f5eab1ebaa5dc6b283117e882a7f4a10bd8b","datavalue":{"value":"7649968","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875427$2231005D-6F23-4E53-88B2-B619A8F5644E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875427$AE644CBF-77F3-4ABB-9DCC-773A9D47D53F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875427$F9E88FE7-AAE6-465A-B6CF-1AD846A717F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b36a4092864d39bf9c99c5936b3d1261e44b9950","datavalue":{"value":"set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875427$7D438CAD-C489-40E5-A5CB-06246B15D965","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1b23248042bd506455f51600d00d7ec5443276f9","datavalue":{"value":"forcing","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875427$C1675957-E55E-4EAA-97D9-1D2BCE84195F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3411aa82b9afc3f210d9df9123146516fcbcd5d","datavalue":{"value":"independence proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875427$7805AF9D-72C3-47FC-A7A6-78FC12A797CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eacb0e4aab3d35beecc1ca5d565cdce29d072a94","datavalue":{"value":"continuum hypothesis","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875427$3EFE065C-6015-4327-910F-AEC952468EBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0432d965a31cea7acbf98425becf9815c9633902","datavalue":{"value":"Boolean-valued models","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875427$3B47DC0E-FEDC-4E76-B1B4-8BF69FF516B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4e8fd89fa28c0f6c3672ef10c3a2104586281edb","datavalue":{"value":"Lean","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875427$D5C88454-A951-48AB-8C01-B92D7840C486","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"67e43cd194146fff0fb8e4b0aacca2f4f32e42e3","datavalue":{"value":{"entity-type":"item","numeric-id":3937387,"id":"Q3937387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$3ACF8749-8BC4-4ABD-AE6C-BBDE10349B20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9779d2f20504dba38f482f942c0abc04f8e04e14","datavalue":{"value":{"entity-type":"item","numeric-id":3310616,"id":"Q3310616"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$E1D2CFB8-2FF1-4AB1-8AB9-3A43F7786332","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e21df1d3055daa4725f01a29fad1e4853704fa4c","datavalue":{"value":{"entity-type":"item","numeric-id":3762311,"id":"Q3762311"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$F1E467C1-00EC-4D08-8B97-FC722EA3662D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84315b2f7f1f1d42ab25304495cafc5e9fdd3aa9","datavalue":{"value":{"entity-type":"item","numeric-id":5145343,"id":"Q5145343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$F01409EE-DE32-4ED2-AF27-3FBA78BEA371","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"109becd8b3cb89cb43b3124cce54827498319001","datavalue":{"value":{"entity-type":"item","numeric-id":3007387,"id":"Q3007387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$358A0D8B-49C5-4DB0-BDB3-D45061E3A22A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c97535c16ff9110182a78f8ecf62c340fe59baa5","datavalue":{"value":{"entity-type":"item","numeric-id":5586268,"id":"Q5586268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$FBF2918C-2C63-46DE-9540-E8D19A256AEB","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":"Q5875427$427C4E2B-C938-4F7F-8AAE-77C26E9BB46A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fcc960d5578d50a62f3f4284fc62698db86743a2","datavalue":{"value":{"entity-type":"item","numeric-id":3533040,"id":"Q3533040"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$AAC617CA-0DFA-42E2-9E33-FA6D179B3B42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ddd70fb9307baa76a2064c43fce88ffa925876a","datavalue":{"value":{"entity-type":"item","numeric-id":5772630,"id":"Q5772630"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$6E282BB9-178D-4ECE-A85A-0A7B99ACF7F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5bf133f24682eadb30cba47d623064046c8dc5c","datavalue":{"value":{"entity-type":"item","numeric-id":2333671,"id":"Q2333671"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$544FB5F4-C4B3-4DE4-B595-3CC068EB22D6","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":"Q5875427$D25AC1FF-912C-4A0C-BCA0-DD019AE733BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03cb8e50e6c3bd60a9a9a59407cf30e8e788baa4","datavalue":{"value":{"entity-type":"item","numeric-id":3618853,"id":"Q3618853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$3E814FD8-12F1-43BA-BB23-06EDCEF682D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22bb2c241ea80bd256983bab3954ba576c4cc464","datavalue":{"value":{"entity-type":"item","numeric-id":450950,"id":"Q450950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$D138A7F9-442F-4AD2-8B04-A12A1DB31DDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"04cc1322638944d58c97f2602d06ebe61743d649","datavalue":{"value":{"entity-type":"item","numeric-id":4354789,"id":"Q4354789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$5412ACBA-4B1A-472F-AE37-F164E3131F2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9852e967ea1a713efc5d953d014184728fa02709","datavalue":{"value":{"entity-type":"item","numeric-id":4879892,"id":"Q4879892"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$F75D08D3-7FBE-41D2-B0A7-DDF08AD25D12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aa8fc741ea84c2e9afb209308c6a6f325d4380c2","datavalue":{"value":{"entity-type":"item","numeric-id":3535899,"id":"Q3535899"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$80BE65E4-B334-4666-ABE7-57417F76558E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65c8c8ed706a86d97db05d5b778c49fb79be8a30","datavalue":{"value":{"entity-type":"item","numeric-id":1144013,"id":"Q1144013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$1C500123-F396-4CC2-977E-EAEEB61765CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d95188dc39a301d822ddc19f4ee4aa7e56f88e0","datavalue":{"value":{"entity-type":"item","numeric-id":5242567,"id":"Q5242567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$76EF511B-3BBD-45E3-B565-E636AEA56829","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0136d3bc330af377385e6266bfd9e4c2d4c7a96c","datavalue":{"value":{"entity-type":"item","numeric-id":1319386,"id":"Q1319386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$49C3C6DC-C436-4F7A-9525-302FD0D00DC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b09f99d6db815f76ae0a8a4fcddc01dc77134f0f","datavalue":{"value":{"entity-type":"item","numeric-id":4809073,"id":"Q4809073"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$9024D0AD-3864-4494-BB72-315FBA7000A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b249a160e40d69f49ce000ae540a153fb317d0f4","datavalue":{"value":{"entity-type":"item","numeric-id":3507465,"id":"Q3507465"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$C6BE99D2-0DE0-48C2-A065-590EBC84923C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df566ef0248fe3e927a10046fdd99e599cbaa541","datavalue":{"value":{"entity-type":"item","numeric-id":5961491,"id":"Q5961491"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$79CC3352-5E4B-4717-B418-68522A081E9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58b883d872eefbd5f8daf82a38b9e66e81e1a15c","datavalue":{"value":{"entity-type":"item","numeric-id":5477663,"id":"Q5477663"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$32E3837C-2FB8-4714-93D0-8011B74DADB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"38602d2b7fd482d2c85a2b53c450a23a2740fb43","datavalue":{"value":{"entity-type":"item","numeric-id":1663242,"id":"Q1663242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$8A8725E4-7D95-4BCD-820A-46C09E5C99AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"481030b7d1e9cac5ae56ed6eb3a25fd1f256c35c","datavalue":{"value":{"entity-type":"item","numeric-id":5528665,"id":"Q5528665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$28472C98-625E-44DD-9A9E-C2E9BF0D6D3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88a2ef7f4e692b490d2e358eca8aa0fcb6f45cc4","datavalue":{"value":{"entity-type":"item","numeric-id":3509173,"id":"Q3509173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$2EA74895-C394-44ED-9CA9-290C19C68931","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bdf15e05266dafab4e09b0bac1834151f0fe8e26","datavalue":{"value":{"entity-type":"item","numeric-id":2250553,"id":"Q2250553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$49687CE7-EB4B-4275-9A4A-C8433BCD7637","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5f1a85252a4c0a5bb2b7a3eae3c76b6088496bd","datavalue":{"value":{"entity-type":"item","numeric-id":4296962,"id":"Q4296962"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$07FF4876-531C-4230-AEB6-3533214E1CCB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2bf66dce643416452adfb65f87a80d3a4ef76081","datavalue":{"value":{"entity-type":"item","numeric-id":5656765,"id":"Q5656765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$9F955219-431A-40CF-9357-574B3D94B9F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"497b4c81f4eb1172c293c9383a73640c83e593d4","datavalue":{"value":{"entity-type":"item","numeric-id":4364399,"id":"Q4364399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$41F6B509-4840-486E-AD46-E3A0145F5B81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9abf91574795850ec57bee78471a40720894abe8","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$0720315F-AA71-4B7C-9847-A18BF6AB780B","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"39d1d25ae8c00cfad058b188db36fd61dac09925","datavalue":{"value":{"entity-type":"item","numeric-id":27041,"id":"Q27041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$7FBAC999-0F05-4BA7-A87F-1612DDF6B03B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"aca41f313ec935c6c7a90dad170b49859b6fac14","datavalue":{"value":{"entity-type":"item","numeric-id":17120,"id":"Q17120"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$63E9D77E-303E-4F78-9A0C-F156F61371F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e338912f65cbd77347bbd512933e55736ef58bd1","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$5416CCFE-A12E-4E19-A859-EFFF4E4E58DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8bf42d0fd66acf369e3d5d44d7ebef6adc7ae452","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875427$9A91A513-0AB9-4247-AF4F-E4B75534E17C","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":"Q5875427$A022E814-647C-4206-BA18-CB248F6711A9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"bd8b31b3029748af5ff4e6f8a2e44ffe97ec148f","datavalue":{"value":"10.4230/LIPICS.ITP.2019.19","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875427$3957FA9B-0DDE-4C1C-B9CB-EA7C5FEC91EC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5875427","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5875427"}}}}}