{"entities":{"Q4645728":{"pageid":6675309,"ns":120,"title":"Item:Q4645728","lastrevid":58320729,"modified":"2026-04-04T17:21:13Z","type":"item","id":"Q4645728","labels":{"en":{"language":"en","value":"Deep network guided proof search"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6999981"}},"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":"Q4645728$EFEE8F8F-795C-4E00-AE3C-434C7F98D247","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b9eaa73afa776e81545e8abb6988de2e4f0bf399","datavalue":{"value":{"text":"Deep Network Guided Proof Search","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4645728$C4BFF05C-D33B-426D-9332-4C329C0D7871","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0dddd1d1f3ae4f07d55fa74eaaa452c5f12f40a5","datavalue":{"value":"1403.68197","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4645728$EDE6E6A0-0423-4905-8DC8-62763CD5DF9B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8e12f58b629e417604ed68a9d1cc5b352a57e50d","datavalue":{"value":{"entity-type":"item","numeric-id":4635908,"id":"Q4635908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645728$3565D1C5-F547-4CF9-8243-034C6C258209","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fdcab817e753a3fca8b41bfc4270a25f98e1c9e2","datavalue":{"value":{"entity-type":"item","numeric-id":3453881,"id":"Q3453881"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645728$FAD17CCB-8E3E-4B8C-871F-211A8D8403EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4a15b8489bc23e9978bfec23bf3c3944da2339ce","datavalue":{"value":{"entity-type":"item","numeric-id":732239,"id":"Q732239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645728$A6DE1D62-80A2-4C2D-BB23-4AC1CCFEBB86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6ad6a046b48bbe4ab777309f1d5c19b5fc7dfbda","datavalue":{"value":{"entity-type":"item","numeric-id":286799,"id":"Q286799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645728$5A1663A2-AF72-4872-870F-59BEBF8BB6C6","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"eae4601ff702bcaa610b94b3434abd8165930c5d","datavalue":{"value":{"entity-type":"item","numeric-id":4645721,"id":"Q4645721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645728$EA0B4C4D-8B7E-40B2-B3D0-DE3919E9D137","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"412b474a973c0dfa7488c61fc45fdeec318e212e","datavalue":{"value":{"time":"+2019-01-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4645728$E9EEDFD2-C6F1-489A-9AE5-8DEA3BDED865","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6faa5efa084db05e927f30b962c2598a70fac2a7","datavalue":{"value":"https://arxiv.org/abs/1701.06972","type":"string"},"datatype":"url"},"type":"statement","id":"Q4645728$CECDBE03-CE6D-449A-8FB3-CB1A3131D71A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"cfe779e91fe9c53ee133568259955801965765ae","datavalue":{"value":"68T05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4645728$0CEE2012-0C72-41B8-B589-DBD6D5340A69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4645728$4112F0DA-8C15-4151-879F-590707B4B474","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"20804da54f5498ce22ee41d9868893c5e2a15a5d","datavalue":{"value":"6999981","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4645728$7E1BCE5C-8877-46AC-8A66-BDFCFFC8BA7D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"977ed9a5dd338bf424fd0ab29d89678ee0103ad0","datavalue":{"value":"deep learning","type":"string"},"datatype":"string"},"type":"statement","id":"Q4645728$42368F36-2A19-43BD-A58F-8354EC1B4451","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e2e80a7123e4ea6d0418cb24d37b1837f13e3514","datavalue":{"value":"first-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q4645728$9C34AFE7-8D9E-41A2-920B-9BAB7969806F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q4645728$DF49EB9C-9071-42ED-8DEA-ACC860AEDFDA","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"70d015556c31c98a717d424a0c3205751e4d8261","datavalue":{"value":"Q108482125","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4645728$044D8E22-1C45-487E-BC3E-6900EC965504","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"d21b914114b66fc00f5e1083eda38eba4fd88e7a","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645728$B826FE22-429C-45DE-AB5A-F7D988357EDE","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645728$CC1418A2-489B-469B-98A3-FDF0436FF2C2","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":"Q4645728$C77F6661-AE44-4CA3-8064-7CD33D4B5E3D","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":"Q4645728$DA52DBAE-DE20-4F95-83FC-64C6D43DE113","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19db008058ce3a679389c190541b4b00e350555f","datavalue":{"value":{"entity-type":"item","numeric-id":27113,"id":"Q27113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645728$4176431B-FE5F-4046-BE2C-665DB532C2DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"30bf75efb36ce548a631ba3177096a709329cc05","datavalue":{"value":{"entity-type":"item","numeric-id":34000,"id":"Q34000"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645728$E7BAF008-DE43-4543-BA0A-662584B2EE32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"484f589bd857c6ecd5604196ba88033adb11a795","datavalue":{"value":{"entity-type":"item","numeric-id":15128,"id":"Q15128"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645728$633DD3B4-7BC2-4316-833B-AD3F5E7FF442","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27d0ba0f2385e1f67c7a3b66f367fed0cf34c380","datavalue":{"value":{"entity-type":"item","numeric-id":27063,"id":"Q27063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645728$82F33EE7-12B6-4419-B450-E2A071A2726A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4a1e94f157d41116391eea794e4679c715853699","datavalue":{"value":{"entity-type":"item","numeric-id":32991,"id":"Q32991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645728$BDC4A983-67CB-4B27-A730-7A4E2041A808","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"dcb34fec21d2aa2876d052a28b00086d38b84e0f","datavalue":{"value":{"entity-type":"item","numeric-id":41838,"id":"Q41838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645728$707E1EE8-4BB8-4FEB-A80B-5DD8001D2799","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":"Q4645728$961BE484-EE5A-4777-BB41-F2C55852EF4C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"62bcbe829deb09c082539875a4333b4110a050d8","datavalue":{"value":"W2963376030","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4645728$99861319-A2F2-4AE5-8113-C705F68853A4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f140f0bc8ba00c3caf4dd539de59a5988a0f332a","datavalue":{"value":"10.29007/8MWC","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4645728$63968397-8DA5-4240-BDC9-C0A23FB2CFE2","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3ebaf6830eef584d7ab2dc884caeba9d75a64948","datavalue":{"value":{"entity-type":"item","numeric-id":2180215,"id":"Q2180215"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce813994a9deb85cec65966a0bcb1dbf32b598e4","datavalue":{"value":{"amount":"+0.8169493675231934","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":"Q4645728$57951346-E2A6-4675-B34A-69D393E145F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"96c1b94eaf00f419592c0db5550312cdb39e980b","datavalue":{"value":{"entity-type":"item","numeric-id":6166153,"id":"Q6166153"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e37bfb354a646a8ed1c072a2a0fe6f6f4ea2f812","datavalue":{"value":{"amount":"+0.8111553192138672","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":"Q4645728$C1C6A1BA-5908-4115-A9C6-F3728CC9DAE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0c546c37062a648d50a89f0a16d38293ac6aa402","datavalue":{"value":{"entity-type":"item","numeric-id":2104548,"id":"Q2104548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e7bd1f7c7de6ba3b8d7a09ab22318f7742df424e","datavalue":{"value":{"amount":"+0.7940417528152466","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":"Q4645728$3AD8C010-60E6-40CE-89A6-AF08F00970A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b3be07494f3ef7fb3e317edac85e81ec7cceadab","datavalue":{"value":{"entity-type":"item","numeric-id":2364671,"id":"Q2364671"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"34f1b4e820f9f92b7c30ec9ceab83373a81be3ed","datavalue":{"value":{"amount":"+0.7813276648521423","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":"Q4645728$8D50AD54-375B-4473-BFBF-EE32FE7405B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f30c338b15471376e69c1a9415f436ed234c90c2","datavalue":{"value":{"entity-type":"item","numeric-id":2055841,"id":"Q2055841"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"641e04ab13a5bd219bf13af0ccdc4030ad0ab3b9","datavalue":{"value":{"amount":"+0.7717621922492981","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":"Q4645728$96029908-E3B3-4B17-AC5D-4A73D8257368","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4645728","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4645728"}}}}}