{"entities":{"Q6854431":{"pageid":20623228,"ns":120,"title":"Item:Q6854431","lastrevid":84263009,"modified":"2026-05-14T08:59:31Z","type":"item","id":"Q6854431","labels":{"en":{"language":"en","value":"Efficient full higher-order unification"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8163117"}},"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":"Q6854431$CCC8D970-9AA2-4F68-8923-8D53530F8255","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0ed806f0c9d0770545a45b2bc3873e800dbe1b8c","datavalue":{"value":{"text":"Efficient full higher-order unification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6854431$8DC18F04-2A80-425A-9FA1-E1094B313FE5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"44c7aaa45c8dce26fce1055a7b81036597d5f1ba","datavalue":{"value":"10.4230/LIPICS.FSCD.2020.5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6854431$94E23563-256F-4627-9CCE-B0941966B21D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4bdfb0e05a7f9b26ddc4864b42413727acf0142d","datavalue":{"value":{"entity-type":"item","numeric-id":2051563,"id":"Q2051563"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$43D6B249-7387-40C4-8974-CC181B24EC99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"15de60d15cad4f16d9ed61faf6018fbe1d338db4","datavalue":{"value":{"entity-type":"item","numeric-id":1687713,"id":"Q1687713"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$1624CC24-2EE1-4819-BF01-1EC4B2A5521B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"57daeb427a94ed438696f38eadc20a015b03531c","datavalue":{"value":{"entity-type":"item","numeric-id":2055872,"id":"Q2055872"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$F4AD877F-8053-48A2-B4A1-382EDEDEDB1D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"23f7bc78d27ce33f5d6c9d48966ef81d2c43df8b","datavalue":{"value":{"time":"+2026-02-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":"Q6854431$26A8E9B7-F0B6-4BF1-85A9-730A13AE4FA4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"62a49b155c9af634e6c3562b1547da1f7c08791a","datavalue":{"value":"68-XX","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6854431$C364A380-B17B-4859-8234-5959719057AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6854431$2600AAC5-E1C0-4FE0-A1B1-AD46EB6DEBC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f969879f531643f058f8dd4c87a7dd4eb7b8c4c8","datavalue":{"value":"68Qxx","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6854431$883319C2-58BC-48A9-838E-254524A00115","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2c78d37e4b2847d48e4626558cfd9a35a31e7563","datavalue":{"value":"8163117","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6854431$0F384C0C-7E01-4A8C-8351-988F5C732EB7","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"daf5f856a5d861312ad309ab567540337a5f61d6","datavalue":{"value":{"entity-type":"item","numeric-id":57050,"id":"Q57050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$FDA4FC41-6501-42CD-8378-2CCC8A3D03E8","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3922eb0b8235fb2b824bcb3eaa0c8d395dbd512","datavalue":{"value":"unification","type":"string"},"datatype":"string"},"type":"statement","id":"Q6854431$7E7E8539-6399-4F4C-8299-9D7F555EA6E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6854431$18BB5F2E-5EC8-4759-81D2-B42D8D8B7DBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q6854431$C272F740-5641-4536-88F4-D956DA511C58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5a664fc87eb2216b1fad976387dcf6ff589b12b5","datavalue":{"value":"term rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q6854431$4F65DE88-D336-4178-B057-17F74BCDB39E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3f431460ee53197a70fd1cb1eae11681825d1401","datavalue":{"value":"indexing data structures","type":"string"},"datatype":"string"},"type":"statement","id":"Q6854431$EE9CBD82-5E19-4294-A9E4-6BA3E4A9A5DC","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":"Q6854431$3F6F5AB0-25EA-4F65-8603-D43A35BE1BA6","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d7e9017e9f92808788a0b971125d9368ce41250","datavalue":{"value":{"entity-type":"item","numeric-id":5919500,"id":"Q5919500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$A87402B1-3F97-409E-8FDF-30079218F937","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f7a0bc91167b07d4a815fc8e545c25eb6c16c5d4","datavalue":{"value":{"entity-type":"item","numeric-id":2305407,"id":"Q2305407"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$A1A6FD88-B747-4C9E-B9C9-F7ABC2D68AC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"73747d1be528c82497c6517bd1ecf143bfa790b1","datavalue":{"value":{"entity-type":"item","numeric-id":2908482,"id":"Q2908482"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$64AC25DB-C2DD-4B1D-9AA8-CB09E46399BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86c32d3283dbc1fe39bfc7c16048659fcd75d91f","datavalue":{"value":{"entity-type":"item","numeric-id":1687553,"id":"Q1687553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$3D91D2F8-DC14-4460-B725-10FA159E51F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d785b21a69be08181134dbfdfbfbce22753fc47a","datavalue":{"value":{"entity-type":"item","numeric-id":2367541,"id":"Q2367541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$73AFA128-AA57-444F-8A3C-E5C5C8E7D8CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9b757d362e566e6bb8567869560a0af0408a0e3","datavalue":{"value":{"entity-type":"item","numeric-id":1109019,"id":"Q1109019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$2FD1A3C9-5E93-4C34-A73F-B55C742DF7E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1eb387d93d6d1c7b34f751c3ee7736c48adf0665","datavalue":{"value":{"entity-type":"item","numeric-id":1227601,"id":"Q1227601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$5897584A-CA9A-4D41-83C9-5D930F9685CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"18ce06304bf3709cc235c3276b4f500aec1ac468","datavalue":{"value":{"entity-type":"item","numeric-id":1239309,"id":"Q1239309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$CB2EBF34-B7E3-4795-8CA2-6F2324900DCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03e3fc9d5f443dce36999088c8e09a4d011bac11","datavalue":{"value":{"entity-type":"item","numeric-id":3454122,"id":"Q3454122"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$486A31EC-3613-4E6E-AF6C-68903FED435A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"766964ed770f17368ef6d7d908286406ac544300","datavalue":{"value":{"entity-type":"item","numeric-id":5369491,"id":"Q5369491"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$899B9AC3-96AD-47E0-9492-B91C1E1C9A1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d380a2f18f4b02ba06d230258197a946757b5301","datavalue":{"value":{"entity-type":"item","numeric-id":2891520,"id":"Q2891520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$5C19D776-EEA2-4ED7-AD0B-6FBD9B1D495A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$2504D828-2B46-4E71-8023-7643E4CE2040","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$D476D443-AA27-4DCD-A979-CA3D256AD450","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42003db60c26fc6c71649bea3c3f355fc8d1c110","datavalue":{"value":{"entity-type":"item","numeric-id":2908518,"id":"Q2908518"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$715F1FE2-7D8F-4C29-9829-C0334505EA0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aed17d1d7b1ff67830dae739e9417248cd25f604","datavalue":{"value":{"entity-type":"item","numeric-id":1823936,"id":"Q1823936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$1C9CE17F-C8AE-4DA0-ADA1-C2FAEDC489E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad1bdd6abc4d3cf5dea2b7602404acd1281c9b7d","datavalue":{"value":{"entity-type":"item","numeric-id":1799072,"id":"Q1799072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$304A6372-FF43-46F4-9EAB-63A00F23E890","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25368b7fa7ccbbb4d1737a3c36ac442f00182a1d","datavalue":{"value":{"entity-type":"item","numeric-id":1948289,"id":"Q1948289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$0A2B4676-6781-48CC-82A2-C6CA92CBE7F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f82f0f40ab66cf033c5a229880b34de6b2284f9c","datavalue":{"value":{"entity-type":"item","numeric-id":1694574,"id":"Q1694574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$2293DAF2-F290-424F-B261-FF679849E3F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9ae658c7b9ce655f09bbbbf265b43c9366e7c7d1","datavalue":{"value":{"entity-type":"item","numeric-id":5145460,"id":"Q5145460"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$16311527-742D-4CEA-BC8B-5BF09F38F1E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a659ee0ee00bccde846bf20d7f4a7f6a389a214f","datavalue":{"value":{"entity-type":"item","numeric-id":6854431,"id":"Q6854431"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$9AE6455D-5B2E-48CE-86B7-2FBF9C0E9806","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1001498dbf07b01f43f21bb5a8ee3d4a10f94d4d","datavalue":{"value":{"entity-type":"item","numeric-id":3708774,"id":"Q3708774"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854431$1E39A1ED-807E-4FDD-98D2-FC7E75732583","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Efficient full higher-order unification","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Efficient_full_higher-order_unification"}}}}}