{"entities":{"Q3541699":{"pageid":5571603,"ns":120,"title":"Item:Q3541699","lastrevid":80954444,"modified":"2026-05-06T17:22:57Z","type":"item","id":"Q3541699","labels":{"en":{"language":"en","value":"LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5374239"}},"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":"Q3541699$E9EFD770-5C86-4618-9EC9-C05B0E086182","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"596f2bfde84ba2e9a52567ad908fb74ac4947bac","datavalue":{"value":{"text":"LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3541699$A31C85ED-B9D1-49F8-B314-FA0C63FA25F0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ae8b4e51fc092f009abb496e7804c2a2ba7632a0","datavalue":{"value":"1165.68446","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3541699$C6FAB265-A96B-4A24-8185-D50EF634602A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8cdbf7f10019e382774f8723cc46436a2df65cfc","datavalue":{"value":"10.1007/978-3-540-71070-7_14","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3541699$BC22E167-FC88-4DE0-ADD5-870270D17B0E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a525f7cd8b191ac2b9090383b0dabde3689f4ff2","datavalue":{"value":{"entity-type":"item","numeric-id":287280,"id":"Q287280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$C65C89EA-2814-4D73-B998-BF29D98B61B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"68b7f3340a0a00e21a2a028d54af2e9ff7bcc35b","datavalue":{"value":{"entity-type":"item","numeric-id":287282,"id":"Q287282"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$E22C6F2F-2049-4486-94BE-EA9B2DDD8D46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ef16cf0ac7c5453ce39911865487b110cabbd361","datavalue":{"value":{"entity-type":"item","numeric-id":1037395,"id":"Q1037395"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$FCD8D05A-B99D-4589-AF8B-A8671761B3F0","rank":"normal"},{"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":"Q3541699$19F4F543-0161-49A4-9C13-B852F8536738","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3085facee3457e7f15d7356906b0165b8709b141","datavalue":{"value":{"entity-type":"item","numeric-id":2817907,"id":"Q2817907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$875499EA-2FE7-49D5-B4DD-1395E8F6F2B1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4a5749b126b021d85a2ebf6a8aa65ef57ba3c669","datavalue":{"value":{"time":"+2008-11-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3541699$DC693A2A-3B86-46A0-B41E-DE2A7F967DC1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3541699$93F75E0C-FEE8-46C6-AFF9-134477B92EC6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f67383ac38cf8f5f0f67136213785a3ab294852b","datavalue":{"value":"5374239","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3541699$D32EF72B-A0EC-4205-BB8D-BD8EA75606B2","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"8190f0b55beb7fb4c380e5f7d44c45e8edc763a8","datavalue":{"value":"Q56020733","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3541699$6083D116-9B71-4805-9AAD-CDC0995E8E37","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9c40cf9a35904f638a7cabef2bc178bad46391f7","datavalue":{"value":{"entity-type":"item","numeric-id":13717,"id":"Q13717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$2A0AE22D-D280-4A37-ADBE-09B1F0038B40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"73bf07fb0985efe0166024eb806e5cf2244671a5","datavalue":{"value":{"entity-type":"item","numeric-id":18489,"id":"Q18489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$D1D6C75F-4721-476D-BB94-F858922F155C","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":"Q3541699$F9C62B2B-EC9B-4C98-BAE4-B6728D90039C","rank":"normal"},{"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":"Q3541699$514B237D-DEDB-4434-B42F-09DEB9F7626E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1017108dce3983431546a14c274f65bc4aaae70b","datavalue":{"value":{"entity-type":"item","numeric-id":22154,"id":"Q22154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$69C11C14-0C75-4065-AA20-3BAA50A20D13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b443b776731e3bc75eb79b752e7ef8c4cee2d97a","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$8F134A3D-B82C-474F-B085-1BB087C27B49","rank":"normal"},{"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":"Q3541699$2A506B17-3537-41BC-B917-5B9A271D34FA","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":"Q3541699$9DE13370-5573-4340-8881-9C1CB15F6C21","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":"Q3541699$6DA70D26-74F2-4C47-8E3B-AFB47EC4541F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2c1f1b0d192f3285ad8bae5169a9ecc2f6a94baf","datavalue":{"value":"https://doi.org/10.1007/978-3-540-71070-7_14","type":"string"},"datatype":"url"},"type":"statement","id":"Q3541699$1850A169-3071-4A83-AADC-4C10FC84E2D0","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f5a50b883f1579630d8e7172ba24e06189cb650d","datavalue":{"value":"W1955821421","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3541699$FE8C9607-F434-4427-93F7-A70D22074631","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"16ba4c761d0afd2b68b331890cbe715eaa366ee6","datavalue":{"value":{"entity-type":"item","numeric-id":865629,"id":"Q865629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$C9D6E77E-1137-461C-9D57-F5E35A3C3FE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9f4ec34970699a60fee9b67f04e9456c847a6819","datavalue":{"value":{"entity-type":"item","numeric-id":861715,"id":"Q861715"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$1869E548-7AD0-45C9-B62B-1B9695BD562A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4adc22ed174f33297ffa675f67b5ee27a98ff71c","datavalue":{"value":{"entity-type":"item","numeric-id":3541699,"id":"Q3541699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$4FD11583-60FD-40C5-964B-12AF198DCF92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"698a1c70562d11d060e1b869bd175ba19e1e7c3d","datavalue":{"value":{"entity-type":"item","numeric-id":3541725,"id":"Q3541725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$BF783541-B49B-4BDA-9716-2CC5EE66609D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d5ea882d37bc8b25208b41167eaea5742ca9b7a6","datavalue":{"value":{"entity-type":"item","numeric-id":4797443,"id":"Q4797443"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$F524CE11-E179-4C70-9F0F-AB1D5B955029","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3526b6dc59fcce39025ddb78a0186693039ed731","datavalue":{"value":{"entity-type":"item","numeric-id":946572,"id":"Q946572"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$76A4889F-5357-4171-ABAB-5D09827DB1D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb436ab2eeeb524568a9b987facbb81b25a59620","datavalue":{"value":{"entity-type":"item","numeric-id":4809075,"id":"Q4809075"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$5F65EB89-EDF9-432A-91E7-94A7E0FFD0C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70d5dcacdf82491509f047ffa7adf630e71ade90","datavalue":{"value":{"entity-type":"item","numeric-id":5667469,"id":"Q5667469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$59E2FA3A-6845-4D61-A749-9CD4BFC857BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$DD89B962-D212-48A0-BA68-B3F495DD1825","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1fa8e099c59f8b6819b5b09b786ac872f2d64b8","datavalue":{"value":{"entity-type":"item","numeric-id":688554,"id":"Q688554"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$4B6E2E10-7383-4EF1-AF67-45FDB09FE6B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8cff8a314d9fb157a7d13b3fe1123cbf96f16e53","datavalue":{"value":{"entity-type":"item","numeric-id":4539610,"id":"Q4539610"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$CE882AC4-6178-4373-AD9F-11D0AA3CE8DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$05DC6A28-97D8-4B10-A04A-6F8F673FECEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f306d53ffaa3316872c03d5120ded3df09d397f","datavalue":{"value":{"entity-type":"item","numeric-id":5191491,"id":"Q5191491"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$DC47E71D-B8F3-42D1-8456-EC347D5C36FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0cb051a6b1eb9b88364c46513701492fc0e99189","datavalue":{"value":{"entity-type":"item","numeric-id":3150300,"id":"Q3150300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$091A7975-58E3-4F3D-BD4F-EFEB749B56BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93fc8985b7898988b7d52edb5c0cd61c1b917df6","datavalue":{"value":{"entity-type":"item","numeric-id":3150301,"id":"Q3150301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$5B2F38F0-541D-4C68-801A-977D4B41DFF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"be986acc9e1b8514990926935f126389f1f796f9","datavalue":{"value":{"entity-type":"item","numeric-id":865650,"id":"Q865650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$73223B48-C5CC-4245-B32D-B790911C3E5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f49bddd3d8758939d2c56cea336fa15d4d01af13","datavalue":{"value":{"entity-type":"item","numeric-id":4809064,"id":"Q4809064"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3541699$EC993363-57D8-40BD-8E99-154EE426640B","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"132d130602658447cb9dfd9a99fd5540517bd0dc","datavalue":{"value":"conf/cade/BenzmullerPTF08","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3541699$ADF171A3-D0BA-4B5E-AE3B-91A256DAAE7E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e2a77260c5c813d21764d59a1fec5766803eafe5","datavalue":{"value":{"entity-type":"item","numeric-id":287283,"id":"Q287283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a3fadff234b3fa502170ac6fd25449d065f85b17","datavalue":{"value":{"amount":"+0.9241126179695128","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":"Q3541699$EA7123C5-63CF-4767-916F-34524CE97C47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"496052fc3273e7e47cd8686294fee309f85ea3be","datavalue":{"value":{"entity-type":"item","numeric-id":1799072,"id":"Q1799072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"57b08928837d3f10c14d57a02237c9ae93b0f3a8","datavalue":{"value":{"amount":"+0.8179736733436584","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":"Q3541699$C84AC218-B20C-4BC4-9535-D5D4D6ADAC59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e5071410fb4f588702a1cd4f98b5757b9c9f99e5","datavalue":{"value":{"entity-type":"item","numeric-id":2666959,"id":"Q2666959"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fdbbc462ecefe46fc47cc7cfcbb1a3fa74e850c7","datavalue":{"value":{"amount":"+0.8092454671859741","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":"Q3541699$C2313423-2AAC-4FFE-9C08-8EF0D553E856","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0c601f4f623fbf5cc4d0350b613400bfc77126ce","datavalue":{"value":{"entity-type":"item","numeric-id":3541708,"id":"Q3541708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"517625c953a1bb87f832bde58c5f8e5fe6bb91be","datavalue":{"value":{"amount":"+0.7754347324371338","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":"Q3541699$16873596-E640-4B1F-979E-F36FBB312F8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f30f1d8f9b1d127514f6c20dec24f6e39fa58c46","datavalue":{"value":{"entity-type":"item","numeric-id":1948289,"id":"Q1948289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"045a4a01e7eff8846c85c4cf377f33afbce7bc27","datavalue":{"value":{"amount":"+0.7575364112854004","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":"Q3541699$2C4E0D25-AD87-46F4-B9D3-674AA10155B8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)","badges":[]}}}}}