{"entities":{"Q1404981":{"pageid":1415721,"ns":120,"title":"Item:Q1404981","lastrevid":67521942,"modified":"2026-04-12T18:34:28Z","type":"item","id":"Q1404981","labels":{"en":{"language":"en","value":"IeanCOP: lean connection-based theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1970574"}},"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":"Q1404981$F166D2BC-D93F-4F80-AB56-FD82D83D5CD4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2182458597a3b8d12fa07376a875c4401a820106","datavalue":{"value":{"text":"IeanCOP: lean connection-based theorem proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1404981$ACBDB9CC-250E-40CD-B4C0-8DA85798A939","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9a904a9bc6fde38c64c81d0c401c83f40784c9a5","datavalue":{"value":"1025.68076","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1404981$DEA4804F-38C2-4D7A-8331-7B1247F53BC0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c4298982e0f3a4600debce325bd968b1a8e26c9d","datavalue":{"value":"10.1016/S0747-7171(03)00037-3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1404981$22215902-7BA2-4BC8-A437-340390661814","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d2d00c1197e57bdc49c1c8779be1049cb4d10dbd","datavalue":{"value":{"entity-type":"item","numeric-id":877896,"id":"Q877896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$105DFDFD-AF7A-4F0F-B69C-704C9FB72556","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"244cbb0c7c29d260462be69c255a90e4965cd8bb","datavalue":{"value":{"entity-type":"item","numeric-id":287328,"id":"Q287328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$BC732A2B-8B2D-4A98-8777-B73C34410849","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ea72303f92787da89554ee5fa15621068821a762","datavalue":{"value":{"entity-type":"item","numeric-id":99061,"id":"Q99061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$9394AC11-4ECB-4C0E-9B30-E3646873DBBC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"988a1f1f38c2f749de54c12ebc5774f827c2b17e","datavalue":{"value":{"time":"+2003-08-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1404981$011F8CD7-718E-4B85-AA2E-87838D379DD9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1404981$10B14C94-8BC8-45C1-9823-59D8472AB887","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"67eff000dc99a5e43d2fb667dff617aac78a8a26","datavalue":{"value":"1970574","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1404981$D5CF04E5-8F16-45E4-B2CD-46F227E856E8","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ff67fedbe8c50d3daca036875aed531217cd953b","datavalue":{"value":"Prolog","type":"string"},"datatype":"string"},"type":"statement","id":"Q1404981$268D491C-5629-4F23-A242-38E02C696552","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8bf549142b710f01581b24fd28cbb67614316cd4","datavalue":{"value":"theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q1404981$803E9EE5-25A7-4E61-9526-D9C07547B3E0","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c845b927c7c8299e3e10848fbe9373f51ae3559b","datavalue":{"value":{"entity-type":"item","numeric-id":13461,"id":"Q13461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$DBFE607D-140A-40D0-90C9-F5AD1AE7BC71","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":"Q1404981$B12F5DE6-30FB-473F-B2F4-988D82C4F1B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bccd1d0bb2717360c541381c661e7bb40d86b318","datavalue":{"value":{"entity-type":"item","numeric-id":21962,"id":"Q21962"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$327F7E92-D560-4C5F-9505-6D36A0D63826","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b6f0aa77e475c4664199396d1dc04a1aa751a004","datavalue":{"value":{"entity-type":"item","numeric-id":23925,"id":"Q23925"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$CF289EF5-ECC2-4BA3-BAEB-E0996780E48D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f1ac18480cfc9c6929462301cac5fe5599af9444","datavalue":{"value":{"entity-type":"item","numeric-id":38058,"id":"Q38058"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$2AB5298B-CD24-4928-AE30-0AD316322A3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"daf1126f3bf58ae583160328d0dec0da3aedc25e","datavalue":{"value":{"entity-type":"item","numeric-id":40434,"id":"Q40434"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$547AB515-06E3-4120-8D7D-022B29F3C4D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1e7b4d238eeafa5b21b1ef85a0d6b8900bfdc422","datavalue":{"value":{"entity-type":"item","numeric-id":15442,"id":"Q15442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$F3FB64AB-B3C9-42C9-8ACD-F5FD4A63B8E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"70c51cb69cf83ba52d30c7a2c9abf4fc48a6f8a5","datavalue":{"value":{"entity-type":"item","numeric-id":18707,"id":"Q18707"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$85F3A1C5-D8FF-4C9A-A8B2-C3F5E8C4E1B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"497739b1d588e442d5b7ba6bb4cccae512fc3231","datavalue":{"value":{"entity-type":"item","numeric-id":19196,"id":"Q19196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$24030ABA-5774-479E-98FD-3E3EB5F2F8C9","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":"Q1404981$6B5B97DB-0522-4B87-9B10-22ACFCB73937","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4d51506a7596e8959151c2c9b9334a415c6932a8","datavalue":{"value":{"entity-type":"item","numeric-id":5210764,"id":"Q5210764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$E9D911D3-C6AE-4421-B513-4FAA6E43976D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe8901129bf6a7a6fa71fcab493125724abbb8f4","datavalue":{"value":{"entity-type":"item","numeric-id":4610317,"id":"Q4610317"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$6B30B094-8ED5-40B9-8CB2-E663396C145D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"43f9608b13e21870d0ea96a60dac80597e508d93","datavalue":{"value":{"entity-type":"item","numeric-id":1904400,"id":"Q1904400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$8E6A0793-655F-43B3-AF5D-2B7492A96706","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"850ca39a94aac87362042c94528de0b33c665341","datavalue":{"value":{"entity-type":"item","numeric-id":3668887,"id":"Q3668887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$074967AA-CC1A-4E4B-978D-EE36F93C40A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dbb4aa8dad638334a86cbf0de6c1439e4250b0ce","datavalue":{"value":{"entity-type":"item","numeric-id":4692618,"id":"Q4692618"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$C9F80FA5-BBE0-4D76-8081-B427808B5346","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ed083649962311e9cb36edd1af7a903443454ddc","datavalue":{"value":{"entity-type":"item","numeric-id":3833651,"id":"Q3833651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$9752D1E8-C9FC-4F05-BDF6-FFCC3386AE47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4259ba96907648c795d34036ee1d1e7daa76735","datavalue":{"value":{"entity-type":"item","numeric-id":5210812,"id":"Q5210812"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$88B9880D-4494-42AF-AC76-AC903CD3BD2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70200912b15e3f6d8f97f26c605e4ed0a53464e8","datavalue":{"value":{"entity-type":"item","numeric-id":3919057,"id":"Q3919057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$11CBFBA5-A58B-4EFE-AEEC-D21A51296922","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e74a7a357b1b46dc042b2194329594218f6b370","datavalue":{"value":{"entity-type":"item","numeric-id":1840142,"id":"Q1840142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$9C73F841-C735-465D-B13E-8118BDA9A9C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dffc16544718d83a4fdaaf484258616599c048b4","datavalue":{"value":{"entity-type":"item","numeric-id":4520768,"id":"Q4520768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$737EC4DC-ED5A-4AAB-85A9-A0D888146946","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"158bb2233935470152d2dc667c5dec4b7a43c81a","datavalue":{"value":{"entity-type":"item","numeric-id":1344875,"id":"Q1344875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$8BF02A30-AA6F-4459-B48D-72E695F4EBAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"07bde1b1ec996aeb071ba3c817fedaeed25122f5","datavalue":{"value":{"entity-type":"item","numeric-id":1189726,"id":"Q1189726"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$9FCF1AC3-EFCE-4DE9-8CDD-78E5149E19FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65f72fa731d5ef46f7c8727b7b59f2eaf22c3523","datavalue":{"value":{"entity-type":"item","numeric-id":5544307,"id":"Q5544307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$D497E13E-58C3-4377-9EF4-F4A88FA10063","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"442e3fa6ac35d64bb4bbe8f58a34e439aaaa3352","datavalue":{"value":{"entity-type":"item","numeric-id":4263017,"id":"Q4263017"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$2B008DC3-4C27-4C27-B3F5-1F223E74085E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c16bedf88d37c78219926e82b3d7a7a9dee66a31","datavalue":{"value":{"entity-type":"item","numeric-id":3821629,"id":"Q3821629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$AF3717AB-6917-4562-BF9F-C5B3C9371D17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"584b0a5f836e827cd0cf945b4c1a7db2631a4eea","datavalue":{"value":{"entity-type":"item","numeric-id":4610335,"id":"Q4610335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$B59ABC54-1E09-4D04-9FBD-BB3968F7C5F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"24c43ac445635282dee6e89db178fe88ba09f072","datavalue":{"value":{"entity-type":"item","numeric-id":4645241,"id":"Q4645241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$182D5E80-3BBA-4837-8783-F3EC4AEAFB30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d5587664e371fa7cdb52e3b1329f22cf9fcff022","datavalue":{"value":{"entity-type":"item","numeric-id":1101242,"id":"Q1101242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$3EE7C3DF-C6D7-4C82-AA6D-68CB58860164","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b4094e7f7f2ab505c350a295eaa8dccedd87c7e","datavalue":{"value":{"entity-type":"item","numeric-id":2753605,"id":"Q2753605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$A89B3D24-4E2D-490C-B08C-B4EA456BFE1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62113b852f82fecf9e34912decc495ba0abfaf0d","datavalue":{"value":{"entity-type":"item","numeric-id":2721215,"id":"Q2721215"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$71BE7F1D-9180-4366-B570-F30C10C717D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ab938ba3d2bb1de7d34dc0f9166735f59a48b21","datavalue":{"value":{"entity-type":"item","numeric-id":1114446,"id":"Q1114446"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$EFB9B8D3-0BC5-4750-8508-9B43574F8683","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e9808046a6f8fa62d1a453b12f211b7893e78bc6","datavalue":{"value":{"entity-type":"item","numeric-id":1199932,"id":"Q1199932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$27C6950D-856A-4055-8761-A81E08E55016","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c5b09e879fc9e6d166a18cb26ec583e2bf401aa","datavalue":{"value":{"entity-type":"item","numeric-id":1272614,"id":"Q1272614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404981$D7416665-99C5-4764-AA9B-66A755A38978","rank":"normal"}],"P1643":[{"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":"0625b3c9b2555e8255a62c83ff10b59a464c4781","datavalue":{"value":{"amount":"+0.8610786199569702","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":"Q1404981$5D893C1C-83AD-4217-80DD-B3A1ED62FEC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"546d9adf7e0eed11370eb8b4e06e8d4cf94fe5dc","datavalue":{"value":{"entity-type":"item","numeric-id":4539650,"id":"Q4539650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4225e7d2fbd4fa34ac1e1285b95e2189a55410a2","datavalue":{"value":{"amount":"+0.8214667439460754","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":"Q1404981$4052DF5C-1ADE-4A7C-B2E1-C79E6365B960","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7c998849da60ad4b2d93edd5732dd975d1ecd9fa","datavalue":{"value":{"entity-type":"item","numeric-id":5479281,"id":"Q5479281"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"166c3c75c5590677ebec0ca8955dea24d67e181b","datavalue":{"value":{"amount":"+0.8209300637245178","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":"Q1404981$21138D4E-1620-4572-9F92-E3CC04FEF216","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2dacbde12ba11a83e5f0b2e5b5eb4a7e3a0cfe3b","datavalue":{"value":{"entity-type":"item","numeric-id":3192198,"id":"Q3192198"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"681c43735d260c638d95c4364c4ca8fd721ad93b","datavalue":{"value":{"amount":"+0.792479932308197","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":"Q1404981$57245BC6-77A7-4FA0-864D-AF855B72DC77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c5fc5e20ca080feb7bd3755314bb2d0db94d1bc2","datavalue":{"value":{"entity-type":"item","numeric-id":4610335,"id":"Q4610335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7740ce44d64d0f03fad15dfacf3a503c7a27f604","datavalue":{"value":{"amount":"+0.790883481502533","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":"Q1404981$57C1DD1D-ABEB-4491-842D-363C4A826FCF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"IeanCOP: lean connection-based theorem proving","badges":[]}}}}}