{"entities":{"Q3696549":{"pageid":5726455,"ns":120,"title":"Item:Q3696549","lastrevid":50347298,"modified":"2026-01-13T21:04:47Z","type":"item","id":"Q3696549","labels":{"en":{"language":"en","value":"Lessons learned from LCF: A Survey of Natural Deduction Proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3922015"}},"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":"Q3696549$27900804-8E91-4A19-B9AC-B02EEC683FD3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"baf9586274033c387080d608c2381ecddc8ce755","datavalue":{"value":{"text":"Lessons learned from LCF: A Survey of Natural Deduction Proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3696549$BF30476B-A73E-4FAD-BE16-D14F22162533","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"250616caefa6afe46af564fb953bea704b8fb270","datavalue":{"value":"0576.68070","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3696549$0901410B-15A2-44ED-90B9-27C842103F6F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ba9f0a801691b290ffcb9a042b4379a6a2cb49b3","datavalue":{"value":{"entity-type":"item","numeric-id":83484,"id":"Q83484"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3696549$41799428-BCAF-4EC5-8D44-10290B3B36FF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3c94df5c9af0ede578c52141befd29044de13172","datavalue":{"value":{"time":"+1985-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3696549$FF18C19A-4E5C-45B7-A5FD-303560C71499","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3696549$FA928FE2-8731-4E42-9300-970F982B2456","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3696549$0A1E1A57-AD59-4806-911D-BD5E7E8A7977","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1e903e68a16880f66ed79a0863889f1b2d3c837c","datavalue":{"value":"94C10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3696549$4A8F0F67-7A92-4FE9-9963-B8916288065F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b3166a809d4b74813c49f274fdfbe6fe5d95daa5","datavalue":{"value":"3922015","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3696549$BE6BABF1-B681-4914-9A91-8BF254A11748","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q3696549$1DD92697-434F-43F6-BBBF-6988C333781C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"94691655736ed2309ddb42ec3b3fcd5b5fb1dbb6","datavalue":{"value":"verification of hardware and software","type":"string"},"datatype":"string"},"type":"statement","id":"Q3696549$B540E436-E9BD-4FFD-AE50-11CB4BCF8099","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb5dfbdfa6d8a2070a67ff948fb8abd387eda36e","datavalue":{"value":{"entity-type":"item","numeric-id":352969,"id":"Q352969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3696549$C08019F3-38C2-4260-947A-3AF5B497527F","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":"Q3696549$88AAC40E-88F1-4036-B19E-A34F19709454","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8fad24938c0b56394579e59996def62b72bd823a","datavalue":{"value":"https://doi.org/10.1093/comjnl/28.5.474","type":"string"},"datatype":"url"},"type":"statement","id":"Q3696549$4BE73D25-2EDA-4F4E-8D1B-D1AB49B6E831","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"067a54c064330e8e534f2c5dc8f719a4b93c0117","datavalue":{"value":"W1991293669","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3696549$05D1D85A-3D2B-47AB-881F-787C411F5590","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"937c89ae1ec8cac0b2bf7030d801681a11c8ffad","datavalue":{"value":"10.1093/COMJNL/28.5.474","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3696549$43D5AEB6-CFA2-4825-A766-8C1B3981709E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"173aee9d2a48e7f455741b1c3b087943876bf963","datavalue":{"value":{"entity-type":"item","numeric-id":1060023,"id":"Q1060023"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e1682729e86d134cb67c383dca5a9589bbe49b99","datavalue":{"value":{"amount":"+0.7753334045410156","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":"Q3696549$6E232D63-98FD-44F3-8924-C0DFDCFD307C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"97650e096cd8fc874b01c43330063955389b285b","datavalue":{"value":{"entity-type":"item","numeric-id":4720797,"id":"Q4720797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4923686f71088cece1efc37c449f8b921f4ead7a","datavalue":{"value":{"amount":"+0.7748836278915405","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":"Q3696549$0114443A-B33E-4F0F-9C1E-331B69C83423","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dcd3b89e7c056e5c3efae55cd77c3c34ddfa4c74","datavalue":{"value":{"entity-type":"item","numeric-id":879370,"id":"Q879370"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6a1a3f8744017398f01e61c997e13119f624dd29","datavalue":{"value":{"amount":"+0.7704699635505676","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":"Q3696549$4EA4CF6C-8FBC-4A8C-87E6-13CD20C72AE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2565d9e77d9b51b905daa5bfbb63ce859f62d93b","datavalue":{"value":{"entity-type":"item","numeric-id":3345811,"id":"Q3345811"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0d174b6263ab5a213311b2904a34f9bd9a8fca4d","datavalue":{"value":{"amount":"+0.7596826553344727","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":"Q3696549$5ADF81AE-9CEF-48B8-8A29-65B909A9B855","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":"06fdb3ea2939a17c85f9aed607b9627d1c2d4de9","datavalue":{"value":{"amount":"+0.7559593915939331","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":"Q3696549$3EC7BDD9-55F1-48C1-AE82-A60A8F51AEB2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3696549","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3696549"}}}}}