{"entities":{"Q4945209":{"pageid":6974791,"ns":120,"title":"Item:Q4945209","lastrevid":47471371,"modified":"2026-01-01T20:18:19Z","type":"item","id":"Q4945209","labels":{},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1424019"}},"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":"Q4945209$0AE41022-8EB1-41F5-97D7-25D497FE7CA4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b814df31bedb109c4ccbd98d45e7194e579f07b3","datavalue":{"value":"0954.68093","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4945209$C1B46105-EDF9-4487-A1FC-A915B3BCE61B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"09dd3c96e1e6b9d594d4b38ca2de4ecc7417fe21","datavalue":{"value":{"entity-type":"item","numeric-id":671984,"id":"Q671984"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4945209$D49FA118-70E7-413C-971A-4C717D9175E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0a40fb8ae99741e91d6a63c85400bf5c0ece51d8","datavalue":{"value":{"entity-type":"item","numeric-id":265796,"id":"Q265796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4945209$E5B59314-8766-4974-80D8-A0A57E98FF91","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"35fafbbe8209085733f3754bac7d6ba0f1c137cb","datavalue":{"value":{"time":"+2000-03-23T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4945209$318982D1-0F71-4437-A21C-0FFEE986043E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4945209$5E1E94F4-958C-4A93-8275-ADEFB5ED7B25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4945209$BF4A5338-609F-4CF6-9C72-12C80FAAF749","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"de7f8ec97ee22d323fc6bedcd2b330fc99bf46fc","datavalue":{"value":"1424019","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4945209$D6A1D333-615F-4976-BD34-4EA4E697E970","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"657b1dc58dc8383e3970395d34173e20fb990340","datavalue":{"value":"programming language","type":"string"},"datatype":"string"},"type":"statement","id":"Q4945209$09F8B8AC-8D94-46FF-8075-9E71540D432A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"08f2d1affd1646c6bc1bcf16d4ec25e026f7b737","datavalue":{"value":"theorem proves Isabelle98","type":"string"},"datatype":"string"},"type":"statement","id":"Q4945209$BEA0BB86-1A16-47F4-AF8F-E5670A2901E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f3e04a2b734a1cac93a9ddfefc5a4de51edbfaf1","datavalue":{"value":"bisimulation","type":"string"},"datatype":"string"},"type":"statement","id":"Q4945209$3D193B8D-E910-4102-B9E3-8CF757C0D1BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1b6692564b9126396903952c44aa98b86a268b23","datavalue":{"value":"contextual equivalence","type":"string"},"datatype":"string"},"type":"statement","id":"Q4945209$E9B81595-6BAC-424B-BB96-ABF87224806E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b1203243fb6d1e0ba6a8d0eb5c56d76a1539719","datavalue":{"value":"automated proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q4945209$A1CB0EAE-4D81-49E7-8C79-DE3A65D2AC92","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":"Q4945209$577ADB19-05DA-483D-91D3-F33764AD2F33","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6328892829268e13d65cdead5f98e742e6847e06","datavalue":{"value":{"entity-type":"item","numeric-id":1272764,"id":"Q1272764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"865c5f3b0621abe1f5198f5ecdca023023bb6d13","datavalue":{"value":{"amount":"+0.7534391283988953","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4945209$A36C0907-E85D-495A-8C31-C0BA58724ACF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"38aa120b25c6a2afd536e54ca4c3bec74fcc152a","datavalue":{"value":{"entity-type":"item","numeric-id":5236557,"id":"Q5236557"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"91a3d3b0e655dca9a653568a853abbc6c7d27204","datavalue":{"value":{"amount":"+0.7376963496208191","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4945209$224AE5B0-30C0-4D69-A0B6-71A973FA65E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9a2566155239714c00e61ec0ef8651340a4fc288","datavalue":{"value":{"entity-type":"item","numeric-id":3400636,"id":"Q3400636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"084f9b19e92c6e348aab96bbf66b0d73dbc4c54d","datavalue":{"value":{"amount":"+0.7370607256889343","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4945209$6CBB97C5-181D-456B-ADE0-5E788147784C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9b29c499323d35dfcc5c765968119e36c36f5c9d","datavalue":{"value":{"entity-type":"item","numeric-id":5096388,"id":"Q5096388"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fc8574efd80fe0e4cbbd25c3ba2287d2cb7a851d","datavalue":{"value":{"amount":"+0.7368842363357544","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4945209$76073BE4-ACA6-4864-903A-FA3F31874DA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3dc1c862398ae999c50fa68994dcfd97c8f0ceaa","datavalue":{"value":{"entity-type":"item","numeric-id":3336725,"id":"Q3336725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6f3bb841bd7f6c02e814cadcc2f67f7d1991689d","datavalue":{"value":{"amount":"+0.7305525541305542","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4945209$AEF6B7FC-724B-4532-890C-75041F6D6665","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4945209","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4945209"}}}}}