{"entities":{"Q2817300":{"pageid":2828038,"ns":120,"title":"Item:Q2817300","lastrevid":79428416,"modified":"2026-05-06T13:53:11Z","type":"item","id":"Q2817300","labels":{"en":{"language":"en","value":"Extending E prover with similarity based clause selection strategies"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6620493"}},"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":"Q2817300$5C5C2274-AA21-48A3-92C1-FD61EEE8DF7B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"df741052eebabd4cf2dd162dd3b8f37f320b7fc9","datavalue":{"value":{"text":"Extending E Prover with Similarity Based Clause Selection Strategies","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2817300$2545BDE8-D35B-4C2F-9B48-3AE5D1CD4927","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e63d59907d9e5ecf5708d02e6b9419b9da9d56ec","datavalue":{"value":"1347.68303","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817300$8441ACB1-12DB-49B7-A989-36E5E7A52C90","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4b1d0c1b6d4dd2a91b170656a7f3e7bdb748f1f8","datavalue":{"value":"10.1007/978-3-319-42547-4_11","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817300$C95F0B2E-747E-434B-B303-E34CF95B49D3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"87dc4de4518b8db4a5efca79e388ac462c23bd10","datavalue":{"value":{"entity-type":"item","numeric-id":831935,"id":"Q831935"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817300$27D8D76A-D335-43BE-87F8-1D0E9AC28FDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dc204e2e78d924e815f2b640ec35c8c2356ad41f","datavalue":{"value":{"entity-type":"item","numeric-id":286786,"id":"Q286786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817300$8EB67306-D330-4330-9F9D-8631F5D4CB1F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817300$6498DA34-A7D8-40BB-A655-9B2913B66F50","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"85d9f70abb070df81833000bc59244d6fec26f1f","datavalue":{"value":{"time":"+2016-08-30T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2817300$5B92C47D-06AF-4C06-A8A1-6549230BA20E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5e5bfd50eda1a8f6c5d6a57b268dc902adcad865","datavalue":{"value":"https://arxiv.org/abs/1606.03888","type":"string"},"datatype":"url"},"type":"statement","id":"Q2817300$CCBBFA3B-BC53-4486-BC13-38C87A5773D2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817300$BE55AA97-1865-4A52-B85D-82E9B4B72DE9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6d37323f109a8b71301ae44b9755c7d58794bd0b","datavalue":{"value":"6620493","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817300$438E60D9-D638-4A6F-80F7-ECE6572D150A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2817300$C4941BA9-761E-4603-B9FC-5A4F09190ADF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5db6451c9835b7bd65aa9274ead86a0d9a55ee0d","datavalue":{"value":"large theory reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q2817300$C1592B81-E6B2-4169-B094-2BCD17F51F67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"05a8f9ec83e26a19d4d6048f4bacb97d662c90ba","datavalue":{"value":"clause selection","type":"string"},"datatype":"string"},"type":"statement","id":"Q2817300$F189DEDF-6881-43BC-B205-6B181A7950E9","rank":"normal"}],"P1463":[{"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":"Q2817300$07726B76-EA3F-419C-A26C-835F8D0963C4","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":"Q2817300$D3B56363-5ADE-4FA8-94BD-0E8587ABD40F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"30c23680895c6c05b43b4be92074136c496750ec","datavalue":{"value":{"entity-type":"item","numeric-id":28682,"id":"Q28682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817300$B990291B-5F3F-4A85-80BF-4F3F1A271160","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":"Q2817300$5C6D494E-BD3B-4908-9DDB-73EB8F8C7E0A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"60ca6daa673c391c5f1aaf28929249155111c4c6","datavalue":{"value":"W2438025153","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817300$A36DAE50-BA88-448C-9B3C-C1EB9887FAFC","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"f60fbed1ceb9b0323ab1151fa7422484629814d8","datavalue":{"value":"Q62044871","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817300$F0783C38-3579-41EE-A06E-F8AAC36C3B1F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"29b0802dd9ffb89108bee25aa26120dffc46ad60","datavalue":{"value":{"entity-type":"item","numeric-id":2352489,"id":"Q2352489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817300$392B312C-6423-4339-9380-7BA277A898A0","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":"Q2817300$45EF1675-DC74-4913-AF2C-E62D2CA52E63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e9af2f72684ec7589c1f4c3f09ffb0ae40e708ba","datavalue":{"value":{"entity-type":"item","numeric-id":3034830,"id":"Q3034830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817300$716520A5-16BC-4408-B298-EB382B86E645","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"dbe0bd874e8e3dccc5794da84b2df2753f4a5cfd","datavalue":{"value":"conf/mkm/JakubuvU16","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817300$9D6E5D67-8079-444E-A294-C6C462E98472","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2b065cdf9ee5815d7aba3bc448dd3137c103308e","datavalue":{"value":{"entity-type":"item","numeric-id":2870167,"id":"Q2870167"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4942ad76fadb4c33cf011f3add15552e55d7ef7a","datavalue":{"value":{"amount":"+0.8043698668479919","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":"Q2817300$69B2EC60-A6A8-40A5-A3F8-FAD01E677620","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec8522d2416898af206aef854d5fb2e109849c1a","datavalue":{"value":{"entity-type":"item","numeric-id":3150301,"id":"Q3150301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4286878554f44167cda9ea763b54155a9daecbe0","datavalue":{"value":{"amount":"+0.789953351020813","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":"Q2817300$C8422ECF-E15F-4592-873D-01B7B40F1E43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8e6ca25e782efc69d84ec6f429f6411d8ceba52a","datavalue":{"value":{"entity-type":"item","numeric-id":2817931,"id":"Q2817931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c13929a6b51fcdc7c6653271af774568612970c4","datavalue":{"value":{"amount":"+0.7880201935768127","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":"Q2817300$9AE524FF-DD8F-4B66-A3E8-92D6A753A17A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ca094adf73b2db58c56421e97dacaae30aeb0afc","datavalue":{"value":{"entity-type":"item","numeric-id":4539621,"id":"Q4539621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"151c121b7561f504fd362d53eecf506b3de3b2f9","datavalue":{"value":{"amount":"+0.772702693939209","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":"Q2817300$FC05E046-12F4-4206-A847-EDA740884715","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f43e7969c109a38e6139d16e770409e6632533fc","datavalue":{"value":{"entity-type":"item","numeric-id":2817933,"id":"Q2817933"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9fa546349740a6e6e0dd013811c9d5b8105a2e03","datavalue":{"value":{"amount":"+0.7668841481208801","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":"Q2817300$61EF63DB-82F5-4774-985F-ABCCDBDEC40D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Extending E prover with similarity based clause selection strategies","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Extending_E_prover_with_similarity_based_clause_selection_strategies"}}}}}