{"entities":{"Q7361076":{"pageid":31518767,"ns":120,"title":"Item:Q7361076","lastrevid":105362591,"modified":"2026-10-07T13:34:22Z","type":"item","id":"Q7361076","labels":{"en":{"language":"en","value":"A Verified Efficient Implementation of the Weighted Path Order"}},"descriptions":{"en":{"language":"en","value":"AFP entry Efficient_Weighted_Path_Order"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"aa4960413e40b6d997b70407077816a216ef21ab","datavalue":{"value":"https://isa-afp.org/entries/Efficient_Weighted_Path_Order.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361076$E2211407-D691-433A-B384-6A82C138D392","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1e1ff792d185300099d93a7961359890b67878e2","datavalue":{"value":{"time":"+2023-06-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361076$928FD2EF-95AA-43BD-AA71-DC4FAE146461","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"3e961f1f2b2e533bd88ffdbcd178bd2ef2813f73","datavalue":{"value":"Ren\u00e9 Thiemann","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361076$DBD9B6E3-B3ED-4960-8D4E-93D6B0E0D3FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"d3632b898ce270785b084275cbaa12e70cafbc24","datavalue":{"value":"Elias Wenninger","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361076$D5CB03C1-01A6-4E2D-90C5-3DF52A6B500F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3c7a25bf917d0942a121f5956b1a77b6470710ae","datavalue":{"value":{"text":"A Verified Efficient Implementation of the Weighted Path Order","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361076$B4805451-38B6-488D-9DAE-C9C426AA6857","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"cb692768e972d6b241cb67cbfc44a3100966f891","datavalue":{"value":"The Weighted Path Order (WPO) of Yamada is a powerful technique for proving termination. In a previous AFP entry, the WPO was defined and properties of WPO have been formally verified. However, the implementation of WPO was naive, leading to an exponential runtime in the worst case. Therefore, in this AFP entry we provide a poly-time implementation of WPO. The implementation is based on memoization. Since WPO generalizes the recursive path order (RPO), we also easily derive an efficient implementation of RPO.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361076$7301901B-B2EB-4EA0-A5E7-A3A5B44F7193","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"d6d3f5f0e6d39b0610560c479018fc71a2adcd20","datavalue":{"value":{"entity-type":"item","numeric-id":1098624,"id":"Q1098624"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361076$6E632FB5-B263-4FBC-A2C0-02C120FCF440","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c18873a91638da67cfe8ac354267476880abf3d9","datavalue":{"value":{"entity-type":"item","numeric-id":6854432,"id":"Q6854432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361076$E3760F8C-D101-4C4E-98E6-67CF62738F17","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":"Q7361076$FA9FF392-AF1B-4959-8933-82027B2D866D","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"4818bbf7d89ba2c3179bc556d045d6dc521fe671","datavalue":{"value":{"entity-type":"item","numeric-id":7361813,"id":"Q7361813"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361076$EE2551E7-92E0-409B-9497-F96813736125","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":"Q7361076$77AFDDF9-2C2E-4413-BBEF-D7AAC670F7A4","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":"Q7361076$67670EF2-7FCE-401C-A860-6449DF1ED5EB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A Verified Efficient Implementation of the Weighted Path Order","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_Verified_Efficient_Implementation_of_the_Weighted_Path_Order"}}}}}