{"entities":{"Q3543642":{"pageid":5573546,"ns":120,"title":"Item:Q3543642","lastrevid":80854097,"modified":"2026-05-06T17:09:06Z","type":"item","id":"Q3543642","labels":{"en":{"language":"en","value":"Twenty Years of Theorem Proving for HOLs Past, Present and Future"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5378165"}},"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":"Q3543642$8D83C4B8-6228-4DDF-A7A7-05F4296F2A1F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"acc3cc07bb8670afed337fbd7eff49b7df373843","datavalue":{"value":{"text":"Twenty Years of Theorem Proving for HOLs Past, Present and Future","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3543642$3C09FD1C-50DE-4511-A45C-73FD43A24350","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"fc70458297e6d96754594a3b37eed4d6aec21361","datavalue":{"value":"1165.68459","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543642$66CC7015-A32C-44EF-8BE8-5A77D29AC34E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b356771951bf8a4750e0d43dc7514430d6fb4b60","datavalue":{"value":"10.1007/978-3-540-71067-7_1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543642$76AB217F-4040-4157-80FE-7027801BD91A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ae59b8d5f9d02ef4cf33abf637ff500edd878cc9","datavalue":{"value":{"entity-type":"item","numeric-id":1566865,"id":"Q1566865"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543642$1CF150E1-6D50-4C93-A73C-63393531EF06","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543642$CEC433C3-D552-440F-9CE1-5C75024D34F8","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9390341f6bd0adb4a80933997da5182af87828a8","datavalue":{"value":{"time":"+2008-12-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3543642$564B3821-BFA4-4A8F-AB92-A141F5D49A26","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543642$A05B550A-7191-4108-B26B-76412A80684F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"cb4e8adab438c1dab04758cc14f3a5f6511a34c6","datavalue":{"value":"5378165","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543642$7150DDAF-1FE9-44FE-97B2-1CA33441CD45","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543642$BC6C0CC4-3BED-4704-94CA-162D3444FB7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543642$CE77543E-9D24-470F-9D75-428E3CADA3EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8b2040a476017b43b21bd352cfec0a67d631d6d4","datavalue":{"value":{"entity-type":"item","numeric-id":18467,"id":"Q18467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543642$FEEBCEA3-986F-4C33-8FBE-D57222E42829","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543642$9833C54A-78C7-461D-B86E-ECE4B7186AB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27b6ae20da44d6f09b655d9481cc0df08a8ffcdf","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543642$F6B5CC32-5E91-4ECF-8AA5-9B5EC85C009C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543642$7DB38035-A4E3-442B-A22E-41B0F2A69A31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543642$E23BEE96-7CA7-4D09-BFBC-4ABF7528575D","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":"Q3543642$B3DAC6E3-7053-4124-960C-861C69D76A63","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fe08dfd1e23cd89bcd4e762ab1af66688eb4377b","datavalue":{"value":"https://doi.org/10.1007/978-3-540-71067-7_1","type":"string"},"datatype":"url"},"type":"statement","id":"Q3543642$B20CE987-BF6A-49E4-A73E-6D9529F696E3","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"66c379b00e00cd20ed6471c49786c649f4004c2c","datavalue":{"value":"W1606397589","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543642$8D8305F5-5D7C-4D1A-B9EF-0221A3A8A6D6","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"799a38e83bea9921db7a769536fd5def8b656e78","datavalue":{"value":{"entity-type":"item","numeric-id":1923825,"id":"Q1923825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d24ae4f4608c3783d8a6b8ef613b487b3bbe302c","datavalue":{"value":{"amount":"+0.8091228008270264","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":"Q3543642$AA5C52C6-E568-44E4-92CE-F95B1E8209E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9d8c676f8538b024eb2a80be0edde23296e2c1db","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9f1a3b93c3f690b706f568413d0f0f0dc56c77f8","datavalue":{"value":{"amount":"+0.8090988993644714","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":"Q3543642$966D8B0F-92B5-4C30-BAA2-E600909A6FF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6c21c4cd5d4993c28f29a090d2fcc426973edfae","datavalue":{"value":{"entity-type":"item","numeric-id":2280211,"id":"Q2280211"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"99665426fb216de20df0e0e506fcffca820b2ee3","datavalue":{"value":{"amount":"+0.8036302924156189","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":"Q3543642$AD3F18BB-AB63-4E18-B9E0-A44C20EF374A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cef7c286fb322135f98a489f42e729b7284efa24","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"475f15c38c5e44b5db5167680128449641ae8895","datavalue":{"value":{"amount":"+0.7746993899345398","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":"Q3543642$9F8FF8F1-002D-4147-8FB4-5D372FC22B71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7ba65f6a58ed08b60fa73248e76ff032f9c8be87","datavalue":{"value":{"entity-type":"item","numeric-id":2722041,"id":"Q2722041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"475f15c38c5e44b5db5167680128449641ae8895","datavalue":{"value":{"amount":"+0.7746993899345398","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":"Q3543642$03A19980-B0C0-4FCF-80D1-ED331B573144","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Twenty Years of Theorem Proving for HOLs Past, Present and Future","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Twenty_Years_of_Theorem_Proving_for_HOLs_Past,_Present_and_Future"}}}}}