{"entities":{"Q4835513":{"pageid":6865093,"ns":120,"title":"Item:Q4835513","lastrevid":41086123,"modified":"2025-04-18T05:07:34Z","type":"item","id":"Q4835513","labels":{"en":{"language":"en","value":"Increasing the efficiency of automated theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 761093"}},"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":"Q4835513$E7443E02-A96E-43A9-935A-74443E6F6BFA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"36c9a3ee434831aac65d9e7366b0baf5ad2e87fe","datavalue":{"value":{"text":"Increasing the efficiency of automated theorem proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4835513$33E09B8A-3E71-400C-BD0D-C05D234047D1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"22124e2368d42ec2e82cd4660631491955b50d32","datavalue":{"value":"0827.68100","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4835513$04B7CAE1-EFA8-47BA-82B6-C48F71700D25","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9fa84c15995271af28b9421eef066518f165555b","datavalue":{"value":"10.1080/11663081.1995.10510841","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4835513$FF380920-1171-4A59-9F7B-46C24EE7BD89","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"92adb13e09b5aab7763bdddfde64b12a08209166","datavalue":{"value":{"entity-type":"item","numeric-id":236749,"id":"Q236749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4835513$CCAD0438-E9AD-4AAB-B3D0-AE7453C58CA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cd19067cbec995ef7149bbe9b912062e617be2bf","datavalue":{"value":{"entity-type":"item","numeric-id":1346221,"id":"Q1346221"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4835513$B12C4669-2FA9-4104-A1C4-910609ADA1FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7d4bccdf7c2b388b6e3e888805bc1f0030b29c7b","datavalue":{"value":{"entity-type":"item","numeric-id":1403341,"id":"Q1403341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4835513$105F5081-2885-45AA-8983-6855B90D7DF8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"932edb623e9fc48fa0c14766bb48b251dc113bb4","datavalue":{"value":{"entity-type":"item","numeric-id":2901187,"id":"Q2901187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4835513$D1080B23-593E-4036-9A18-115876BBCDB9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d2c5a0478135439b51e1336eb30896ff68f823dd","datavalue":{"value":{"time":"+1995-12-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4835513$EEECD11F-3CD8-4EF4-8987-B5C3DBD8022D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4835513$78CE424A-C2ED-46BA-9379-18563A841532","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4835513$A4B67D7B-F83F-4879-881D-EA42106EE1A3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a63b94a62a0fe2cbdaec812ebd7911e0548f0ae5","datavalue":{"value":"761093","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4835513$F9E4E8DF-58B1-4CF8-9FD3-A70DF148B813","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5fbe3c7285c82b7e85a0384689c42c38ba7418e4","datavalue":{"value":"automated theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q4835513$84999629-1C7D-4B36-947B-ED4E69E3E1D3","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c271564990b51b3fdbf68356ca04e9947a77eba1","datavalue":{"value":{"entity-type":"item","numeric-id":17051,"id":"Q17051"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4835513$355B47F6-1AED-4E4E-A4A2-616C3C68ECBC","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":"Q4835513$292738E2-C74C-4850-834B-38AFDA8C9D43","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b3caca14c208ad0ad32cdc236d22bdf4e3da84bd","datavalue":{"value":"https://doi.org/10.1080/11663081.1995.10510841","type":"string"},"datatype":"url"},"type":"statement","id":"Q4835513$BFFA6225-A069-4AE0-92ED-7301AA2673BE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1481f903a0a6975e7778c80f65d6804431c8e147","datavalue":{"value":"W2103879019","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4835513$8339529E-6BD8-4A9E-B5E2-8F6268F9E20C","rank":"normal"}],"P223":[{"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":"Q4835513$8FE87F66-3A47-4142-BB83-96EA19D2E38F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77f70484bd2d56db595fa191ad0d54a382774ee3","datavalue":{"value":{"entity-type":"item","numeric-id":3335722,"id":"Q3335722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4835513$E40602F8-AEB7-4068-BBFB-BC3088E98F1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8bf1eb0085816c68ff7078182501fe6b0337105","datavalue":{"value":{"entity-type":"item","numeric-id":3743300,"id":"Q3743300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4835513$F036FD19-8200-471A-82ED-BD9AB5E872E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec6ea36d95d0179a7b0ad8ca8835fd68a540dc34","datavalue":{"value":{"entity-type":"item","numeric-id":1208722,"id":"Q1208722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4835513$7A5874D6-6262-4DC7-9AC3-5BACB3E4720D","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":"Q4835513$409D386F-02FE-4137-AAD0-88C6D6AEF922","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eba87f647d350da9410e3009029b609261e32924","datavalue":{"value":{"entity-type":"item","numeric-id":5797033,"id":"Q5797033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4835513$E8E33F83-2BB4-4964-AF97-91333CD8503E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"febba330446bda559f2952d624c63d67c91597ef","datavalue":{"value":{"entity-type":"item","numeric-id":5560258,"id":"Q5560258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4835513$2DCE5C5E-73CF-43EF-881B-D31B314BFE9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"079d26960fbad67a47fb78241cb8cbf2b682033c","datavalue":{"value":{"entity-type":"item","numeric-id":3999539,"id":"Q3999539"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4835513$2694E995-F0D9-449F-AC8A-DD4BCDF0C1BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d9c3982efd0f7ccc059068ad9e9a439bba5bf60","datavalue":{"value":{"entity-type":"item","numeric-id":3949989,"id":"Q3949989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4835513$05F25251-1B67-47B9-82C7-93DB834309C5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b73f67e85a8f6fae8d616525462a58624976e801","datavalue":{"value":{"entity-type":"item","numeric-id":3750137,"id":"Q3750137"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"33853d1827dcd7d366540c5d07cae1acb3fa9083","datavalue":{"value":{"amount":"+0.92768574","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":"Q4835513$6E8C75F3-D7CD-4397-9F02-5E9522191608","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a2cb6bb34055bd7687681718ca2c7bf00c0ca64f","datavalue":{"value":{"entity-type":"item","numeric-id":1057850,"id":"Q1057850"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a3db2224525879867d8c63c2e2b21695701421bc","datavalue":{"value":{"amount":"+0.91167194","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":"Q4835513$A13B7B39-B866-4979-82B9-7A8FC3C2BFE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dcbb17b5eeff24acc0ae046b77968c0618c1cbba","datavalue":{"value":{"entity-type":"item","numeric-id":5204800,"id":"Q5204800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4f19b7f7e841856c9b81be9d3191536769bbef71","datavalue":{"value":{"amount":"+0.908339","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":"Q4835513$0B0DBDC4-C22D-4B2E-91A9-8B8F314D8072","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cfc908b5a67bc17bd2b3b9d7e3d3d9681aac12d3","datavalue":{"value":{"entity-type":"item","numeric-id":3781734,"id":"Q3781734"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f6c0f4587949e0d1bbcf3289b4161caf0db6c8e0","datavalue":{"value":{"amount":"+0.9043423","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":"Q4835513$5792CBBE-356B-4189-A346-DCC7CD990117","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7c7bdb8bd55bdeddb7b2aca0d1ffe3ace97771ed","datavalue":{"value":{"entity-type":"item","numeric-id":5443571,"id":"Q5443571"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b1a594dfd91699d3a52941093ea374e199f10736","datavalue":{"value":{"amount":"+0.90397084","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":"Q4835513$7F6D9672-CD04-4491-89C7-AD0FD1E6A8FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"df4b0d16db5f218d4ee065f1f1897c47e139fa49","datavalue":{"value":{"entity-type":"item","numeric-id":3998281,"id":"Q3998281"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"32a41bcf531e36fc0829a7a6ba146fb03d756897","datavalue":{"value":{"amount":"+0.90092814","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":"Q4835513$F8A84C48-DAAB-4E68-BA4B-F9FFDFCA781D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7c464355e162bb39742d35675ae4f88b3e02fa0d","datavalue":{"value":{"entity-type":"item","numeric-id":4370791,"id":"Q4370791"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d69cfae0d26d118faf3557573b4bab1396eab6bf","datavalue":{"value":{"amount":"+0.9001211","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":"Q4835513$4ACC2EFE-59D3-4E16-AEBB-386AEFAFBEAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1b09c6a971b6451ef202d48aa08df2a5aabea6c5","datavalue":{"value":{"entity-type":"item","numeric-id":3709920,"id":"Q3709920"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"547399d5f05468df9f94ab3506437d1813f11732","datavalue":{"value":{"amount":"+0.8977077","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":"Q4835513$7B982DF0-76AD-4A1C-8EC1-809EAB78114C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"de035f677bc940e95a40c03e8df5350bb9add37b","datavalue":{"value":{"entity-type":"item","numeric-id":3216155,"id":"Q3216155"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b9f4b602f2e2fb6fde81b058d80fd9848df33ba1","datavalue":{"value":{"amount":"+0.89644927","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":"Q4835513$3B630D89-445D-4E43-9F82-537219B16F89","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4835513","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4835513"}}}}}