{"entities":{"Q2180215":{"pageid":2190958,"ns":120,"title":"Item:Q2180215","lastrevid":82575098,"modified":"2026-05-06T21:13:57Z","type":"item","id":"Q2180215","labels":{"en":{"language":"en","value":"A neurally-guided, parallel theorem prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7200353"}},"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":"Q2180215$FF51C956-5902-4D7D-B3F2-750B9ACBF79A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"14350a20f5b2e4700fe2408a505c05f07c853396","datavalue":{"value":{"text":"A neurally-guided, parallel theorem prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2180215$B2EC537A-73B7-44A4-B1AF-FE1DEC9905F4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9d233b18b9218835fab54b198bd71be7df011b42","datavalue":{"value":"1435.68374","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2180215$4E02D5F9-20CE-4F77-A106-5C85940D4C9B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b06c7b1915a4ba19692233e9bfae08359707c103","datavalue":{"value":"10.1007/978-3-030-29007-8_3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2180215$C1FB1723-3186-4E84-83A7-BDECB236DF76","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fb7dd3297c3c7baf9cae0b0d12835083a74349d0","datavalue":{"value":{"entity-type":"item","numeric-id":2142074,"id":"Q2142074"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2180215$16CAC7BE-0ECA-42FB-9D43-7F45F7BED735","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"395a9171f6bae9b8af4e7440aa83cc44ae6e3948","datavalue":{"value":{"entity-type":"item","numeric-id":2075783,"id":"Q2075783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2180215$871579CD-A266-4FBC-8093-EEA8342957A4","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6d0c48627b068f854a947856c3807165d49ca3ba","datavalue":{"value":{"time":"+2020-05-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":"Q2180215$B37E8960-B9EF-4ECA-936A-B44615E4B47C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b772cbef448d3123b31247f5558bf0997ee9766d","datavalue":{"value":"https://www.research.manchester.ac.uk/portal/en/publications/a-neurallyguided-parallel-theorem-prover(d64986e4-5d48-4f6b-9f7c-a329ddd4c6e8).html","type":"string"},"datatype":"url"},"type":"statement","id":"Q2180215$C2041405-8D7A-4A87-A35E-87629F0412B7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2180215$D18251FF-DA27-4EFC-81AB-321AABFF3059","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"988173f83ba36b50a20769cfc8026292f0fe0dbe","datavalue":{"value":"7200353","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2180215$D6A15A12-4568-4F58-B835-0F268C31DA87","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3640b5395457c8e78cd0865e114c80a8efc0e4bd","datavalue":{"value":"ATP","type":"string"},"datatype":"string"},"type":"statement","id":"Q2180215$4B34FFF0-3B26-4B75-9565-FD691FBAE172","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"642c553111ff0374dc7048588c9b5ce18dbfbb2c","datavalue":{"value":"graph convolutional network","type":"string"},"datatype":"string"},"type":"statement","id":"Q2180215$74C96C2D-0211-4A5C-B212-501922E2220E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"45ba0550e07e04a3326d1cb7dbe398ac3d7c209d","datavalue":{"value":"tableaux","type":"string"},"datatype":"string"},"type":"statement","id":"Q2180215$63CB7831-715B-4ED3-9E0E-B757BC1E30C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ca45f3e82cce9156201a7a268dd0890c00ca469f","datavalue":{"value":"MCTS","type":"string"},"datatype":"string"},"type":"statement","id":"Q2180215$C3DEF1B2-726B-4833-AA98-C9E8EFC9C042","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b443b776731e3bc75eb79b752e7ef8c4cee2d97a","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2180215$44CB88B6-B3F7-4CE7-BA17-4FB1F22E867F","rank":"normal"},{"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":"Q2180215$875BEDA9-DE1D-42A0-849D-272D4408D633","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d4725be8fa705861afbab12b59e447099c9ebb4e","datavalue":{"value":{"entity-type":"item","numeric-id":20216,"id":"Q20216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2180215$4D741B9B-2082-4136-A3FF-1C324DE30C5B","rank":"normal"},{"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":"Q2180215$6DF64C24-CCA9-4D1B-8946-B1B9CDA567B1","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":"Q2180215$AEB8976B-9C11-40D2-BBFD-0EC1AB0FD0F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"62af2c5e450adf37bd9acb47c5a55b60b68447ea","datavalue":{"value":{"entity-type":"item","numeric-id":22241,"id":"Q22241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2180215$A0DCE558-2445-4176-9E5B-628A3716C3E6","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":"Q2180215$1D1641AF-DD6A-4262-BFA8-496BCFBD5AD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"effe99d4b547ffcbc07915d8ced5dc197768f166","datavalue":{"value":{"entity-type":"item","numeric-id":15028,"id":"Q15028"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2180215$91FEA071-29BB-4CB9-8F8B-5C4C97DFADE2","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":"Q2180215$4E8AC86D-343A-4134-9E89-3F3C9883363C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4db67863b5fec3bef62722f41df2cb373dae295e","datavalue":{"value":{"entity-type":"item","numeric-id":27083,"id":"Q27083"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2180215$380A3FE4-4950-4EF9-8028-043253CE9610","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a28c49518b2391a3c9e2da3891679e04c0308e5d","datavalue":{"value":{"entity-type":"item","numeric-id":32752,"id":"Q32752"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2180215$1F384C90-DFBD-4516-AA11-6053139A836C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5d21be4c8a37ad19736ca38bb83a00d1f4ca63e3","datavalue":{"value":{"entity-type":"item","numeric-id":33354,"id":"Q33354"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2180215$6300B2D4-8BCE-4173-B655-E0E7B9334FC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d7080ec90546ccf740799d90136dfd2e93385c80","datavalue":{"value":{"entity-type":"item","numeric-id":39267,"id":"Q39267"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2180215$8FA0127A-88A7-42E0-A663-CA3A9B4CABDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"33061b9a75e57d93e8912d2c2b716b27d6bd52ab","datavalue":{"value":{"entity-type":"item","numeric-id":40369,"id":"Q40369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2180215$29EBC2B6-3C24-443C-BB57-DA1EC2FD922C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bd3fa568ce44545ce1c1bded3c45ecc37b43b7c1","datavalue":{"value":{"entity-type":"item","numeric-id":21467,"id":"Q21467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2180215$B8252691-69D0-4F19-B30C-DE736D366E3F","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":"Q2180215$3F976E47-F37D-41EE-BBDA-1A899F8E7BE6","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"cef614ca12b3ec0546e03fb6756cb98ffcd17c47","datavalue":{"value":"W2963560424","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2180215$0DFA2AF2-6CE0-416E-B45E-0FA78977793E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7450ef75eab7759ec3e2c41e6b79462da7c276b1","datavalue":{"value":{"entity-type":"item","numeric-id":4645728,"id":"Q4645728"},"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":"Q2180215$703CEA6E-8E04-4C01-82BA-57BEF32586EF","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":"e0d4f5ded1cb5df7fa777a5ddbdb7e7d44cb1d87","datavalue":{"value":{"amount":"+0.8052183985710144","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":"Q2180215$C5768AFF-35BA-410B-B234-A511A4930CE1","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":"102618f9a62015fccfa36730a4dc8a562d20d612","datavalue":{"value":{"amount":"+0.8022658824920654","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":"Q2180215$D3D4B30C-4A6A-4C82-A74C-9A4933154555","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7d85b2603075e198252cf747fcc485a279e29304","datavalue":{"value":{"entity-type":"item","numeric-id":6488552,"id":"Q6488552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e86a9e851d1fc52859b3e333a1c537be578962be","datavalue":{"value":{"amount":"+0.7635107636451721","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":"Q2180215$B48769C8-80A3-47B9-887C-BB8FEA146A40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"93b0ee1aa1059e8357bcab602d009a9564d46164","datavalue":{"value":{"entity-type":"item","numeric-id":1390660,"id":"Q1390660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1354577505adbf44be7dc9cd0cdcae89767e9ba5","datavalue":{"value":{"amount":"+0.7595673203468323","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":"Q2180215$4517B2C1-6959-4A73-9CC8-583C0186A75F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A neurally-guided, parallel theorem prover","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_neurally-guided,_parallel_theorem_prover"}}}}}