{"entities":{"Q1977575":{"pageid":1988317,"ns":120,"title":"Item:Q1977575","lastrevid":46899285,"modified":"2025-12-25T19:51:30Z","type":"item","id":"Q1977575","labels":{"en":{"language":"en","value":"A benchmark method for the propositional modal logics K, KT, S4"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1448649"}},"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":"Q1977575$CE350B59-F542-4253-ABD6-CF413CAA93CF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7ef6979ff278609cca73f7b9e14b1eabf0c16829","datavalue":{"value":{"text":"A benchmark method for the propositional modal logics K, KT, S4","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1977575$C6E147FB-7BC6-449A-B9D9-A59ED22A3843","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"bf7d592539c7d4e12724a7d06ec91e1c961e8660","datavalue":{"value":"0955.03013","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1977575$EC5E388A-8897-4E6B-835E-8D42350B53A5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c19aa3b53a1d8056d0379c7fdd4598f4ff96ebfd","datavalue":{"value":"10.1023/A:1006249507577","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1977575$CCEDA998-B2FD-401A-9C57-1356544BEE99","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cd6d8c3b12a00de5e492f36a193625eb2e939fe4","datavalue":{"value":{"entity-type":"item","numeric-id":1977572,"id":"Q1977572"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1977575$12DEA33D-68B5-4002-BA08-026B42C2873A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"74eb0eb5682edf2a7906d14ae0153599f4ab7c53","datavalue":{"value":{"entity-type":"item","numeric-id":1977573,"id":"Q1977573"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1977575$663E714C-D5FE-4C25-99BD-72A194D66894","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3098809787dbc9b498c06667dc239e38acbd2495","datavalue":{"value":{"entity-type":"item","numeric-id":1977574,"id":"Q1977574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1977575$F1F58E2A-2AB2-4AF5-B8C9-56428B1BAC2E","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1977575$10FB2E22-6317-478D-9469-D46E91FB8952","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3592adebaf5375a0aca8d0c2df6b20cb85499565","datavalue":{"value":{"time":"+2001-01-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":"Q1977575$17FB8377-AA97-4140-86E8-389EB3CB3F57","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"fc60bb14bc3af5ab4e4b96b2128b35fca3f34221","datavalue":{"value":"The authors propose a set of benchmark formulas for testing automated theorem provers for the logics K, KT and S4. (The classical reference in Classical First Order Logic is the TPTP library [\\textit{G. Sutcliffe} and \\textit{S. Suttner}, J. Autom. Reasoning 21, No. 2, 177-203 (1998; Zbl 0910.68197)]).    In addition, a method is given for assigning a performance index to different provers, according to certain postulates, so that one can compare the general efficiency of a given prover.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1977575$7996375B-83D9-4D20-9F96-D414BEBF83BC","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"d9c7994377655925beca167212c6ec3527b954b5","datavalue":{"value":{"entity-type":"item","numeric-id":587084,"id":"Q587084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1977575$FB58DA44-F96F-4EF2-BC41-8AD90BDD2841","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1977575$9A5086D9-6338-4CE3-A795-0241AE85D72F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1977575$49715C14-3B55-497B-8A14-7F2EC28AF02A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1977575$D619CD92-A76B-4BED-9251-47E361442956","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e08836b878504859812d0425a2d9f3b99c49cb69","datavalue":{"value":"1448649","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1977575$2FF8E21D-3D5F-4B3E-9540-674E08E6CCFA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f1dda010537b7b36bd45151721146f720815706e","datavalue":{"value":"modal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1977575$05BBCC29-EE3F-48BA-8CD9-9926C7601A45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8e84272dbac2a3ee8278e9805270916cf6e089b3","datavalue":{"value":"benchmark formulas","type":"string"},"datatype":"string"},"type":"statement","id":"Q1977575$BEF8109E-297D-4D11-94C1-D76C07021F52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1977575$A339CDED-1298-44D7-8623-0B303D956EB1","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1977575$45E731C0-F6FA-411E-B28F-B98DEB49612D","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":"Q1977575$C79A422B-3B76-46E1-B990-A8322C8C2B36","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8b38a31fb019e1c7ea5c0230b7f2be959cf08d57","datavalue":{"value":"https://doi.org/10.1023/a:1006249507577","type":"string"},"datatype":"url"},"type":"statement","id":"Q1977575$1F8A79D8-B0CE-4CE7-AE1E-F7A90B8EB30F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"46bb1d4c57c66a0f67f54fe4bbce9dc9536caaa1","datavalue":{"value":"W1593443951","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1977575$22049903-0DB6-420C-94D0-36ABCC34FAB2","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dd4f4ec85980c8c79a6bf25c0a2a61aeed189f1d","datavalue":{"value":{"entity-type":"item","numeric-id":4443417,"id":"Q4443417"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3c1e4d7af9425beb423ec006d5791831d637b9f7","datavalue":{"value":{"amount":"+0.824248194694519","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":"Q1977575$1F825B76-7549-43EF-9F9B-CECC0EEBED80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0899321ce5faacd266fb465b9c236f64db718a53","datavalue":{"value":{"entity-type":"item","numeric-id":4365323,"id":"Q4365323"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"78a3ae0a629c8bee006e41c6b8a4d4703af7d57e","datavalue":{"value":{"amount":"+0.7726891040802002","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":"Q1977575$6709EDDB-7C50-46D4-BEFA-8CDED706CDFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0070f198188188a05d47f95f4d06f1e231693ba5","datavalue":{"value":{"entity-type":"item","numeric-id":4539633,"id":"Q4539633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"426914045120a6fe35d5a8205c990a8ec8ae9271","datavalue":{"value":{"amount":"+0.7656442523002625","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":"Q1977575$852DB997-72A2-412A-B475-C4D601917597","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"44d41a256d8a0fbb20ef755ba4f2fcfca939d6f1","datavalue":{"value":{"entity-type":"item","numeric-id":1005938,"id":"Q1005938"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e3f17179cc1e63f3ede73712b8730d93f45ed361","datavalue":{"value":{"amount":"+0.7643831372261047","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":"Q1977575$77A1A3F7-5859-43B1-A5AC-C2F96F79C986","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ee590fc7e4e96baf110a09e808de8be714afffc","datavalue":{"value":{"entity-type":"item","numeric-id":1181709,"id":"Q1181709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3352b5bdfac8fcd2fe13ed428520dd6e4cc893a2","datavalue":{"value":{"amount":"+0.758125901222229","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":"Q1977575$FDEA8B7D-E903-4B86-B5FA-D0A1F0B5732C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1977575","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1977575"}}}}}