{"entities":{"Q5741559":{"pageid":7771110,"ns":120,"title":"Item:Q5741559","lastrevid":52582682,"modified":"2026-01-23T01:02:47Z","type":"item","id":"Q5741559","labels":{"en":{"language":"en","value":"A light-weight integration of automated and interactive theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6607275"}},"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":"Q5741559$305B4A96-4E4D-4483-8526-CD1073D70368","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3b7cf11f536dea4b4ed1e354b60f5e7214d8e304","datavalue":{"value":{"text":"A light-weight integration of automated and interactive theorem proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5741559$51177230-A691-40E3-B7A4-6D9ED422600D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"82ce779b0caf7e090549463e6deed6ddad0f9a23","datavalue":{"value":"1361.68189","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5741559$A2DC5A45-37B6-4982-8E67-036A6BBD4258","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f42bb681fd055ab9528686c3131fe8229ffef322","datavalue":{"value":"10.1017/S0960129514000140","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5741559$96B7F119-9DB4-4577-B3C0-87A969966471","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7b835f7012590722dffc1e957cc656b1036d775d","datavalue":{"value":{"entity-type":"item","numeric-id":5178971,"id":"Q5178971"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741559$B2564184-F639-472D-A9B6-FF39345087BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"726d6d17ffd7097481aaa7acac69959461b65139","datavalue":{"value":{"entity-type":"item","numeric-id":587965,"id":"Q587965"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741559$1002E283-48D7-45F6-BEB4-9BF54CB74586","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a53527e88e2413966f3c8ce14c92b878c452756d","datavalue":{"value":{"entity-type":"item","numeric-id":2709784,"id":"Q2709784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741559$E6FAB7D0-7DEC-402E-ADE2-62F7A9B4BD76","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"983499d539ab43bbb6f5e5531bc62eb931d87235","datavalue":{"value":{"time":"+2016-07-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5741559$EAE8517A-F63C-41BE-BC48-18987D39A178","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5741559$91138941-18E1-4407-8DAC-4C1A4DE5B5E5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b98a41a9b7bdcdbfcd9512d97cee344e87d79894","datavalue":{"value":"6607275","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5741559$FB224BB9-0461-4408-A5BA-B442608F1031","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1a8b6b13bef47cb19f4e2508b5917af235a65eb0","datavalue":{"value":{"entity-type":"item","numeric-id":21668,"id":"Q21668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741559$08AA24E3-FC40-4EAC-91EF-5037E7457CD4","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":"Q5741559$7767FADA-AA22-4F3E-B78E-E864731ED451","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f788536331bb87ba4e75963340b885a6c5e47c5c","datavalue":{"value":{"entity-type":"item","numeric-id":5747643,"id":"Q5747643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741559$E74112D9-757A-4BCC-9A83-FAD5B9ED4123","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"10e6adfc48f3005b2216b8762425b09fe34d6ad2","datavalue":{"value":{"entity-type":"item","numeric-id":5178972,"id":"Q5178972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741559$805E1B52-D9E9-482E-97A3-AAB1F57A1584","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e2785ec87503aae4e4b848bf91a2672b0c85122","datavalue":{"value":{"entity-type":"item","numeric-id":1868509,"id":"Q1868509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741559$2184A469-E24A-4236-9483-906932BBAFFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16c58bccac3eb8e167d77acc1c92ca853e7a5fcc","datavalue":{"value":{"entity-type":"item","numeric-id":2655326,"id":"Q2655326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741559$27E06D01-7FAC-43B0-8AFD-DC0E987D56E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"716d170b6d9b095492bf0c2b742ee0dbade5bbe0","datavalue":{"value":{"entity-type":"item","numeric-id":3523178,"id":"Q3523178"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741559$A2D2F276-E4A6-4C04-A8BD-CC692E8C9C3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ab5d7b35f67f940445411fa45c1b02bcb40d39f","datavalue":{"value":{"entity-type":"item","numeric-id":3999860,"id":"Q3999860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741559$28219474-59AE-4250-80B2-037B1EFD1F04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"231698d7227e366d9fe674d764042c9f593bc35c","datavalue":{"value":{"entity-type":"item","numeric-id":792319,"id":"Q792319"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741559$66B9E326-CD3A-432B-A3CD-6A526F464C61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"32c2c3cd37ae471eae65a3748f90112254f38d8e","datavalue":{"value":{"entity-type":"item","numeric-id":4758660,"id":"Q4758660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741559$DA20430B-81C3-43C7-AF28-7387742856A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1903be4a36187a0a0e197e708bc72f62f93b28bd","datavalue":{"value":{"entity-type":"item","numeric-id":3183520,"id":"Q3183520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741559$8CF1D70F-9FD0-45BA-BEA2-0DCF5EDDCC27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c39b9040e3d2807bc13175b6074f0175a0a4a1c","datavalue":{"value":{"entity-type":"item","numeric-id":5747754,"id":"Q5747754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741559$22A06544-F3C3-47C5-B1E1-8775E53996FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"197321586b52697dc5005c2bf7b5e782bc94762d","datavalue":{"value":{"entity-type":"item","numeric-id":1131250,"id":"Q1131250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741559$CC8D7D24-9D6D-4721-8797-4D5926887BFF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d31ac5b611e1dc394bc6dbb9071cf4d1998a3862","datavalue":{"value":{"entity-type":"item","numeric-id":4524769,"id":"Q4524769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9d5978773cd09283b858c2dce9c18f1a6a9a3330","datavalue":{"value":{"amount":"+0.7905959486961365","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":"Q5741559$7F6A3193-A2AA-467E-95D1-F9F2AB1FD2F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2741c52220bb969f7227380e5961fee06f2cc5a7","datavalue":{"value":{"entity-type":"item","numeric-id":264193,"id":"Q264193"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6a5eb2c116770517ff8eb8136e1256461fdd32c9","datavalue":{"value":{"amount":"+0.7388622760772705","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":"Q5741559$A3FCEB3F-BDA9-43E1-AD06-A3A829A60182","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec89f728f4f21b2786c7fd178f4ff74b964a04b3","datavalue":{"value":{"entity-type":"item","numeric-id":5178972,"id":"Q5178972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"86b393abcb3871cb1e0afcac78dbef70d035d8d4","datavalue":{"value":{"amount":"+0.7088091373443604","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":"Q5741559$632CCD52-51A7-44F9-BF3E-60519AEF8695","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fe520b881e25fb4c4c8a205177018870f594e4e9","datavalue":{"value":{"entity-type":"item","numeric-id":5394197,"id":"Q5394197"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"23da8d805d66d33283b89de81445f7ce40c4a3e8","datavalue":{"value":{"amount":"+0.7063263058662415","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":"Q5741559$8063293B-5ED3-4E8B-9772-03637E87776D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b3af864a3489d6e87eacccff0728680b50e49627","datavalue":{"value":{"entity-type":"item","numeric-id":2908568,"id":"Q2908568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"769c292c14e4269145a412ad4ac6f72cb3a92cdf","datavalue":{"value":{"amount":"+0.6999050378799438","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":"Q5741559$71001534-17F0-4E50-B740-FEF2BDFC0E3D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5741559","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5741559"}}}}}