{"entities":{"Q862827":{"pageid":864675,"ns":120,"title":"Item:Q862827","lastrevid":50006587,"modified":"2026-01-12T14:49:35Z","type":"item","id":"Q862827","labels":{"en":{"language":"en","value":"A clausal resolution method for branching-time logic \\(\\text{ECTL}^+\\)"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5118382"}},"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":"Q862827$BFCBD499-79C1-474A-B9D8-0B7B8C81737F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"deb73f816729edd0a13a6657535f173c73cc2650","datavalue":{"value":{"text":"A clausal resolution method for branching-time logic \\(\\text{ECTL}^+\\)","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q862827$11D131B8-066A-42A2-983D-71B7BDC8186F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"15acab1e77fa9c6e0da2c7f4d9420db62662e9b8","datavalue":{"value":"1112.03010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q862827$4432F8A7-3EE6-4F30-B36E-8ACDC6987A2F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3a0c039d765482b928c3f3eae6d2c20d57ac6169","datavalue":{"value":{"entity-type":"item","numeric-id":862825,"id":"Q862825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q862827$44B2DC24-4184-4A59-A43F-5F77644F2055","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b656f62e97554a998e2f0d6aa876c3a4cf8788d8","datavalue":{"value":{"entity-type":"item","numeric-id":862826,"id":"Q862826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q862827$30A3911B-857C-4AE6-AC9E-27B415774D55","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7346dc34d1d50fea46ec345fbc7e3214530889ab","datavalue":{"value":{"entity-type":"item","numeric-id":276517,"id":"Q276517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q862827$F491F099-BBB7-4D97-94FE-97CEA30B20FB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b780548d1931bae4ac5b1caff374698a268a9351","datavalue":{"value":{"time":"+2007-01-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q862827$87BE509A-C08D-4280-9034-C4A31044499C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q862827$10BD5E82-CCDF-4631-B419-23288F7CAC94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q862827$6C8B2413-6E4C-4F56-A311-6130EDC807AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q862827$CB7CDFA7-9CE0-4E5C-A1F8-1AF2FC9F7882","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q862827$7DA2237C-AD92-4FF7-968D-CDE0C9280D55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q862827$883339E9-2DE8-4A86-AEB9-52489107F6CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q862827$54BB0336-6E94-4A00-94F6-4DA1E74EEB65","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c8668a87ad0a2c1c80ea56339a18ea9c9d364997","datavalue":{"value":"5118382","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q862827$10EC258C-E2D0-4FAB-9868-BAADA2116A4A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a20a062630d1bb5cf9aa5d669cd08fbd3eee7671","datavalue":{"value":"automated deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q862827$60D90FF2-E352-4E17-8637-DEB5E3563F1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bab95dfbcdceac6cb0c1480eb7dd795ff46e5c45","datavalue":{"value":"branching-time logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q862827$36D97775-0E55-45D9-9FCC-3D47DEAF6F6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eb24640e171cf57876337d4a041eb77419f90f12","datavalue":{"value":"program specification and verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q862827$28EA97CA-C6B4-49CD-AC1C-3BE1F98D20F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q862827$8D0B26BF-BDC1-4771-82D3-492B30A3675B","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":"Q862827$50C7EE95-FC52-40F1-9941-2572035579D3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"887075274f9213e59e3e9cda3980fa1c21c24e26","datavalue":{"value":"https://doi.org/10.1007/s10472-006-9018-1","type":"string"},"datatype":"url"},"type":"statement","id":"Q862827$2537A721-15DC-4CCC-9DF6-C90E4337B286","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"794b352a3ef2dc01385daa467cdff59ef9c9b8a1","datavalue":{"value":"W1983538726","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q862827$4143191A-297D-4B3D-8CB3-0D24151C6284","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b1137cf78c4cad0e217f70ec321f2a593915490","datavalue":{"value":{"entity-type":"item","numeric-id":2751353,"id":"Q2751353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q862827$7CFF6A8B-65BA-43EF-AB1E-D6D9C07658E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e1bac099fbe4678082a91d992b4ab581e8ee2e8","datavalue":{"value":{"entity-type":"item","numeric-id":4421285,"id":"Q4421285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q862827$F09C8BE3-CD4B-492C-8391-809D92C85D7A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"395f0c4f840021549fd3880e42aed6b986058659","datavalue":{"value":{"entity-type":"item","numeric-id":2495388,"id":"Q2495388"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q862827$102185C0-58EF-4F90-BC28-982BCF6A7C25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"26b89896d12727ad637f84067fae27b2c42f93ee","datavalue":{"value":{"entity-type":"item","numeric-id":2760241,"id":"Q2760241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q862827$C88C542E-DB9F-4DB3-9F50-7AC91D761A0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3cd835cd92b4ffb8a8dc9181c7068cd47877b025","datavalue":{"value":{"entity-type":"item","numeric-id":2265816,"id":"Q2265816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q862827$45AB57D7-126A-4BF4-B0E6-A9C4A1596FEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2cd56f820547becaf1640ba57e415b67b2dccf11","datavalue":{"value":{"entity-type":"item","numeric-id":3766825,"id":"Q3766825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q862827$92CF352C-1748-4D91-B9FE-6D0EDFDFD063","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93f7e9b51624f25e880af792c7f9d74c82f45335","datavalue":{"value":{"entity-type":"item","numeric-id":3722471,"id":"Q3722471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q862827$39FF48F7-95E7-4772-8477-71DCA04406E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5b330f5cd7a65a8735b5cd88f9d99cd7626efdb5","datavalue":{"value":{"entity-type":"item","numeric-id":4012170,"id":"Q4012170"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q862827$C93F0874-CFDA-41A5-AE0E-070C2B01A79B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4d63fad87ee9ef86f723aa7605967cbf5545e39","datavalue":{"value":{"entity-type":"item","numeric-id":3768883,"id":"Q3768883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q862827$701EA7C0-B476-444E-BB7C-50B711FE6EEC","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e7288c00b9cd84eda22efc555c6b02fc8a32a5e4","datavalue":{"value":"10.1007/S10472-006-9018-1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q862827$368CCF66-7283-4CE5-92E1-757355F4AA84","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"95ea9aa45486b72268cfa1c99d9e71cf1836aabe","datavalue":{"value":{"entity-type":"item","numeric-id":2495388,"id":"Q2495388"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1cc6082586ea1255fe288fcbedd77efde2053c8b","datavalue":{"value":{"amount":"+0.9224652647972108","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":"Q862827$9F50D45F-3346-40C3-82F1-BCDFEBE2F12D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0397c16d05660865fcc8040789ba222e8321fe95","datavalue":{"value":{"entity-type":"item","numeric-id":4421285,"id":"Q4421285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b83300998651af0272d5cd64acc472d6cac2b0ac","datavalue":{"value":{"amount":"+0.8840079307556152","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":"Q862827$B14CB121-2F2C-450F-B79C-89D0C55F3981","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ce5e0b8d098d3904f1abf841ee4f7c4b9abf9c8c","datavalue":{"value":{"entity-type":"item","numeric-id":4941896,"id":"Q4941896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8b3baafc9f32617166cc72a4e5764d9cde3d0d77","datavalue":{"value":{"amount":"+0.8624460697174072","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":"Q862827$2E00B5C6-49D4-44C9-85F5-CBE830FB4036","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"516d48398076e912b71a16180c018b3f2f44c9ca","datavalue":{"value":{"entity-type":"item","numeric-id":5410337,"id":"Q5410337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2bcf96d0d2787a7460d10cca0bf4fe4b507c68fb","datavalue":{"value":{"amount":"+0.8330243229866028","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":"Q862827$483268ED-FA91-4427-A84B-7B1090E7D0DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"878200bb7d6deda2e858113e30ee5e79946f3371","datavalue":{"value":{"entity-type":"item","numeric-id":2500472,"id":"Q2500472"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6ae5f80338596b567dd0094d7f667c125d49160d","datavalue":{"value":{"amount":"+0.803753137588501","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":"Q862827$2454CA21-5A35-44A5-8BA2-ADB8F2DAF484","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:862827","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:862827"}}}}}