{"entities":{"Q851137":{"pageid":852985,"ns":120,"title":"Item:Q851137","lastrevid":64826994,"modified":"2026-04-11T22:29:49Z","type":"item","id":"Q851137","labels":{"en":{"language":"en","value":"First-order temporal verification in practice"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5073789"}},"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":"Q851137$79CF6703-104F-4593-8595-90D400F4A51E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e96a07d59747fd77d823f47de84fdd3e83e2dbdf","datavalue":{"value":{"text":"First-order temporal verification in practice","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q851137$7721BAF1-A7BA-4F2B-8EFF-C19443C79A4B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8f6db2dae2c81c3da5dbee4c3d42ac4ded555a93","datavalue":{"value":"1108.03018","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q851137$F103A980-B859-4B4E-A56A-B85BF8957D55","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c5832f8876614de1887b6fff71a1066143db327e","datavalue":{"value":{"entity-type":"item","numeric-id":786129,"id":"Q786129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$669AC49F-E697-4887-B335-F7CFB2253F93","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$81167E42-56DE-4D82-8186-55B7BB3A5742","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e72da49a9cdc23965ff0d1c9fcf6159ca75a2a61","datavalue":{"value":{"time":"+2006-11-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q851137$9E55F9D4-369A-4F31-99B7-F6DADD3E42BA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q851137$493FF207-2C76-4592-99F2-A02FF77684AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q851137$BDB12ADA-915F-4B6E-9499-1DAAFE559A57","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"baefa1cb94ee60ae32dc68653a17cdf369794331","datavalue":{"value":"5073789","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q851137$CA878E81-73A1-4B45-86FF-E00208A286FA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4a1a1b4de2f6601636779c475343b36943870036","datavalue":{"value":"first-order temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q851137$25AEEA14-B4B5-4BDE-B332-4361851F394D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b8fee61d23cb46f9daf1055a85964115dbe5219b","datavalue":{"value":"temporal logics of knowledge","type":"string"},"datatype":"string"},"type":"statement","id":"Q851137$313DEC10-DEE3-458D-A64E-4BD09C0291F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q851137$ED2B9FF2-B589-4E5D-B09D-FDFA3368FF4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q851137$B3C4C5E1-009B-4175-AB6B-2BBB03BE0E0E","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"176011d67804790c0bf26dea3e8097883ead3319","datavalue":{"value":"Q98283887","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q851137$931447D1-19B2-42A7-B836-B9A9ACD7EC51","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"99667ff6306724dbe63bc589a546934d523de225","datavalue":{"value":{"entity-type":"item","numeric-id":21966,"id":"Q21966"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$949E99DD-9ED9-4C97-9967-3BD46BCE9489","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b443b776731e3bc75eb79b752e7ef8c4cee2d97a","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$310367C6-64A2-4FD4-81A3-2F686B0EA53D","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":"Q851137$1BF5F234-6EE3-42CF-A052-59BC76E72BB4","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2cb7be8ef75e51c7d945b8a6e97508a775c4bb38","datavalue":{"value":"https://doi.org/10.1007/s10817-005-7354-1","type":"string"},"datatype":"url"},"type":"statement","id":"Q851137$F8EF5E87-B60A-4CFD-9967-C58FAEBEA712","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0f90893ab1727b70dd820b3d7d4165ff363282d5","datavalue":{"value":"W2065380071","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q851137$2F96F367-24F5-442B-99A5-2996FF28BC7B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"37e804d7aea2d1418057c94d927a03053fdf3435","datavalue":{"value":{"entity-type":"item","numeric-id":1601879,"id":"Q1601879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$4F64D144-370B-40D4-B1D0-783BC34B3D54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e6d22c4f0f18fa0a8fa8a72b3aa3dd8f4f8c3a4","datavalue":{"value":{"entity-type":"item","numeric-id":1908342,"id":"Q1908342"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$A8E9BB86-C3A4-407F-A54E-E34C105C8E18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d8546934d1a971d73166157b270518f6fc63999b","datavalue":{"value":{"entity-type":"item","numeric-id":5900729,"id":"Q5900729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$7D6D082F-7418-4B77-A36F-9F9EAACE7D79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"51eb2f16343f4cf146e8519c84d3ee965035a1ba","datavalue":{"value":{"entity-type":"item","numeric-id":3408140,"id":"Q3408140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$AD03D616-36BC-4FD2-8687-BD48A2F0D2E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9397c0ca21fdbbac66956e5308e7ec33a27c2d64","datavalue":{"value":{"entity-type":"item","numeric-id":2702565,"id":"Q2702565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$688CB291-DFC4-4207-BC73-4A3EF9025086","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fd1708cfc46a389f6b2616c3dfd0c367a4c0790e","datavalue":{"value":{"entity-type":"item","numeric-id":4209289,"id":"Q4209289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$72C98CA9-78F1-4B9B-BD30-8529C246FF11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"120c8e41431895a309f8ef32cac52a772f33d796","datavalue":{"value":{"entity-type":"item","numeric-id":4385542,"id":"Q4385542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$ABCA2B88-E1B0-4163-9E06-AF576ECE2A8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05cc22e70cd29988fee99676201ee18c4ac4f87e","datavalue":{"value":{"entity-type":"item","numeric-id":4351796,"id":"Q4351796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$778B776A-5350-4105-8A36-699B374C3FB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"047205c489fbc234ded30a0b774835426a93b0e0","datavalue":{"value":{"entity-type":"item","numeric-id":1422049,"id":"Q1422049"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$F0D892C5-CB7F-48AF-9C73-EFCFB5A639B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8280aaa780c3cf7d95f0d867169f4c1e1bc3f64b","datavalue":{"value":{"entity-type":"item","numeric-id":5715695,"id":"Q5715695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$D2737657-D372-4E62-9F89-3DBC6EB801AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c81c210aa51b53d004ca3564c20b46519be31e0","datavalue":{"value":{"entity-type":"item","numeric-id":4948538,"id":"Q4948538"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$96EBA433-3379-4F4A-BFCD-D67261FB7C90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9454776c8e95be8590581925e4520a2ce0d4e418","datavalue":{"value":{"entity-type":"item","numeric-id":1119565,"id":"Q1119565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$038078BC-E90C-4427-AB97-F9943ECC8AA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0b28346939d64d7b059d337185059efec5b3f823","datavalue":{"value":{"entity-type":"item","numeric-id":1863828,"id":"Q1863828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$38CB128E-BDD3-4476-9E35-34FAA93BEFA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a25c01e8d4be176dddf944065ec7d363ffdadbd","datavalue":{"value":{"entity-type":"item","numeric-id":1591203,"id":"Q1591203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$93842859-7247-47B9-BC1F-9BBC50134BD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b5dfbb5bd6c7d89dd077ac227b69a104533f344","datavalue":{"value":{"entity-type":"item","numeric-id":5307069,"id":"Q5307069"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$4E9D3658-AB4F-49A5-B88D-EA561AC6B8B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e354eb56d1cea816c283aaca8bcbdb05e7271a41","datavalue":{"value":{"entity-type":"item","numeric-id":2486579,"id":"Q2486579"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$2CDA562A-AE43-47F1-907C-DB66936EE0DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4968b8cabc6e7e2146fbbb19353be5139e1037e5","datavalue":{"value":{"entity-type":"item","numeric-id":4002642,"id":"Q4002642"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$21AA5D72-D2DA-42D4-8F5E-FE5D451DCE85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"174e3f2701a2bacd196e2d244539c0776079d382","datavalue":{"value":{"entity-type":"item","numeric-id":4858037,"id":"Q4858037"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$480DF450-47AC-4D7D-A163-4680B931AD2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2fefd3695fc6c127353eeeaf9bb631916756e929","datavalue":{"value":{"entity-type":"item","numeric-id":4168037,"id":"Q4168037"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$3D78778C-66D4-4B0F-A47C-E1824B5C57CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"008723b33cb14bbda59226503d753d137dc6f8ef","datavalue":{"value":{"entity-type":"item","numeric-id":1098330,"id":"Q1098330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$FE47611B-B4E0-4908-A17D-16D05ACF46E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0cb051a6b1eb9b88364c46513701492fc0e99189","datavalue":{"value":{"entity-type":"item","numeric-id":3150300,"id":"Q3150300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$86B5B16D-A944-4F43-8722-CD0E0F99A015","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"579ae597b0782ef330ce6a47c42ceecfe91b0160","datavalue":{"value":{"entity-type":"item","numeric-id":5900730,"id":"Q5900730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$8CF0609C-F18D-4960-8783-DE181DEF8DFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b3b11555faa74c9dd9ad74dc7ae9b8d6db990575","datavalue":{"value":{"entity-type":"item","numeric-id":1904404,"id":"Q1904404"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q851137$085E2736-E945-4C31-8CDE-08918D207C3A","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"7f60403b213e45e2c292f55fa4af6f5058035d52","datavalue":{"value":"journals/jar/Fernandez-GagoHDFK05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q851137$3F6FB65E-48F1-4941-A190-500F18749EB1","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"92f8356958b2dbce6f1540a6de619e4e8bb5c083","datavalue":{"value":"10.1007/S10817-005-7354-1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q851137$14AE5C34-991F-45E7-93DD-294A2BE24658","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bacb2655f24cf763ac0a90cba76831de3a67b9f4","datavalue":{"value":{"entity-type":"item","numeric-id":2486579,"id":"Q2486579"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7039622fb8a389337d6d8391efe72f7bbb7b1aac","datavalue":{"value":{"amount":"+0.7758742570877075","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":"Q851137$FB8BC4FE-3986-4DE0-9BCB-6DBA251AED9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4861a14ab967cf642d0c02bb6a8219904e654998","datavalue":{"value":{"entity-type":"item","numeric-id":5900729,"id":"Q5900729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"95b1aaba888b37c102e377d564daf21cb22f2394","datavalue":{"value":{"amount":"+0.7688433527946472","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":"Q851137$F3FEDCEF-F892-4BE8-8D2F-65BDF20A82FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"27780aec0d5eb5cc4ca2ca574681644ff67f3ee7","datavalue":{"value":{"entity-type":"item","numeric-id":1350527,"id":"Q1350527"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8d0c6dd5a682660bcc3add332c98b404648ad28c","datavalue":{"value":{"amount":"+0.7681460976600647","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":"Q851137$7ADCD119-8DBD-45F9-9ED2-BA3AD0A67AA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d2a29d0306f804f3bd56e2fc0751c80afa2ebd71","datavalue":{"value":{"entity-type":"item","numeric-id":3474286,"id":"Q3474286"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4626e86d60244f11f9af9268d9726812cad6693b","datavalue":{"value":{"amount":"+0.7638673186302185","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":"Q851137$9ACE3410-F8D6-4DD7-856B-99E37B151E2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2ecfe897fd42087dbb77e7e02edb6a256aae0e03","datavalue":{"value":{"entity-type":"item","numeric-id":2996150,"id":"Q2996150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d6099a8763d918871e5d340869a05037f70ca16c","datavalue":{"value":{"amount":"+0.7612454295158386","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":"Q851137$A3D3746C-40A6-4A86-8271-6A53B3FC5249","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"First-order temporal verification in practice","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/First-order_temporal_verification_in_practice"}}}}}