{"entities":{"Q6541150":{"pageid":14152293,"ns":120,"title":"Item:Q6541150","lastrevid":57344679,"modified":"2026-03-30T14:09:59Z","type":"item","id":"Q6541150","labels":{"en":{"language":"en","value":"Machine-learned premise selection for Lean"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7850744"}},"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":"Q6541150$297F655F-B0C4-4E71-955D-A8F2CFE81EBF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"93c8cfe24d29a52b2708c7544b150a0b702c76d7","datavalue":{"value":{"text":"Machine-learned premise selection for Lean","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6541150$0B72FBF4-F4CF-4CB2-B921-005673B5674B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"daf5ac6f16e00a4f00507a84f127d74a7fd99a22","datavalue":{"value":"10.1007/978-3-031-43513-3_10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6541150$B92E5AC1-4031-4009-B718-7A631AA69BF9","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"95bfee5a3b5a686f6bf8619ba46dc852c102368d","datavalue":{"value":{"entity-type":"item","numeric-id":1799116,"id":"Q1799116"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6541150$A180BF24-735A-4038-A71A-52E0BDA323D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d7ecb067658e7c3fd12da21c0701295e873dfc92","datavalue":{"value":{"entity-type":"item","numeric-id":6536122,"id":"Q6536122"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6541150$7459581A-3631-4498-B3D9-7C5C2DBBB281","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c8b130515804cee740998b0f664f3c6c23d65127","datavalue":{"value":{"entity-type":"item","numeric-id":6157244,"id":"Q6157244"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6541150$F1297C9C-669B-4B5F-B7CB-094E71C65799","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5058b142e80716c010ccd8a59c73f958f0c0be23","datavalue":{"value":{"time":"+2024-05-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6541150$FFE5B34C-6010-4541-9A3A-CBBEC6451942","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6541150$3DDD524C-9654-4D21-A7A7-D4F13C35F5D2","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"03c96fdedcfea83209b876b2872937426009fa1d","datavalue":{"value":"7850744","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6541150$A33ABD7F-7566-4535-A5A7-542B53A16A01","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f2f01d32e8f9fde0c2fbd1835d9d0396484ba4a8","datavalue":{"value":"premise selection","type":"string"},"datatype":"string"},"type":"statement","id":"Q6541150$AA650E9D-BFF0-47A8-8548-E39A2D402117","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e0afe30fcd4cd25e8e8273c02ad48a97b4a0e001","datavalue":{"value":"machine learning","type":"string"},"datatype":"string"},"type":"statement","id":"Q6541150$7CC4A153-7A90-4974-B67D-2A7D0AF03F67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2b1a6d8526faab7fb68d03e5ec74d5fb9fe3ff04","datavalue":{"value":"Lean proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q6541150$0CEB6856-E3AA-4906-B890-4D4ABBF031B9","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":"Q6541150$F2E37E52-85AB-40BE-98B2-C56C8893D476","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":"Q6541150$A6AF595C-EFF8-4878-B80A-4A954496D9CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9ced8d6f2a9df1ee71786851c7533b59c2dba2f","datavalue":{"value":{"entity-type":"item","numeric-id":331617,"id":"Q331617"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6541150$C7F88D2F-2F4D-4DD4-9578-245507531EF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ee178f7541c5d2ed1d6ee17e1e99ce6d2d8a20c","datavalue":{"value":{"entity-type":"item","numeric-id":5195271,"id":"Q5195271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6541150$AA810346-188C-4151-BA96-20626CE33572","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5a73b7e48adb4260cb48d91e95198beb0803e94","datavalue":{"value":{"entity-type":"item","numeric-id":5952197,"id":"Q5952197"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6541150$DF7D9FA0-B0FF-42F7-AFB2-2CF464285BDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0320a8b4e1768178ac291cd6c061d19c550f5f06","datavalue":{"value":{"entity-type":"item","numeric-id":6483406,"id":"Q6483406"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6541150$A7C9ACF7-6D56-43DB-A9CB-F421231CD266","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e74d3fce405174a77b93de2a6b609361e3b5e6c0","datavalue":{"value":{"entity-type":"item","numeric-id":2364687,"id":"Q2364687"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6541150$A99F36F0-F878-424A-927D-37EF362E0816","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"483d3c17c09c578723154da4261b70aeda673d47","datavalue":{"value":{"entity-type":"item","numeric-id":2351415,"id":"Q2351415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6541150$B2666C49-26B9-4EF5-A6D7-9347EE69409F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e14549321cbae3c57ae9ce6a9266b4af3d64fd4f","datavalue":{"value":{"entity-type":"item","numeric-id":286800,"id":"Q286800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6541150$746411A2-6C8B-4D7A-B295-32D30D11B517","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"15c58f40f8893ea08e9b168dd3629a56d2e8291d","datavalue":{"value":{"entity-type":"item","numeric-id":2908509,"id":"Q2908509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6541150$CC6BF71E-8DCC-4C71-AD59-DAFCD327CAB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"432347ebf7758fa5347be4c601bf2d08f68cb652","datavalue":{"value":{"entity-type":"item","numeric-id":2055901,"id":"Q2055901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6541150$8B10CF0F-1D29-4914-8878-3EAF7CD76DDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"41c828c42273fdd92d75a81a8b0926cb29b7e446","datavalue":{"value":{"entity-type":"item","numeric-id":1799117,"id":"Q1799117"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6541150$FF1BE92B-D702-4CEA-A4CA-E50FC558204A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4a29860ebd84f7337a18d8f88370124a69396a2","datavalue":{"value":{"entity-type":"item","numeric-id":2128797,"id":"Q2128797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6541150$3665CA12-EA9F-4B44-865F-81E2B9D8EEA2","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6541150$05BF218D-0F0C-4231-BC6B-94FAB719A9FE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6541150","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6541150"}}}}}