{"entities":{"Q7361475":{"pageid":31519964,"ns":120,"title":"Item:Q7361475","lastrevid":105366701,"modified":"2026-10-07T13:36:42Z","type":"item","id":"Q7361475","labels":{"en":{"language":"en","value":"Linear Temporal Logic"}},"descriptions":{"en":{"language":"en","value":"AFP entry LTL"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4fb23cb41ceec10674afe7c1502d877d8fe37efb","datavalue":{"value":"https://isa-afp.org/entries/LTL.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361475$00361EDC-CE5E-4186-9DA3-24B841039E62","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"40a47289abfd31f69fe37ba4c6b3070ad16edf97","datavalue":{"value":{"time":"+2016-03-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361475$9D1893EE-7EF5-4BA2-BE73-C47A3D3990E4","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"34ca23e13f3744b21ae1779c590b97468a47c009","datavalue":{"value":"Salomon Sickert","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361475$3114789E-0FED-40E6-A96C-32665070CCA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"35d09caaadf85c8cddb24e4ac2098ba8a6337a32","datavalue":{"value":"Benedikt Seidl","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361475$292C8C59-6AF9-486D-A28A-01EA17EB495A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9a7b7108afea8fed68ced15b2c249f5b4b3d254a","datavalue":{"value":{"text":"Linear Temporal Logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361475$1219842C-E0BD-4AEC-B217-527E780CDE9D","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"43fdf347bbe3e45bed5af061af085b889377a0d9","datavalue":{"value":"This theory provides a formalisation of linear temporal logic (LTL) and unifies previous formalisations within the AFP. This entry establishes syntax and semantics for this logic and decouples it from existing entries, yielding a common environment for theories reasoning about LTL. Furthermore a parser written in SML and an executable simplifier are provided.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361475$6C98BA4A-8891-4B99-9B0E-DA59E269B249","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c906cc491504927b1b4f424ee7fe2803fd3b11df","datavalue":{"value":{"entity-type":"item","numeric-id":1572746,"id":"Q1572746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361475$41B4E0C5-010E-44F5-B956-AB47CE7F168D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f2cd54413287e6e70989953202b0183dd784ecbc","datavalue":{"value":{"entity-type":"item","numeric-id":2754087,"id":"Q2754087"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361475$9E08D525-2C52-494A-BD60-87AE4AC08D18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ddcc641ff7e57a4e6017578f7e30b24f5a72870b","datavalue":{"value":{"entity-type":"item","numeric-id":766306,"id":"Q766306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361475$7904FF47-14F6-4853-B53D-C5911D8CD038","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a9d943a0ef985ccc7c0d6f0843144df920387ac2","datavalue":{"value":{"entity-type":"item","numeric-id":2894268,"id":"Q2894268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361475$35DF8BCE-B65B-4B55-960D-D5E5FA856C39","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":"Q7361475$ADE35C26-A46E-4996-A0D4-683ABA9D8BC1","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"c9cc367333522e85e08c5dafe5daee23f98b641d","datavalue":{"value":{"entity-type":"item","numeric-id":7361409,"id":"Q7361409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361475$494E0ED6-DB41-4A6D-BB13-C4180EDA017E","rank":"normal"}],"P2651":[{"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":"Q7361475$A4437459-0B88-43F6-975B-B04109741615","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":"Q7361475$8506A9D4-36E3-4AAD-807E-0AB5E2F8F816","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Linear Temporal Logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Linear_Temporal_Logic"}}}}}