{"entities":{"Q1355780":{"pageid":1366519,"ns":120,"title":"Item:Q1355780","lastrevid":68810988,"modified":"2026-04-13T02:13:10Z","type":"item","id":"Q1355780","labels":{"en":{"language":"en","value":"Interactive theorem proving with temporal logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1014264"}},"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":"Q1355780$19266802-014D-4A51-B4A9-00B1770F37D8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ba14000beb8cffaa9e20a4d3dfe85e820496b10d","datavalue":{"value":{"text":"Interactive theorem proving with temporal logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1355780$231C7B63-2097-4B5B-9DC0-95408A4C4FF0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4fdc245c3d033b4af329748bafd8c72acddc3689","datavalue":{"value":"0872.68170","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1355780$3D154927-FE23-446B-93D3-DFB5C89F6DD5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a5fa5da603477bed196262dce34c616a0a67c991","datavalue":{"value":{"entity-type":"item","numeric-id":742366,"id":"Q742366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1355780$4FBB2A0F-2519-4863-9E8F-19110EA0F32E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c3098c31aaa054039cc5414efb85f4a6bce38102","datavalue":{"value":{"entity-type":"item","numeric-id":590551,"id":"Q590551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1355780$B5485988-9122-45FC-92FE-257B346C9C1D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ea72303f92787da89554ee5fa15621068821a762","datavalue":{"value":{"entity-type":"item","numeric-id":99061,"id":"Q99061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1355780$E577E174-856B-4C1D-A408-1A7A825D2E72","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"edfa5e14945505ceb7fb76cbee084bcc0d972deb","datavalue":{"value":{"time":"+1997-10-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1355780$4112AB9C-CEC9-434C-94DA-5781EE33DDF8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"28f4057d5e6c110393680f8f69dd57bb8b047871","datavalue":{"value":"https://semanticscholar.org/paper/47e3ed564e5f69494670608a6485c436b5172990","type":"string"},"datatype":"url"},"type":"statement","id":"Q1355780$257A1C0E-B50F-4C02-B052-A1B44261E496","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1355780$A55149EF-CB04-4FDC-A07A-9E9016630EA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1355780$50C6A660-14FD-4CF1-B4F6-3AA8DD95F40C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"63adc6ce7c6a0fa8dc3cb4790e002e5e01ed6969","datavalue":{"value":"1014264","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1355780$8857EA54-F356-4B4B-9B81-878487D95385","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1f1cf12c900aeb5813ce8f84db8812e6bb27ae87","datavalue":{"value":"linear temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1355780$D4ED09BA-50D6-4666-806B-338CDD6683A1","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"786a5236ac94f9692f521c02ac8270dab6d23cde","datavalue":{"value":{"entity-type":"item","numeric-id":29799,"id":"Q29799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1355780$1C5DDCEC-E215-4B16-8A5B-BA1C84B8453E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1355780$A6DA0274-EE2E-4B89-9B90-74632AD6C1C6","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":"Q1355780$0CE573F8-8911-4F72-8AD9-40D5DBA5F71E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"668e1129faf429127c23c9679913cb9bc4df23b0","datavalue":{"value":"W2039976806","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1355780$CCE9C8DA-E5AE-4D9C-9609-F91943169169","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"781583c77220dab36b8fc5fa58b9ae0961e122b6","datavalue":{"value":"10.1006/JSCO.1996.0094","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1355780$2D15D850-B8CD-492F-B371-ABD9D3C10230","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c4a7012ca2bd562a7e57df0b315383bccdc5bda4","datavalue":{"value":{"entity-type":"item","numeric-id":2300079,"id":"Q2300079"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1033b47c9b2a3e9a540dccef604957ce5d8cf861","datavalue":{"value":{"amount":"+0.8011497259140015","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":"Q1355780$18F102D2-EA73-4739-9A0C-7FFE71EF4449","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8289dbf842c912fbfdcafb36365317c85127fc60","datavalue":{"value":{"entity-type":"item","numeric-id":2197533,"id":"Q2197533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"335c5b4026332d8a6c1b9371a54d797692bc05d8","datavalue":{"value":{"amount":"+0.785569429397583","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":"Q1355780$6B5FE9A2-FEC9-456F-A0D1-7F8F14B5AF44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4444e22cf4a815a8834036d41840500b1509c8b3","datavalue":{"value":{"entity-type":"item","numeric-id":1895457,"id":"Q1895457"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c62915e97203598d53e9a8316b784b19d9f5df54","datavalue":{"value":{"amount":"+0.7696560621261597","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":"Q1355780$28693803-E2C0-4FDF-B837-F31698192C73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3b603f9a2204ddc0915373daffeaa615ab14400a","datavalue":{"value":{"entity-type":"item","numeric-id":4490359,"id":"Q4490359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3563cb6b7fc9e373237277c8ac6010f80569ecbf","datavalue":{"value":{"amount":"+0.7647919654846191","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":"Q1355780$FEFA9C31-F737-42F7-932A-3052C07F61DB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Interactive theorem proving with temporal logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Interactive_theorem_proving_with_temporal_logic"}}}}}