{"entities":{"Q3568224":{"pageid":5598128,"ns":120,"title":"Item:Q3568224","lastrevid":87397577,"modified":"2026-06-04T11:34:52Z","type":"item","id":"Q3568224","labels":{"en":{"language":"en","value":"CTL-RP: A computation tree logic resolution prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5722874"}},"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":"Q3568224$83092E34-C60F-4CC4-97E0-A849E22767D4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c72bd6f25d409af0549df8bb4048f6f182157631","datavalue":{"value":{"text":"CTL-RP: A computation tree logic resolution prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3568224$3FB85F01-6921-4FF7-9B09-6EF4D4601105","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a445b79382b70d63559f62234fe563aa5226fb4e","datavalue":{"value":"1205.68365","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3568224$4DFE2A22-FBCD-41AF-878E-5D3B091DCCA0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ee9aabafa7f838fbf5e6ee1c42657237b75c5f01","datavalue":{"value":"10.3233/AIC-2010-0463","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3568224$9F1F2023-AD42-4415-9B9D-B54BC4101CAC","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"86eaa5dde981e4173207292c8c7312c59a933956","datavalue":{"value":{"entity-type":"item","numeric-id":235703,"id":"Q235703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3568224$B6B51CC0-690A-4A5C-A740-C132143A3161","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"531bacf41fa7f19b08f4a713dec30b9d0307505b","datavalue":{"value":{"entity-type":"item","numeric-id":924722,"id":"Q924722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3568224$CAE41260-6FEB-4FD5-AA3A-00AE4AF4F782","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e7c764ac21e0f0934969acd440140a93a6d4c985","datavalue":{"value":{"entity-type":"item","numeric-id":1383356,"id":"Q1383356"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3568224$514F7274-B0F4-46A6-957E-0F93BA99B243","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b0d5ef245f17a6ec236579b9502514ae3fc93c36","datavalue":{"value":{"entity-type":"item","numeric-id":2811219,"id":"Q2811219"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3568224$5B9F4396-48FB-41D7-8AA9-9691BFFA6054","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1f3ce47aa4f0dc34b47bc79e3d35b38da1ee5e5f","datavalue":{"value":{"time":"+2010-06-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":"Q3568224$56285A08-1725-4C5F-8991-0A57DD34EA26","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3568224$3DF2C3CD-7C3E-4358-8EF5-71E2AAA49C97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"62ae2f4e9717dc72a20d2c4f17bdde30d85a417c","datavalue":{"value":"68T27","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3568224$9E235EBF-5858-47DB-8954-01AA4AA42884","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"43710cd70e81ac518c4a4e16ec938431536c54d9","datavalue":{"value":"5722874","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3568224$E5D7DF85-EA36-4718-8121-7BBEB08919C0","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5bb64f2dd8c681aa4257a13634b9f78827d61857","datavalue":{"value":"branching-time temporal logics, resolution theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q3568224$813B6D5A-05C5-4A8A-99F6-D80A255E5556","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"351376af9337c9358d4b7714d8543cf671d9a4b6","datavalue":{"value":{"entity-type":"item","numeric-id":26576,"id":"Q26576"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3568224$7C53B475-F412-49F4-B0AC-0B3596DA9903","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c6f90a2f4d38316e0bb5a27c4b90cf6cce495aa0","datavalue":{"value":{"entity-type":"item","numeric-id":16295,"id":"Q16295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3568224$FBDF7D24-B46D-47CD-877C-E7C2BEC6E12F","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":"Q3568224$1CA7050F-D2F4-40BF-8D47-A8BEDF50D7C6","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5037c8e5eec8ddfbb8c2fccf70e0d9a351b17094","datavalue":{"value":"https://doi.org/10.3233/aic-2010-0463","type":"string"},"datatype":"url"},"type":"statement","id":"Q3568224$DE805B98-8521-45E7-B2A5-ACCCBD8FB517","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d48eb32171f12063de26ac869d44500f1f8c0942","datavalue":{"value":"W1671579239","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3568224$DC976B2E-5DB4-4884-A85E-E5A9994479AD","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"50b0aaaed09b0b5c28910245c964b3ff93c05623","datavalue":{"value":{"entity-type":"item","numeric-id":5191106,"id":"Q5191106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5d1dfe94433eb78dd66e17092aef28eac584febe","datavalue":{"value":{"amount":"+0.9038023352622986","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":"Q3568224$FCD3F5C8-19DC-4EB2-AB52-9FA0F3EC6490","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":"f5ab3f770c8d3d7f20277f87f4b804efb376d5fc","datavalue":{"value":{"amount":"+0.7961454391479492","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":"Q3568224$E4FCA58D-1713-4D3F-89E4-92A73BE1F2E4","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":"8f187e4ad8e94bf5c4fb8857dfee3b0e899ed3e8","datavalue":{"value":{"amount":"+0.7950608730316162","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":"Q3568224$0FB21E0F-106B-4CA9-B2A3-853CCDB63DBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e9e807ba28c404afbdb10d863d94e82cf902f46b","datavalue":{"value":{"entity-type":"item","numeric-id":432138,"id":"Q432138"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7f3235ba49e9238220b231200bba86b415705c97","datavalue":{"value":{"amount":"+0.7949392795562744","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":"Q3568224$EA1EAFFA-5CAA-4158-96A1-206F1AEB4E04","rank":"normal"},{"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":"654ffc3cc8dc308b0ed5ffce14da92d75b245b18","datavalue":{"value":{"amount":"+0.7897166013717651","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":"Q3568224$690B782F-910C-4320-9EFF-21E356F6C8A3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"CTL-RP: A computation tree logic resolution prover","badges":[]}}}}}