{"entities":{"Q4817211":{"pageid":6846791,"ns":120,"title":"Item:Q4817211","lastrevid":40916139,"modified":"2025-04-14T03:06:00Z","type":"item","id":"Q4817211","labels":{},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2101985"}},"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":"Q4817211$8FD8C609-35DF-41EC-B0CF-7B9A28916129","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4e8d5186314412ccc74d65ffcaa4326fa3f30063","datavalue":{"value":"1066.68120","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4817211$43996AA4-D8DE-49D5-AC82-FBD063B98470","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e6bbab2ea230ef82cf7d72bee404dd827d5aaeed","datavalue":{"value":{"entity-type":"item","numeric-id":230814,"id":"Q230814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4817211$6DF0DC97-E240-470E-8FF3-E4D9CA338929","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b0d384413a2d1b8185eb46b74e5b2c74244e0aac","datavalue":{"value":{"entity-type":"item","numeric-id":928667,"id":"Q928667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4817211$B6DA771C-6C71-4DB2-9167-ECAD91EBE2DB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c7bd962bada8b0dc37e98aacdd29c36343a02c75","datavalue":{"value":{"time":"+2004-09-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4817211$D9A7CBDA-B3D5-4623-BD9D-83B9B134D484","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4817211$3A8D509A-5EA5-421E-AF73-F2F4FFD52651","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4817211$4912D0E0-E2B2-4A23-ACC6-90BF6572AB4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4817211$A6189553-F1FE-4B02-A20F-3588C9B526CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4817211$D1C19CEE-5438-4C09-9296-D78F0873843A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4817211$E0C7959D-01D6-49FA-9416-859F11D42F83","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"10d450fd2d3ca5088e56b8654b6700e5725f1092","datavalue":{"value":"2101985","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4817211$AB17C332-3CDA-4AF1-84BE-CB1D297CCE1E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"471c8f8daa284748af55be6cf731cf1f6d77f730","datavalue":{"value":"mechanical theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q4817211$AACBA57F-E073-4D27-AF51-BF06EF9F0D7A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e29a0a1a089c1739ef594b8aa170de0991ebf7f7","datavalue":{"value":"proof checker","type":"string"},"datatype":"string"},"type":"statement","id":"Q4817211$AB4AE283-FF2F-474B-A0DE-97D227032F18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"657b1dc58dc8383e3970395d34173e20fb990340","datavalue":{"value":"programming language","type":"string"},"datatype":"string"},"type":"statement","id":"Q4817211$143B045C-A684-4019-89D7-5A3E9D055D4E","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c652637493e8de65377ba80065ca4183c6dc627","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4817211$BF8B6B44-6CA3-4487-80D7-DD7282BF32E5","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":"Q4817211$5BE5611A-48FB-4B05-A0B1-6FD24DDE9F0E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ed33447b2191b3f838a06f84d94e7ac1e3acc282","datavalue":{"value":{"entity-type":"item","numeric-id":4730755,"id":"Q4730755"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"31e2a727677d9622dbd68985fdaa55b48ce6e3d1","datavalue":{"value":{"amount":"+0.9058655","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4817211$95FA9450-52B9-493E-9726-25FB2850F618","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6b97095a387083d4829b242d2a1a3f0b04cdcbd7","datavalue":{"value":{"entity-type":"item","numeric-id":3608645,"id":"Q3608645"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7e61637cbc91a8deff6e86fdd3c00bec5559f322","datavalue":{"value":{"amount":"+0.8963756","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4817211$F2C8CDAF-E349-4B7B-BBFC-5D74CB9B4D7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"00aca7c03c64ed75a1eaf16ca34e9b3b51497b5d","datavalue":{"value":{"entity-type":"item","numeric-id":1314414,"id":"Q1314414"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1b446f641433aaee6e15d8d8a78f741fa5a97e45","datavalue":{"value":{"amount":"+0.89572716","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4817211$F7D83178-710C-4D33-942F-F928F0A024B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4149079e333e9d5d431375275d4ce081e133b30b","datavalue":{"value":{"entity-type":"item","numeric-id":3019505,"id":"Q3019505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2f6c7f0583e308aace66b94447c88e7dcdea0db2","datavalue":{"value":{"amount":"+0.889294","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4817211$5B6AD582-37B2-4647-9432-8B61DD6B8D4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1dfc411987926c5d3e1ef10393b467bc8ebb8b57","datavalue":{"value":{"entity-type":"item","numeric-id":4275257,"id":"Q4275257"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8138f2d0ab25141cc6d242edaae0f3fd7848744a","datavalue":{"value":{"amount":"+0.88589036","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4817211$092CB1CD-4730-47CB-927D-EE4F67490189","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12d93bedac32f49ef29840872a51a1b74b8fc181","datavalue":{"value":{"entity-type":"item","numeric-id":5961490,"id":"Q5961490"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ea482e37aefc946a1b6601c0ca1bbe1a30908915","datavalue":{"value":{"amount":"+0.8853125","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4817211$5FB74B7B-A4A9-44F3-A04D-8A7F3CC87705","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f2e5ac7661f403ccd09bf507d877adbfbe4ab89d","datavalue":{"value":{"entity-type":"item","numeric-id":4215638,"id":"Q4215638"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ef2ab64e65c7510b68e3a5097dc9e03081a87aef","datavalue":{"value":{"amount":"+0.8852192","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4817211$BD11E2B4-2623-48DE-BAEA-3608DBD379A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"776bb2625ed30546b576f2d9fd7e9b57ea3425f7","datavalue":{"value":{"entity-type":"item","numeric-id":3570163,"id":"Q3570163"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1e927dd364de27bbcb05e57ae79410ddc46b558b","datavalue":{"value":{"amount":"+0.8849195","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4817211$3A1CC444-6378-4CDF-BB6C-1AB32589C9CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ab4749f335d0af7e37202df27bd35f2484492f84","datavalue":{"value":{"entity-type":"item","numeric-id":1627457,"id":"Q1627457"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"98e2f56b4a658f7574d45a56e9b4b7d23aa5ce7e","datavalue":{"value":{"amount":"+0.8848882","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4817211$701E74ED-7AFC-43E3-95BF-157CF99156CE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4817211","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4817211"}}}}}