{"entities":{"Q7361192":{"pageid":31519115,"ns":120,"title":"Item:Q7361192","lastrevid":105363842,"modified":"2026-10-07T13:35:04Z","type":"item","id":"Q7361192","labels":{"en":{"language":"en","value":"Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms"}},"descriptions":{"en":{"language":"en","value":"AFP entry Lambda_Free_RPOs"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f63cd0c3b5fbcf301c41fdd9132db8d6c394e1fc","datavalue":{"value":"https://isa-afp.org/entries/Lambda_Free_RPOs.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361192$F2F2711B-7BBC-4C2D-B192-60FC7429DB1C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5396fca6ff93c01f460acc1ce0dece70b0435977","datavalue":{"value":{"time":"+2016-09-23T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361192$68F9026B-0469-417E-BFEE-5D7C8FEB9A5C","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"d593b6f197721b1ecf9f17d8e5bbb2bb5a1f7f8a","datavalue":{"value":"Jasmin Christian Blanchette","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361192$90392E93-B327-4E27-8A67-AE051E213202","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"0bea28856612bb879f597a9d9f573ece274a0783","datavalue":{"value":"Uwe Waldmann","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361192$B1948EEC-D71D-4BEA-AC33-5A224FD4EBA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"8a2e470a50e057f2285d5354789df0be451a8ef1","datavalue":{"value":"Daniel Wand","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361192$F5217E09-4700-4FD8-A83C-548AD7CFAB2C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b07129f2b14cb16071f9eeaa0612a83f7758843d","datavalue":{"value":{"text":"Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361192$D4AC6064-87EA-45E1-A597-B05E1EBCBAE1","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"591e5962a8bea0af1cd0f5371ade459905215bc1","datavalue":{"value":"This Isabelle/HOL formalization defines recursive path orders (RPOs) for higher-order terms without lambda-abstraction and proves many useful properties about them. The main order fully coincides with the standard RPO on first-order terms also in the presence of currying, distinguishing it from previous work. An optimized variant is formalized as well. It appears promising as the basis of a higher-order superposition calculus.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361192$A5772BED-0FD0-472B-9ACE-E2AC1C5419C7","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":"Q7361192$6C1C72CC-6265-4C24-BDA4-544720DCFBD2","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"8f0f13c41ff97fc90cd117120ced19e3dd24a1b3","datavalue":{"value":{"entity-type":"item","numeric-id":7361305,"id":"Q7361305"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361192$E2C4A55F-B63F-47B1-A8DF-25F627E35323","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":"Q7361192$336D6687-5DAA-40B4-B3FF-F756CCA52A0F","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":"Q7361192$D0B3E938-6BB6-4115-9492-A1AB4DA5E132","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formalization_of_Recursive_Path_Orders_for_Lambda-Free_Higher-Order_Terms"}}}}}