{"entities":{"Q541222":{"pageid":542989,"ns":120,"title":"Item:Q541222","lastrevid":62613216,"modified":"2026-04-11T07:16:28Z","type":"item","id":"Q541222","labels":{"en":{"language":"en","value":"A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5904444"}},"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":"Q541222$6F4C249F-3DC5-4F6D-8578-AFB718C693C5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"be4405a13efea00cb6de1c60b8f4191c16982294","datavalue":{"value":{"text":"A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q541222$6BD15C56-06B5-46A7-B6B5-857950D0E638","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c439bfa9eef5a6ce9e3ea1f5a347ac6602a43471","datavalue":{"value":"1244.68053","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q541222$46C08366-34B5-46E6-ABC5-2F33D114AE11","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4d7c4100404442680e9faf3f2ae6e537b0cd1cc1","datavalue":{"value":{"entity-type":"item","numeric-id":319638,"id":"Q319638"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541222$02092D9F-0876-4C8B-A6FC-A28B70B0176F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1caedec2f74947a2d17e2400cfb77f2b4f640d20","datavalue":{"value":{"entity-type":"item","numeric-id":364475,"id":"Q364475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541222$B9979550-4EF2-4344-AA02-5AB5179597E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"07abc0868bbf3c0352f8089c12b27e770f5814c5","datavalue":{"value":{"entity-type":"item","numeric-id":364476,"id":"Q364476"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541222$B594DB01-38E7-41CC-A298-B3357393A9CF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541222$CCE9767E-89E0-4330-B17D-361E83DE62AC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c1d636dc02e31c50ff8e96e46630d760ff43fba8","datavalue":{"value":{"time":"+2011-06-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q541222$D59CEA46-9F67-4EDC-842F-A9A509056F27","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q541222$73EB28F0-5703-462F-B743-5B7A3BD6B831","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q541222$D1EC0CE1-F445-4565-8F5A-8380E5DF9093","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q541222$06D1EB49-F57D-478E-9840-A89977ACF500","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"560d56ad4ee3f60cf75f664894574d850c09b0c1","datavalue":{"value":"5904444","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q541222$8E1FB5B2-F7E9-44BB-9B10-921E0313F3D4","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4fe6a4db7f6d4f320025a2c13e14a4633c9dceaf","datavalue":{"value":"symbolic trajectory evaluation","type":"string"},"datatype":"string"},"type":"statement","id":"Q541222$20AFD4D7-D4EE-4495-A73C-B2E8FF3A26D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3052772e01900d9220f495e188abd512814fb5c6","datavalue":{"value":"netlist","type":"string"},"datatype":"string"},"type":"statement","id":"Q541222$86ECC031-D8F8-4F69-A0DB-D9C483B49A0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8b4804225ce369eb1d5773935b377190245c3fb8","datavalue":{"value":"formal semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q541222$4ADC7568-FA7A-44FE-96D9-FB63B90FF3E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q541222$1FF5DC4B-DE2E-4A46-9801-041BCAB14B68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b4e3b96d3996f7514970ddec9359e907312d1536","datavalue":{"value":"closure semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q541222$F6F8B249-4784-437D-A917-9C01C5537081","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541222$D3B34480-C8A0-40EB-A228-08446BEC4FED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f24032ff3cf9f3c17f8d1145a9d47bb4d132d5c1","datavalue":{"value":{"entity-type":"item","numeric-id":34508,"id":"Q34508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541222$8D8573CC-CF9C-4C27-A1B8-C76318F5C9B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541222$CE11AC3C-AB20-4FDD-BF6E-764C32CEF047","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bb6c2d18287764041ae60ee5f8b5af9b2b2245a7","datavalue":{"value":{"entity-type":"item","numeric-id":40357,"id":"Q40357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541222$075408B3-E4FB-4F13-AC78-F0E6F6678F44","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":"Q541222$64B34085-67C7-4366-BCBC-DCD356B5944E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8cf07f2a1610e9890726f3ef972916e414ba4ec0","datavalue":{"value":"https://doi.org/10.1016/j.tcs.2011.01.032","type":"string"},"datatype":"url"},"type":"statement","id":"Q541222$D60626DA-290A-4E58-A87A-D2783FE77D55","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9c823074bbf22f5d7477ce9fd96c22b558a3a482","datavalue":{"value":"W1974676396","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q541222$D38182C0-7E78-482A-8567-C6996F599178","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0dd09b3fecfbd3fb9f542f7c1e52e3df257f2b9","datavalue":{"value":{"entity-type":"item","numeric-id":4817544,"id":"Q4817544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541222$B6F7E00A-2705-4D62-B323-DA4791452A53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"771dd03f88bc6af814bf7fe11d9a6d384ddec583","datavalue":{"value":{"entity-type":"item","numeric-id":3434722,"id":"Q3434722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541222$C8C8915B-C358-4438-ABF5-021C6D99630B","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":"Q541222$02FCEFD2-BAAA-462D-894C-E5029C945849","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"53272d2173db9c6e31a2df5def7f3ca8e8e0c9bb","datavalue":{"value":{"entity-type":"item","numeric-id":3753927,"id":"Q3753927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541222$AF8405F0-A6F3-4008-849D-D22504A84429","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9b74789688ac51b7ade23d361083007c0a41b1ca","datavalue":{"value":{"entity-type":"item","numeric-id":5966707,"id":"Q5966707"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541222$839B4508-37FC-4248-9D01-D07524D08052","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e8b322b85068cda5215340355caf80f566f6f15","datavalue":{"value":{"entity-type":"item","numeric-id":4494393,"id":"Q4494393"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541222$76EC4E12-CC5C-47E0-9D77-7A174FDB6624","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"198813c726927c2db34a055b30aee635496b00be","datavalue":{"value":{"entity-type":"item","numeric-id":3377460,"id":"Q3377460"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541222$E76EADC3-7507-4324-9A5D-D95907D3453F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da6449fa32317f64e0e88162e1e76272b77ced27","datavalue":{"value":{"entity-type":"item","numeric-id":1272764,"id":"Q1272764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541222$87695695-307E-42DE-9D59-19393328C694","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d78f9e51b63c4e692cfd1c2dfcec05b263377e7f","datavalue":{"value":{"entity-type":"item","numeric-id":5477669,"id":"Q5477669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541222$41C049B2-710D-4EC0-963E-42A07F357865","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"06c35a02114839df8ec37c9b47eb3fe93b7baaeb","datavalue":{"value":{"entity-type":"item","numeric-id":3141916,"id":"Q3141916"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541222$DF2C4EEA-3840-4FD8-8E53-38142E5395E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"085f2f402bb0aaa918a693e06aa64da16c2193f2","datavalue":{"value":{"entity-type":"item","numeric-id":5687569,"id":"Q5687569"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541222$89483AEE-B447-46FE-B21A-1D8E57D7CE4D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"af3c724c575d387ffa31bc58a396871119fe7974","datavalue":{"value":"10.1016/J.TCS.2011.01.032","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q541222$7EA7C64D-3B69-4A95-B24F-071C9BD6818C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3167cd4cfd397a2a8e68118a29816a1a96753ed5","datavalue":{"value":{"entity-type":"item","numeric-id":3434722,"id":"Q3434722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"780e0c341d04df84f457d2a484ebb924726c2f8b","datavalue":{"value":{"amount":"+0.831607460975647","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":"Q541222$36439985-1451-412E-927C-CEDCF97330F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8f4407264dcf973a7a6165955b28c3e3cb06763b","datavalue":{"value":{"entity-type":"item","numeric-id":3176383,"id":"Q3176383"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"01c6c785917625cf3cb2d8f616466cb9f1fe9a6c","datavalue":{"value":{"amount":"+0.8059229850769043","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":"Q541222$43D0BA5A-F847-45F1-9970-802A0C913778","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4e829a9cb3ac79d1e0677ff881a4ef71fb2d5269","datavalue":{"value":{"entity-type":"item","numeric-id":4817544,"id":"Q4817544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ff738754f9bfb0f4ef0c9b0d8a26bda017a7b8f8","datavalue":{"value":{"amount":"+0.7931001782417297","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":"Q541222$4A8BA636-93BE-4AD8-AC9E-8535D2BBFAE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"124f67889e8bbd9aa673433a181b944c636f9cf3","datavalue":{"value":{"entity-type":"item","numeric-id":3636800,"id":"Q3636800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"81ebeaeabe599906b7477583df6d8ae0b1a1ead0","datavalue":{"value":{"amount":"+0.7880678176879883","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":"Q541222$41FEECB2-18A7-4B73-ACF2-A62566B74B2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"54f9bd9490b6f1b69f322f75bdfaf05acbb25e5f","datavalue":{"value":{"entity-type":"item","numeric-id":526779,"id":"Q526779"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bb22f2525def4df0ca9b469ee7bc6f23af93e9b7","datavalue":{"value":{"amount":"+0.7860106825828552","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":"Q541222$9E705DE6-D326-43DE-B8C3-49C930F7D538","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_novel_formalization_of_symbolic_trajectory_evaluation_semantics_in_Isabelle/HOL"}}}}}