{"entities":{"Q1799072":{"pageid":1809814,"ns":120,"title":"Item:Q1799072","lastrevid":42146444,"modified":"2025-05-26T12:52:08Z","type":"item","id":"Q1799072","labels":{"en":{"language":"en","value":"The higher-order prover Leo-III"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6958095"}},"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":"Q1799072$DD1E62BF-C4F0-4B6F-9B34-AFE08C3A1966","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"958640e558de82dedf9c554b9d465b59300ca6ae","datavalue":{"value":{"text":"The higher-order prover Leo-III","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1799072$9463D130-E6A1-4F5A-82E4-6DE548516EA3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"af01e3223a84776310dec4bffd8e0ff2a4460449","datavalue":{"value":"10.1007/978-3-319-94205-6_8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799072$C756F575-DF64-4FDF-9075-5B6B2152C9C4","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d804cf7e485bfddfeb0967f0a2ed09ee96e11180","datavalue":{"value":{"entity-type":"item","numeric-id":1799071,"id":"Q1799071"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799072$9EC2B955-280F-4F2A-A843-AA04FDB8051F","rank":"normal"},{"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":"Q1799072$BA4AA158-5B78-4314-BF6E-E879CFFDE452","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0172cdede3f306f1b36155a82f67164814fd11e5","datavalue":{"value":{"time":"+2018-10-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1799072$8870F970-D488-48F7-A948-0FA807E02FB0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"50c97b7b9ce81c6e6371d42d31cb90a68716c742","datavalue":{"value":"https://arxiv.org/abs/1802.02732","type":"string"},"datatype":"url"},"type":"statement","id":"Q1799072$2F8C55F7-B676-4BB7-96FE-5E72B7236231","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P205","hash":"20be05472bb442926b424452ef4a66bbd2c8f543","datavalue":{"value":"http://christoph-benzmueller.de/papers/C70.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q1799072$2CE50C20-5887-4647-B63D-8CB20D00B8FA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799072$D4C4284D-C9C9-477E-8307-138D1416B7F7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ba9cf1ecb5c9131db8460cb99a516fbd59d4f5f9","datavalue":{"value":"6958095","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799072$3CCB2D37-5DD0-4060-83CE-4D13D5088E89","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":"Q1799072$B22DD3C2-F80C-42DD-8AC0-18FE1A11533C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"491e4169c914222bc349264f15b36cbf2c3ef446","datavalue":{"value":{"entity-type":"item","numeric-id":18920,"id":"Q18920"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799072$5CEF059A-8808-4EDB-94DA-4A156B2734D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7a2e99bf2d721f734420e941cd08910602eca6fc","datavalue":{"value":{"entity-type":"item","numeric-id":23924,"id":"Q23924"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799072$3FF5C9BE-3058-40A4-A843-C24800445ADD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ad14f82278379093e75b5195fcd2d15cc85b252c","datavalue":{"value":{"entity-type":"item","numeric-id":25468,"id":"Q25468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799072$D39B4A96-EA7C-473F-987A-C4A34F41CEA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bec249a9f2158ac9024acac21e3dec3b5d305ee5","datavalue":{"value":{"entity-type":"item","numeric-id":29522,"id":"Q29522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799072$EA4F43FD-F2DB-4BE7-882B-5ED6422E4857","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":"Q1799072$42DA71D1-C998-4238-BC0B-63A6F1FD96BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"11457aba592a0d27712f8b8dca979adeee93d14f","datavalue":{"value":{"entity-type":"item","numeric-id":33329,"id":"Q33329"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799072$EC1D24EF-381F-46E9-8619-3CE4E46B0151","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d83b780839e730b0091759b62a50b0f768844ed7","datavalue":{"value":{"entity-type":"item","numeric-id":21894,"id":"Q21894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799072$242C7764-B7F1-434F-920E-E91FDA1B687D","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":"Q1799072$53734FFF-0196-47DE-AC7D-7D3D8733FEBF","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"887315a1060f86c732578764b220f1969b40db9f","datavalue":{"value":"W2886133399","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799072$32D109C4-71C5-4767-99DD-7E91A98656BF","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":"df9123eadb80da26e5089d0bfc21082becaddf5a","datavalue":{"value":{"amount":"+0.95912105","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1799072$482D95E2-106E-4AA3-AE85-33C61BDE5256","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fb697da6731caef5109d80b7ba8e021555045823","datavalue":{"value":{"entity-type":"item","numeric-id":3541699,"id":"Q3541699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d6653cc8a31f2d379226d3bfe6bd3d95e0dc0287","datavalue":{"value":{"amount":"+0.8757111","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1799072$F87B21DB-F504-426B-9258-F50C47316837","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ab06b27e0fec3c4518b2c6d579879748341c8fd9","datavalue":{"value":{"entity-type":"item","numeric-id":4557854,"id":"Q4557854"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"602d691a67f27278a7a24e7d0ae00688041091d0","datavalue":{"value":{"amount":"+0.86059153","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1799072$D95B7737-3D36-4F64-A697-7D54283C0C4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ee9691043fc2fa83f9bcad490e83cd2b178847bf","datavalue":{"value":{"entity-type":"item","numeric-id":1987736,"id":"Q1987736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"60656cbfa9b322f2f47d37b6f04153b052ab5359","datavalue":{"value":{"amount":"+0.85856134","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1799072$786E2A7E-5357-4E34-9CE2-F1FF4B9F3C84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5dba73bc93b36b44c3e17c0494079c469ef5e18a","datavalue":{"value":{"entity-type":"item","numeric-id":2996134,"id":"Q2996134"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"156da1deda6f2dd0e07852baf3af069351df11c3","datavalue":{"value":{"amount":"+0.8530765","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1799072$56A2DDA4-CD21-4055-BF3E-5E5462C2311E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8139328ea45d0f5f4bbb53ec8e07615b518a5b98","datavalue":{"value":{"entity-type":"item","numeric-id":3578399,"id":"Q3578399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"337313a6d01beabe6983a7244c52549c0114c922","datavalue":{"value":{"amount":"+0.8521729","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1799072$8C18D06C-4F65-456E-950E-66B375F2AD0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e0ec97b8481b3a0b1d3747ab1cfe1014f767440b","datavalue":{"value":{"entity-type":"item","numeric-id":4524794,"id":"Q4524794"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"293a00c0d35f9b4cf37ea46f71f6ba4b1e59d6d5","datavalue":{"value":{"amount":"+0.84559727","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1799072$921BADEE-3C04-4CBF-93BF-585ECC36A7A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3bd033c52f6d78c9dbd4fd32f239dc95922aeddc","datavalue":{"value":{"entity-type":"item","numeric-id":4305311,"id":"Q4305311"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"57f89722514577e6d12151176e046638f34f0036","datavalue":{"value":{"amount":"+0.8453967","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1799072$8C50CF5D-F286-456E-88D2-EBE2CF3B46CA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1799072","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1799072"}}}}}