{"entities":{"Q7361254":{"pageid":31519301,"ns":120,"title":"Item:Q7361254","lastrevid":105364367,"modified":"2026-10-07T13:35:19Z","type":"item","id":"Q7361254","labels":{"en":{"language":"en","value":"Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms"}},"descriptions":{"en":{"language":"en","value":"AFP entry Lambda_Free_EPO"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8a19b12501a8dfdac210b47c8a6e5a913bc8b2d0","datavalue":{"value":"https://isa-afp.org/entries/Lambda_Free_EPO.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361254$F55E094B-9564-4F38-95B5-D83990D211BE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5851604a72cdd40de4e79399957d1d12419d2f19","datavalue":{"value":{"time":"+2018-10-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361254$C51E7724-10B4-40D1-938E-A47C5CCCF9DF","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"82465ac3274d3d0397e8b9a376568cb6edebce12","datavalue":{"value":"Alexander Bentkamp","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361254$3FF84BB1-D267-4BCF-942A-EC18AD063430","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"796ebf1c7a74001c22c95eb54751b63a16275903","datavalue":{"value":{"text":"Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361254$1299BE6C-D2FD-4C7C-99F4-F4E6162D8697","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"95ecca8402e6c73292511156d08e2c282a4de0b6","datavalue":{"value":"This Isabelle/HOL formalization defines the Embedding Path Order (EPO) for higher-order terms without lambda-abstraction and proves many useful properties about it. In contrast to the lambda-free recursive path orders, it does not fully coincide with RPO on first-order terms, but it is compatible with arbitrary higher-order contexts.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361254$FE77D217-F9B7-4DA0-AB72-C63537356209","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361254$A055955D-3630-4148-855C-4C71B79D6CBF","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"cd0c9d6eaf2232ef6bd24acb440211c3c1735214","datavalue":{"value":{"entity-type":"item","numeric-id":7361192,"id":"Q7361192"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361254$5BB699D4-9CB2-4777-B561-A823B2F2B94E","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"edf8a8949edec3767dd80b6d3acecc92e5d25f1c","datavalue":{"value":{"entity-type":"item","numeric-id":7360818,"id":"Q7360818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361254$A47A5A44-EB40-40A3-905E-6E3E2E7A8370","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361254$479029D7-7F0E-4FC2-906B-C213F536DEB3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formalization_of_the_Embedding_Path_Order_for_Lambda-Free_Higher-Order_Terms"}}}}}