{"entities":{"Q5045392":{"pageid":7074969,"ns":120,"title":"Item:Q5045392","lastrevid":54435326,"modified":"2026-01-26T19:49:25Z","type":"item","id":"Q5045392","labels":{"en":{"language":"en","value":"Formal analysis of information flow in HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7612575"}},"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":"Q5045392$4FE0A818-B4A8-45DD-8B74-8360C76F59DB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d18775b81dd91f8201e2744a7afb2ca93616fa2a","datavalue":{"value":{"text":"Formal Analysis of Information Flow in HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5045392$96658F7E-768C-43AC-A9ED-FBC8C6BA5098","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7502223dbcda48e6b8669e26e05e45f38f200253","datavalue":{"value":"1498.68053","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5045392$BE1458F0-E017-4A78-A8BA-D9173538E58F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7d53c5ff0b42bb8c731f8a73bb7a84aedd8d4c97","datavalue":{"value":"10.1007/978-3-319-69483-2_17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5045392$3F8E1917-0F7D-4F6D-9EC0-6FCB7B80B267","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8c685886fb9aa9eb6469bf24dace0c21d3e9ef30","datavalue":{"value":{"entity-type":"item","numeric-id":5045390,"id":"Q5045390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5045392$44D632AF-9DC7-40C0-8E5F-4E800DDC79F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f0d2c11253a443ddc53e205509995096ef6b865e","datavalue":{"value":{"entity-type":"item","numeric-id":246141,"id":"Q246141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5045392$1D65DDB4-4BD5-4B97-BFBF-0E35A6169BA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"393ef07e7673f4510d0e5689d2d44001b3ecc236","datavalue":{"value":{"entity-type":"item","numeric-id":246140,"id":"Q246140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5045392$07CE3A23-8D18-4B2D-98CB-0926D9D17819","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"76e6a2b8be73515f37c4af408f041128a90c7b7b","datavalue":{"value":{"entity-type":"item","numeric-id":5045391,"id":"Q5045391"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5045392$206EE2CA-99C5-499A-B701-42D0A14EBB13","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"02602812e8c677f46c4ba4febbc893f4aab8f2ae","datavalue":{"value":{"entity-type":"item","numeric-id":5045375,"id":"Q5045375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5045392$E64A3DFF-F518-4A47-8555-D1D0FF95B46C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"96420cb12347695a963e770401ec584dde3a55d6","datavalue":{"value":{"time":"+2022-11-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5045392$4C0342BD-087A-4541-8F90-127255824C8F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"2335101d556243c88261e1fccd8d7026b2856a8a","datavalue":{"value":"68M25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5045392$A394850F-C684-44E3-8887-90CAD3CC28F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5045392$F7F256C0-A585-47A0-926B-F49F7CA15C98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5045392$DEB9A9A3-4F4D-43C5-A316-688B3E1E1BAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e30d62051793251cdb7305d492b252b2239dfb5e","datavalue":{"value":"94A17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5045392$CF08C89A-010F-4088-92B5-432E7AAEF6F5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4d37d69dd6a7e624fe1c5b9f4c7b416cfe78dcec","datavalue":{"value":"7612575","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5045392$510B6B95-36EE-48F8-A6A8-5D4F7E6CA701","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6f443739aaf47befb8de516f78c7b4d8d4b14ff9","datavalue":{"value":"information flow","type":"string"},"datatype":"string"},"type":"statement","id":"Q5045392$1D49A543-D4E1-475F-B41F-6A3690F3087C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1c2e069b1a2184cd3b0f52ffa83b5fcb89125e86","datavalue":{"value":"entropy","type":"string"},"datatype":"string"},"type":"statement","id":"Q5045392$56E13E91-85C5-4A00-9D29-F401052DB1EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a17090ce3b7981fe24fb9ab79db374110cd9ba2d","datavalue":{"value":"gain function","type":"string"},"datatype":"string"},"type":"statement","id":"Q5045392$78B655B6-4A29-4019-95F0-57822F65913F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"23c501a6ac63504c189ce0481a325f0bef179dc2","datavalue":{"value":"g-leakage","type":"string"},"datatype":"string"},"type":"statement","id":"Q5045392$9B57530A-5A27-47D7-9B7F-7D9B571C9CBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5045392$CACCA85D-C9E1-4FEA-B59C-C5D025DFCA71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5045392$2A07AD55-E2A9-4A1F-BF49-53CAADB6A778","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":"Q5045392$9B6C4279-20C3-4B45-88AE-6FB66811EFD4","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4f291f3ef76ae95240ee92db9724d018643bd24f","datavalue":{"value":"https://doi.org/10.1007/978-3-319-69483-2_17","type":"string"},"datatype":"url"},"type":"statement","id":"Q5045392$8B95BFD5-7696-44A5-A462-AD49A512584E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"66b6dd8dcdfd745c209fee6efdbbb9d4a94605d7","datavalue":{"value":"W2766158006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5045392$5150303B-04FB-4876-BE8B-0363E4E041E5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a07ff81cd829b73f57957165205d53f775343772","datavalue":{"value":{"entity-type":"item","numeric-id":5166664,"id":"Q5166664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e4640a0f041d196bbca2c2b27b6fd32a1be83cb3","datavalue":{"value":{"amount":"+0.8979663252830505","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":"Q5045392$7FE5C206-260A-4CA1-89B6-2DCFE998E31B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a0f292f547aefc3e600785a7840114d7a8eb4b49","datavalue":{"value":{"entity-type":"item","numeric-id":3088009,"id":"Q3088009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"82c94080ebc0e5b6a0b6fb6582043586c38ce6b5","datavalue":{"value":{"amount":"+0.8309211730957031","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":"Q5045392$7F0715F4-C97E-412B-9F74-A315A013A425","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6190e40cdd6bb6dcf015918a528530f486ac7619","datavalue":{"value":{"entity-type":"item","numeric-id":2422017,"id":"Q2422017"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d59bc4d91f963066480e8da99c3fa2c765bba776","datavalue":{"value":{"amount":"+0.7489728331565857","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":"Q5045392$60ACC5D4-43B4-45AB-AAA0-E33D7B869C93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8b4dd0e27a348546e52d8383d801018c19ef300c","datavalue":{"value":{"entity-type":"item","numeric-id":3575030,"id":"Q3575030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"91416237af68334c649c0d10f856cd93f5d82bb1","datavalue":{"value":{"amount":"+0.7341657280921936","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":"Q5045392$BABE96F6-1E83-444F-8D44-1C4417393772","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3d04ee113d86fa1a9491a45b50f1faeb3985d600","datavalue":{"value":{"entity-type":"item","numeric-id":4902321,"id":"Q4902321"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2722e76d3acde33cf5b31af7ae41741cecc0485b","datavalue":{"value":{"amount":"+0.7315278649330139","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":"Q5045392$BA8CD5C8-3E0C-4F64-AFBE-EEE2A48F7C7E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5045392","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5045392"}}}}}