{"entities":{"Q5747761":{"pageid":7777312,"ns":120,"title":"Item:Q5747761","lastrevid":97044782,"modified":"2026-06-05T13:06:55Z","type":"item","id":"Q5747761","labels":{"en":{"language":"en","value":"iProver-Eq: An Instantiation-Based Theorem Prover with Equality"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5785448"}},"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":"Q5747761$0069A55E-9BCD-46C5-85FD-8AC60B4D79D1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5f2147464ada23392057f79f65aff7984e3890a9","datavalue":{"value":{"text":"iProver-Eq: An Instantiation-Based Theorem Prover with Equality","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5747761$ED5DE1F3-AE17-4156-9559-8069462F9349","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"bef533139cc31953336a7bf0e7dd295067d2de99","datavalue":{"value":"1291.68354","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747761$9E935AC8-91EF-40DF-923B-85B1E1C92DE6","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d840f11148370e09183a32d6f551600a280e130d","datavalue":{"value":"10.1007/978-3-642-14203-1_17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747761$B72988C1-516A-4265-AE5F-CCF817ECD4DF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ce9e1735095a7237c0c699c31f4c0eb57566d709","datavalue":{"value":{"entity-type":"item","numeric-id":1401931,"id":"Q1401931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747761$9ECA97EB-1CAC-4318-9CF5-40C9418D21CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"789b4861f65a07830a1cc39e2d392c6f0d54926c","datavalue":{"value":{"entity-type":"item","numeric-id":2908492,"id":"Q2908492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747761$76788EDA-652D-4A49-8BA3-6AB7FE7B4781","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":"Q5747761$12ED3AE9-D2AE-4362-9866-DC2468DD6E6C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5f7d3744053f89b932df935693d4d726597e5f91","datavalue":{"value":{"time":"+2010-09-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5747761$EC77EE56-1777-4D84-8002-046F2309A571","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747761$8E508513-0D9A-4C42-AB5C-C8B0759E3022","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a90d49730d8247ed8bf92369e93dbb2a0df4a270","datavalue":{"value":"5785448","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747761$E34294A5-02E4-40C6-9790-A4C9D4AE4B5F","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4a2b5b60cbb02303c49de211ce0cda9c94098741","datavalue":{"value":{"entity-type":"item","numeric-id":21435,"id":"Q21435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747761$1AA41006-B7EF-4CB9-A4FF-A67D35D24C77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747761$BB4B96AA-D192-4438-BA0C-1339916A6B2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6d1b503d7c8f19634e207574177819c306621855","datavalue":{"value":{"entity-type":"item","numeric-id":17038,"id":"Q17038"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747761$793B1643-F80B-4713-A4E7-F55D507284A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"83e2dec25ea583652d0e07d4393a843812f4b48b","datavalue":{"value":{"entity-type":"item","numeric-id":21686,"id":"Q21686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747761$EB70C5A5-72EC-48C9-97BD-E0795B7DB3D5","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":"Q5747761$99C8C7C2-3F38-4051-BA84-752DBF998A0E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"58417006de5c3fe1c3bfb74e18b5e8611ccf68d1","datavalue":{"value":"https://doi.org/10.1007/978-3-642-14203-1_17","type":"string"},"datatype":"url"},"type":"statement","id":"Q5747761$DCAB3EA5-63A6-4CB2-AF6A-6E50315704B0","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"14e32bb397470349c78b8f0534216da309bf856a","datavalue":{"value":"W1520118813","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747761$85F51B51-6A72-4810-A021-3D2A7DDB0349","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"22485e2e7f5d751287059d6c89f8749b6a408a20","datavalue":{"value":{"entity-type":"item","numeric-id":5325885,"id":"Q5325885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747761$2BF3A519-452B-42EB-B18B-91BE4A885499","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae611ccf26d614d6f5569c32d95f83372cdd7983","datavalue":{"value":{"entity-type":"item","numeric-id":5311286,"id":"Q5311286"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747761$023044B1-DB5F-4840-BF2D-D73C6B706642","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"33890b7faad584193275d91a4cd4d3b147aff5a7","datavalue":{"value":{"entity-type":"item","numeric-id":3541709,"id":"Q3541709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747761$4DB467EA-B8C3-41AA-9CCC-2B0F422BF576","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5fa5821d5bc9687fe29222b473d9339797d836dc","datavalue":{"value":{"entity-type":"item","numeric-id":5311286,"id":"Q5311286"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ae19c41eb5080681620f47d9520ca6809de9649e","datavalue":{"value":{"amount":"+0.9197621","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":"Q5747761$18D5CBCF-9198-4E20-9D3F-26597A626F5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"792336ff1c3b24bda0a585498d74b554cb5ee6b1","datavalue":{"value":{"entity-type":"item","numeric-id":5864202,"id":"Q5864202"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"08c5785e4e5df611737395c493d173d79a4b15da","datavalue":{"value":{"amount":"+0.89544773","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":"Q5747761$AF874F71-57EA-4837-BA87-36464E3D74CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6f85415bc5243ca4fb021999aff0a144e42ebf84","datavalue":{"value":{"entity-type":"item","numeric-id":3541709,"id":"Q3541709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2390ee4c892ae75caae09b018aca9b9ec6ead4ab","datavalue":{"value":{"amount":"+0.8949138","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":"Q5747761$5FCC982F-9D64-4BE0-89DD-78D6DFE3012C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4baa166647374ce26227c8ae876aaeeb41de44f6","datavalue":{"value":{"entity-type":"item","numeric-id":789177,"id":"Q789177"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dd72b9e56e4c95a0119de37ba36798910464b8d7","datavalue":{"value":{"amount":"+0.87729585","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":"Q5747761$B80E3116-2492-4B0B-B77C-459EF297D878","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ca2c4238698ff483e43a9533614b7db7f49ea887","datavalue":{"value":{"entity-type":"item","numeric-id":2968159,"id":"Q2968159"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"76b568e878116315dec9d49d56931b3a312571a6","datavalue":{"value":{"amount":"+0.8770424","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":"Q5747761$A73DAF46-2095-4B8E-AD69-9BCC895CA125","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4a6e11e44a187b6a2af9f163bed6b8c21e03faba","datavalue":{"value":{"entity-type":"item","numeric-id":4518412,"id":"Q4518412"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c0c7c8b5a114054e06e54bded275e2d2efc795c1","datavalue":{"value":{"amount":"+0.8754589","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":"Q5747761$39D0B458-08C3-46A7-8C74-E1830BEB5757","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4564dcbe209d24a2f509e63518773f769d6b6c9e","datavalue":{"value":{"entity-type":"item","numeric-id":4524792,"id":"Q4524792"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7e46ed8678341136285a2c10de99b86b87daf0c9","datavalue":{"value":{"amount":"+0.87382734","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":"Q5747761$B697B1B3-D872-4019-9870-3780126F7363","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"80ca538f9a91f5be72cb599d2b7a970193505baa","datavalue":{"value":{"entity-type":"item","numeric-id":4447245,"id":"Q4447245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7b6d3bfba5e480c31a673212b27a9a827d07c3d3","datavalue":{"value":{"amount":"+0.8738069","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":"Q5747761$BDC668FB-FDFC-4CF3-9F29-21AF11A870B5","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":"14a329d63f99a1c5c14de1c19723b880a24f57bd","datavalue":{"value":{"amount":"+0.8737079","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":"Q5747761$846E3A4A-3A6A-4D78-BB90-3F71286CD68F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"833e8e0f00263c5abbcbe67732c6e2af666995f7","datavalue":{"value":{"entity-type":"item","numeric-id":4302815,"id":"Q4302815"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7537ab2a6e5d57f8fba07c171f601812e36dd4a8","datavalue":{"value":{"amount":"+0.8687957","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":"Q5747761$91EB5F9E-5D79-49D1-9BFF-852BD46398C2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"IProver-Eq: An Instantiation-Based Theorem Prover with Equality","badges":[]}}}}}