{"entities":{"Q831932":{"pageid":833780,"ns":120,"title":"Item:Q831932","lastrevid":64783779,"modified":"2026-04-11T22:12:00Z","type":"item","id":"Q831932","labels":{"en":{"language":"en","value":"JEFL: joint embedding of formal proof libraries"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7497921"}},"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":"Q831932$35C0FB96-8C5B-4734-9A2C-93B90997178A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e8b38511aaec58fbd0ec2e7a248997f166b3e195","datavalue":{"value":{"text":"JEFL: joint embedding of formal proof libraries","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q831932$AE128E13-3798-497F-BD7D-43F592B7AFB3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"24ce775dd3115ac7db67e9605f2b1647d6454114","datavalue":{"value":"10.1007/978-3-030-86205-3_9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q831932$1ACABC42-123E-43EE-9823-BC335DD59632","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0eb95a4808de8c6b31b57e0ff6eae4b441be1c64","datavalue":{"value":{"entity-type":"item","numeric-id":831931,"id":"Q831931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$04AD9AF7-BD41-42B9-8E4D-DFF78BE09887","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":"Q831932$2A369502-F77F-47BF-8402-A242E27B659D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ee216241628d7ab3ed1211164658dc9e68b98545","datavalue":{"value":{"time":"+2022-03-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q831932$613A77E3-F8A7-44D9-909F-BBC2D9AAAED4","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"48933c02ac0a74056f14ffe66fc8c394066235ae","datavalue":{"value":"https://arxiv.org/abs/2107.10188","type":"string"},"datatype":"url"},"type":"statement","id":"Q831932$51514CB6-77C2-4485-9FF3-0127E8F7AB55","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"18309be7db1da1fcc09fdceba48f604c7de62db3","datavalue":{"value":"68Txx","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q831932$673E3D17-A36B-43E6-98D1-4C05701447AE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"79c129112f86b813279b3abd3f6f450e60dd7d67","datavalue":{"value":"7497921","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q831932$885A84C8-1912-403F-BE85-E6D55B1EE27E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e179f54eeb2c41b6893bec90499f6e8e05df6b86","datavalue":{"value":"unsupervised embedding","type":"string"},"datatype":"string"},"type":"statement","id":"Q831932$14BFB934-960D-481C-ADEC-5BBFC172287E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0071214bcbe526b674c9631c2a35300c654b00d6","datavalue":{"value":"concept alignments","type":"string"},"datatype":"string"},"type":"statement","id":"Q831932$6C00C880-93C1-43EA-8777-1C38E847B43A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"96b5e90e96bd045c12841d8fa089639012760284","datavalue":{"value":"proof formalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q831932$8F1D621B-2D8D-46D4-BB4A-67AB023C2778","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"401d0247890eedd9719fa19794f4465d9a191693","datavalue":{"value":"system integration","type":"string"},"datatype":"string"},"type":"statement","id":"Q831932$DC3EDA5D-CD2F-4ADB-98B5-F025DB17A670","rank":"normal"}],"P1463":[{"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":"Q831932$3A74A608-CF5B-49FC-988E-DC3F73DD8643","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0921b5c7f4a927689ec755cd551d28920f6f495c","datavalue":{"value":{"entity-type":"item","numeric-id":16268,"id":"Q16268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$E63D994D-9C38-4483-8227-3A77A9EA1D36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7cccd35b34888307d4ad7b137783609eb5c56b79","datavalue":{"value":{"entity-type":"item","numeric-id":16825,"id":"Q16825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$4C94CCC6-206A-4AC7-8BA5-53999113417F","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":"Q831932$7D71DD02-BAE1-47A3-A8AB-FE423872B396","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"98f1934de4273aecf7e2e8a89e3ad6c8eb8ad17a","datavalue":{"value":{"entity-type":"item","numeric-id":37943,"id":"Q37943"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$D15E04B2-9F19-4933-88A7-5B33D80BC950","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"801a319db4682ef4442b12d14dec7cb54b5357be","datavalue":{"value":{"entity-type":"item","numeric-id":44336,"id":"Q44336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$44A75EFA-6266-4AFF-9545-8B1BC387E5B1","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":"Q831932$2B0B7CAF-6AA5-420D-BBBF-8F37E01966CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$D904DDA3-6C7E-4D4D-87F7-92E1D4ECE732","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a94daa7865c51c0d2412cced8422ea9361d06e30","datavalue":{"value":{"entity-type":"item","numeric-id":21343,"id":"Q21343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$0E7C4F58-B5A4-46BB-BD10-4B75DD602526","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"66eb045e037081b6f6e8499f9fef44d8fbb7e0b0","datavalue":{"value":{"entity-type":"item","numeric-id":22240,"id":"Q22240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$E5F05CAA-03C4-44D5-A7AC-A04479FC0D6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b1a7a7177e5127c1ee866175dd9d8f56b0cb8a76","datavalue":{"value":{"entity-type":"item","numeric-id":38920,"id":"Q38920"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$6D1A532F-EF3E-42E5-BF1C-24D44EFBEC64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$447E1CEA-D6E3-4E5C-9F0F-1CB05FE92117","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"771503fee8982049925eed89301d9abaf6576239","datavalue":{"value":{"entity-type":"item","numeric-id":19192,"id":"Q19192"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$714A8BE6-D262-4E5C-9E20-386A8B35B9EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b3d79b8b392d9701f6cbf0671ff230a2010e255a","datavalue":{"value":{"entity-type":"item","numeric-id":19191,"id":"Q19191"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$D0F46BE1-3C4C-4F10-826D-A76057B55163","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"23f1d4970d4f2ba01b8146500b5c1a10ed17d235","datavalue":{"value":{"entity-type":"item","numeric-id":23493,"id":"Q23493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$84432067-1C62-403A-B16F-543769DDD6C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"18e5c9ead524534c7af1459727e22fe055b36f15","datavalue":{"value":{"entity-type":"item","numeric-id":26873,"id":"Q26873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$12CD9EF3-1130-47EF-AB22-A1F787F69961","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b0c13719b309f42056db94fee0aed9d4c5388641","datavalue":{"value":{"entity-type":"item","numeric-id":55304,"id":"Q55304"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$D88E6D20-5116-4488-B084-FEEDC9F63C1E","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":"Q831932$CB4A83E3-3DD3-4BE7-A3A0-10421576A026","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e09ae6f06a096828b21009a799a555e9ad00317b","datavalue":{"value":"W3200624497","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q831932$45D33AB9-1543-483D-9675-894DD5413010","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"cd5f141b3f6929166dbb7299b62fcc7d05829405","datavalue":{"value":"Q108482099","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q831932$26A65C6F-3A35-4722-8ECC-CBCE63A37058","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a1cb7253ab23d987cd27ae9edfcce051c5a2d6d6","datavalue":{"value":{"entity-type":"item","numeric-id":3582695,"id":"Q3582695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$25916FD4-473B-4931-8CE6-1CE1EEBC14A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9d10c643a95f23a54b279e960f27e43ad8b4532","datavalue":{"value":{"entity-type":"item","numeric-id":5495929,"id":"Q5495929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$C1DA472C-DDE6-45A5-860A-74688B718C24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e95e6f4239597f494af058b4706d90738a0b9a69","datavalue":{"value":{"entity-type":"item","numeric-id":3460068,"id":"Q3460068"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$F600D159-1E7E-41D2-B84D-E65E0D60C372","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"be2e8f4770b19dfe4ed5db70d9e22ebf6c799bda","datavalue":{"value":{"entity-type":"item","numeric-id":1640642,"id":"Q1640642"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$0F547F26-5009-49CE-8380-277A5310472A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb1bab11b75e766c233c3a1b9a3682b90b0e288d","datavalue":{"value":{"entity-type":"item","numeric-id":3075247,"id":"Q3075247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$BA336827-A53D-4BF9-AA94-4042BCE61A34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"17a69741364102658aa60a87b94db8d7506ce725","datavalue":{"value":{"entity-type":"item","numeric-id":3183517,"id":"Q3183517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$94B98ECC-303E-4B90-8C27-7ACE9E700142","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6072a2f9daadee48cb9bafeb2cca60d5dd661308","datavalue":{"value":{"entity-type":"item","numeric-id":475385,"id":"Q475385"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$6A0A1124-A529-404B-BBEA-5EB2B25CA896","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3bb85590b29131821d96963718430ffa09b000c2","datavalue":{"value":{"entity-type":"item","numeric-id":5408420,"id":"Q5408420"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$FAD715D1-04A4-442E-8B75-DE74BEEEBD4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb771eb1dd5ac3a4e83b6105ce84dd2191d8e367","datavalue":{"value":{"entity-type":"item","numeric-id":5327336,"id":"Q5327336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$01922959-B462-4159-909F-262F76A5AA22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d3aa637d12e7774743d5229e303a10e1589a2a43","datavalue":{"value":{"entity-type":"item","numeric-id":2870150,"id":"Q2870150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$92190B4E-B3F5-4319-9BD5-F2BB63E77421","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":"Q831932$8E47B191-55F9-4C3C-AA2D-FF1319F692E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93c550078709a24810b3ec6e1d82a47c85cb06a5","datavalue":{"value":{"entity-type":"item","numeric-id":2018657,"id":"Q2018657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$F8903DF9-2DB5-4DC2-82E1-F7C137D9151C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14084b41dac7e71956551690bb40c48e6f7029ba","datavalue":{"value":{"entity-type":"item","numeric-id":5747657,"id":"Q5747657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$0551CE93-8AF2-4964-B7E9-3218EE857DF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b2af2092b9c38b5f11bfd9331f5655e22bc0db44","datavalue":{"value":{"entity-type":"item","numeric-id":3283220,"id":"Q3283220"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$9D6759FC-5D4E-4319-A697-BFB810C3D736","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b39c7a736e0e2ac275eb08aa4f632c9e6e208158","datavalue":{"value":{"entity-type":"item","numeric-id":2364703,"id":"Q2364703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$D863A758-470C-4677-AFEE-9C9AEBD513FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2dedc68dadd430a8cbde5a901ead9a15c139e567","datavalue":{"value":{"entity-type":"item","numeric-id":2843035,"id":"Q2843035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$B96869E2-2E88-481A-8D1C-9C426BB8C432","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d4acf12f6f2468476af5b80237d12aa6e90faaa","datavalue":{"value":{"entity-type":"item","numeric-id":3066085,"id":"Q3066085"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$FE44BF4C-FB62-438E-8671-A630193D3B48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bbf7b4ce3ab96d4236a4c36e2f89589530011a89","datavalue":{"value":{"entity-type":"item","numeric-id":877826,"id":"Q877826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831932$EF7819CF-FB3B-4FD0-A61E-F9659E33EE51","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"JEFL: joint embedding of formal proof libraries","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/JEFL:_joint_embedding_of_formal_proof_libraries"}}}}}