{"entities":{"Q7361405":{"pageid":31519754,"ns":120,"title":"Item:Q7361405","lastrevid":105365699,"modified":"2026-10-07T13:36:16Z","type":"item","id":"Q7361405","labels":{"en":{"language":"en","value":"A Verified Proof Checker for Metric First-Order Temporal Logic"}},"descriptions":{"en":{"language":"en","value":"AFP entry MFOTL_Checker"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"42c053b02cd335eaa7924e7157d76e4e8d1705e5","datavalue":{"value":"https://isa-afp.org/entries/MFOTL_Checker.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361405$3A223746-A131-45F5-B0B6-458A1DA78504","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b0e93a36236072eb62846cd5f688ff9538edf556","datavalue":{"value":{"time":"+2024-04-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361405$2D873F6C-6C63-469A-A8C9-CA8B08EAC32D","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"1fd7c94d6c676e0a5bb1e15738c874ce160c1c85","datavalue":{"value":"Andrei Herasimau","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361405$4F8F5670-8BE7-43F6-9624-BA7ED3CB0715","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"5794d91a39dde2e8f368834014ac9f67037fb91a","datavalue":{"value":"Jonathan Julian Huerta y Munive","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361405$1B683F01-334B-4020-A8B6-D020F2ADF639","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"57339c5889ac038ac6587415b4b314d4ec8f5d10","datavalue":{"value":"Leonardo Lima","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361405$9E7E73C0-6242-4578-8782-D489D5D9A257","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"643eb3a0705e82fe3a3d92aab3f3a27de8fd83be","datavalue":{"value":"Martin Raszyk","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361405$F1F52FEC-8210-4439-A58B-E45DBBFF5536","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"2500aa80beaafa12dfa4ab6c7d8363674f762e6e","datavalue":{"value":"Dmitriy Traytel","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361405$AC816C34-7496-4841-82BE-FA6CAAC08589","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b7481d26f596dd0e3baf0d2e7a439396bf767016","datavalue":{"value":{"text":"A Verified Proof Checker for Metric First-Order Temporal Logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361405$234830B0-10D3-4A4A-A5D0-5B813D418DD2","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"825681ab3c3d169cdd6aecc5971038747eed79d5","datavalue":{"value":"Metric first-order temporal logic (MFOTL) is an expressive formalism for specifying temporal and data-dependent constraints on streams of time-stamped, data-carrying events. Recently, we have developed a monitoring algorithm that not only outputs the satisfaction or violation of MFOTL formulas but also explains its verdicts in the form of proof trees. These explanations serve as certificates, and in this entry we verify the correctness of a certificate checker. The checker is used to certify the output of our new, unverified monitoring tool WhyMon. The formalization contains another unverified, executable implementation of an explanation-producing monitoring algorithm used to exemplify our checker.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361405$8628084F-012E-4F9B-9BF4-17902CA0BDAF","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"409913c6d56f4d7474aa85e7d22a8a9eff38193b","datavalue":{"value":{"entity-type":"item","numeric-id":6536149,"id":"Q6536149"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361405$37263619-3E20-44EF-AB23-A68017AA90B3","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361405$DD365DBB-A194-4350-8278-9C86EA9E2A2A","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"35a8e4bc0e4a396cad3ea2a5ddc1f09e16c598c1","datavalue":{"value":{"entity-type":"item","numeric-id":7360787,"id":"Q7360787"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361405$AC332038-5A26-4695-8AD6-23703E4CEA3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P2651","hash":"8e49b85c564ad000f6e625e227bc24c09664b65b","datavalue":{"value":{"entity-type":"item","numeric-id":7360815,"id":"Q7360815"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361405$9817846F-F60A-4966-BECB-4AFB9CCD2B61","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"ddf89b3a1502629b945735d034d072c7b6b3828e","datavalue":{"value":{"entity-type":"item","numeric-id":7361410,"id":"Q7361410"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361405$13A51FD1-4D58-4389-B809-C57016D559D0","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361405$52594EED-2368-42F0-AE3D-AE4244A35BC5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A Verified Proof Checker for Metric First-Order Temporal Logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_Verified_Proof_Checker_for_Metric_First-Order_Temporal_Logic"}}}}}