{"entities":{"Q3454120":{"pageid":5233520,"ns":120,"title":"Item:Q3454120","lastrevid":88240793,"modified":"2026-06-04T14:00:24Z","type":"item","id":"Q3454120","labels":{"en":{"language":"en","value":"KeYmaera X: an axiomatic tactical theorem prover for hybrid systems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6515530"}},"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":"Q3454120$095C1A4B-0F6C-4500-B178-2C3BB2A28FBB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"925cf03515143d06d6837e4e53fe49040ae392f6","datavalue":{"value":{"text":"KeYmaera\u00a0X: An Axiomatic Tactical Theorem Prover for Hybrid Systems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3454120$9B015642-EDCA-4B36-A591-54BA95B90B7D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c13f291351e77de7b25d6c572382af853622fba0","datavalue":{"value":"1465.68281","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454120$409946D0-7045-4633-9064-0E66EA627D32","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9faa496e7224f3ad9033457557697b2d0f820ba5","datavalue":{"value":"10.1007/978-3-319-21401-6_36","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454120$FB4B1805-0AF2-4B8C-AEB2-A2A957FDB1B7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6b2c31dab8869475cc8b66646b92dc92c1b9c06d","datavalue":{"value":{"entity-type":"item","numeric-id":1687736,"id":"Q1687736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454120$A37079B0-6A4E-49F5-9C10-797DCBABAD6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b16426e16334f11344c5d2b57762ae4aeb39220a","datavalue":{"value":{"entity-type":"item","numeric-id":681464,"id":"Q681464"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454120$FF1C9796-D1A0-4EDE-8CD1-5AD21D2D4751","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"23eeef9589cbe39cdbb39af3bc4bb2d05242b0e6","datavalue":{"value":{"entity-type":"item","numeric-id":2908513,"id":"Q2908513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454120$8CAC14D1-C0CA-4A43-821F-8DC868349EAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"294fd8051deb8524fd06e56188039253c095891d","datavalue":{"value":{"entity-type":"item","numeric-id":835772,"id":"Q835772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454120$607F0045-F5BB-45D1-B986-4A8AD4E93BF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fc654f17b8a10219c5683cabcebc6a770c6278e4","datavalue":{"value":{"entity-type":"item","numeric-id":681339,"id":"Q681339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454120$6A538622-C8FE-44FB-B22B-AC4A2715428F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3cc4c7edeb37e5e3024aeff0de74501df6e066e3","datavalue":{"value":{"entity-type":"item","numeric-id":3454078,"id":"Q3454078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454120$280C9294-151D-4E5E-A24B-1316CB5896D8","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9f34c33daac76be2878f4eb0eeca7aa927e679a8","datavalue":{"value":{"time":"+2015-12-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3454120$D1C0C1E0-002B-4182-B62B-6B981DEDFFA2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"89091e456ba6e880864c7dc297b0bb80745403e5","datavalue":{"value":"https://figshare.com/articles/journal_contribution/KeYmaera_X_An_Axiomatic_Tactical_Theorem_Prover_for_Hybrid_Systems/6606683","type":"string"},"datatype":"url"},"type":"statement","id":"Q3454120$0CEBF190-5FB6-4AAE-AE36-6BDCCE4DF074","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454120$2AA93DEF-0509-44D6-8620-E1F8F3A85CB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454120$1A155EA7-B32E-49B2-969A-D763142EA7F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4ea08324a913bdb8e1672d880d325e8fdf42de9b","datavalue":{"value":"34A38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454120$558F466A-4A46-453E-9CF1-7F1C877594F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454120$C55AC96A-8345-4FBA-B272-DFFD7FF40514","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"03dab433bfba873019afb801c4b74e582f4fc43f","datavalue":{"value":"6515530","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454120$4D430D18-8E06-4C57-979D-A3EC40910EDE","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454120$2CBAFCBC-7379-430A-98A9-1B2FACD5F6DA","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":"Q3454120$8821C804-1605-477B-A0A1-5C406B0FDA8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"49f6fb65fa6d2a219475c4a5b936c8907f84d3cb","datavalue":{"value":{"entity-type":"item","numeric-id":16063,"id":"Q16063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454120$B63CAE96-6BB5-4F25-B3E3-8E4062BC06A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"03bc0969d66f63218041357e0da6af3aa771d8bd","datavalue":{"value":{"entity-type":"item","numeric-id":56258,"id":"Q56258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454120$6478FEB1-9056-4C82-A5A9-0A2CAEF39A27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"12b8fef36068e5bdaa4e8c4c10a706c6f98b9349","datavalue":{"value":{"entity-type":"item","numeric-id":21946,"id":"Q21946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454120$975EDF16-1ECD-43E6-AC13-6736F0BF1FAA","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":"Q3454120$5A74519B-B4A8-4279-8889-41819B54EBF0","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"80f5018fa5cb50521a2a996f8a1116fcf3bfaaae","datavalue":{"value":"W1590463358","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454120$1A9D5CE7-1E86-42CE-85BB-876D94643B80","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"18fa226924cc974ee1c50efee3ff193344791f61","datavalue":{"value":{"entity-type":"item","numeric-id":5210800,"id":"Q5210800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454120$574B2C26-E188-4E9B-BCB2-D4C09DF6BB93","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":"Q3454120$77524606-E15A-46FF-83F2-1BBCEEA688B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c347c60e13d160aa53a2f40cfef7b79c62c55cc6","datavalue":{"value":{"entity-type":"item","numeric-id":1040772,"id":"Q1040772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454120$DCEC2ED9-501A-4D32-B485-3E967E203D53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"12bcad11fe97484505c727089d3af542344d4df9","datavalue":{"value":{"entity-type":"item","numeric-id":4930176,"id":"Q4930176"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454120$D572D37C-AEF3-4AFB-B62E-7A4F0070BAD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b91c17eb426dae0dddf6a4c3a8672996b8f72054","datavalue":{"value":{"entity-type":"item","numeric-id":2986778,"id":"Q2986778"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454120$801D95CE-27A2-4CEC-BB07-07C19B96B9AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d369a00a912276bbb6f1d71c301f7df62056f0c","datavalue":{"value":{"entity-type":"item","numeric-id":5277902,"id":"Q5277902"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454120$7D1AB05C-4098-451B-90D1-19A300F16C7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f293ebffa7635fb3106a8df0dadaea92d38203f3","datavalue":{"value":{"entity-type":"item","numeric-id":3454116,"id":"Q3454116"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454120$BEBC1B0B-B6C6-4DE6-ADE1-751810103E6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b3fbc226d62731020dc0ca64fe7600f26430f11","datavalue":{"value":{"entity-type":"item","numeric-id":3541700,"id":"Q3541700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454120$E5B7AD06-F454-4D4B-841D-1B16F8AC3DA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"19ada66642746211b5654261da252d4720bb95bb","datavalue":{"value":{"entity-type":"item","numeric-id":6488526,"id":"Q6488526"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454120$47BEA46A-20F5-4064-9DF3-17B0FAC3FD7E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b22f2f528629b828577d9f109bdefe9f9e3855f8","datavalue":{"value":{"entity-type":"item","numeric-id":1687737,"id":"Q1687737"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bcfd7d7e98bbf0146e9770f1aae256b199a30ae0","datavalue":{"value":{"amount":"+0.824317216873169","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":"Q3454120$B22CC042-2253-4242-A496-6D73D02C9253","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"57d2fd2ba699138a4f63804de3c693240cf2632e","datavalue":{"value":{"entity-type":"item","numeric-id":3541700,"id":"Q3541700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"80b33edc85ec635d9720da093b1b60104e207ecc","datavalue":{"value":{"amount":"+0.8179284930229187","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":"Q3454120$ABE926C7-B8F7-440C-A162-99A08DBE542A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6e3ad1daa0422dafc412338975fbacb14726f295","datavalue":{"value":{"entity-type":"item","numeric-id":2908514,"id":"Q2908514"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aeac8e18b45de93c4947dceadc50d1a124bbcd05","datavalue":{"value":{"amount":"+0.7534417510032654","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":"Q3454120$0A2C9523-E20D-4482-B8D8-02A3E4E852CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1aa1f4841de960501ed36ce114855cf0bd00d78f","datavalue":{"value":{"entity-type":"item","numeric-id":1040772,"id":"Q1040772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"11b8c753d258ff31cf0596636d8adae582afc3b2","datavalue":{"value":{"amount":"+0.744063675403595","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":"Q3454120$6A2A0FA8-95B9-4CD6-A5EF-B0C571B43BA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a36d4ffaea81afbba1040e30b03bf77b623831dc","datavalue":{"value":{"entity-type":"item","numeric-id":2520674,"id":"Q2520674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"342bb1e6749d2b8b83725a7589d0d3e8167470ac","datavalue":{"value":{"amount":"+0.728710412979126","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":"Q3454120$C2FBBA59-BEAA-4592-9816-E9E4B3AD6E56","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"KeYmaera X: an axiomatic tactical theorem prover for hybrid systems","badges":[]}}}}}