{"entities":{"Q3523164":{"pageid":5553068,"ns":120,"title":"Item:Q3523164","lastrevid":80636633,"modified":"2026-05-06T16:39:25Z","type":"item","id":"Q3523164","labels":{"en":{"language":"en","value":"Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5318934"}},"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":"Q3523164$8132383D-CC2E-41EC-BCA7-47131D50CC1F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"61583b63ac83c2e3bfe5812ee7c8dbdbbec975fc","datavalue":{"value":{"text":"Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3523164$AF6AC02E-12C4-4221-A2A5-2D6322CD5AF4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8ce74b902be426731627371a752b12d137d94c67","datavalue":{"value":"1144.68352","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3523164$9F43B780-B626-445D-9B76-CC8461664C1F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7cf0d7a4ac69499ab83b53898418e184b6fdb234","datavalue":{"value":"10.1007/978-3-540-74591-4_5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3523164$4A30ECBE-BDEC-4C8F-B294-AAAC96DA4084","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"08f6a76b1a5751a176b642aca232b1b00d17f433","datavalue":{"value":{"entity-type":"item","numeric-id":2891446,"id":"Q2891446"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3523164$A9FE3C95-069A-41DF-90AB-5D1EE6627B10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bb9a75665101462bc01a2c7426c95f31a74ce050","datavalue":{"value":{"entity-type":"item","numeric-id":438557,"id":"Q438557"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3523164$8F24211E-74ED-4A12-BD42-4FE96F27D535","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bd39997decddd4925a8ef09cbbffc4f41d2b1f00","datavalue":{"value":{"entity-type":"item","numeric-id":670700,"id":"Q670700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3523164$47E945D9-A2A4-47E3-A1DB-C7BFE04EF24F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3523164$43FD2C29-0DFB-477B-A09C-87FED2399E31","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"20b7f535510e218ce28c7540c7cdc4660c15d850","datavalue":{"value":{"time":"+2008-09-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3523164$6EB4DD03-E99C-41B2-965E-A4503A930A6E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3523164$2B0E024B-4C04-47C9-8AF8-5DB65EC0A37A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d5bf1b5557315bde2270ac1f12a0be5d8bb4569e","datavalue":{"value":"5318934","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3523164$3EB9252B-A355-4FF9-B16C-52896A2C6328","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3523164$E7BD07C7-8488-455D-B903-3098E1ECEF53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3523164$D650F0FC-E6FA-4E6E-83ED-00CFAF3FAC28","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":"Q3523164$9E76A6B4-D17A-4B12-9004-6C370240C8B4","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":"Q3523164$A7655328-C8D6-4D51-8DBC-A522FF402783","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":"Q3523164$DBC8B561-2DE6-4FB1-B515-F5652450CD06","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f288bebc5a13163d12e4dd0e4500a0840fb630db","datavalue":{"value":"https://doi.org/10.1007/978-3-540-74591-4_5","type":"string"},"datatype":"url"},"type":"statement","id":"Q3523164$6EE8DDEA-EC93-421D-8C8C-E0978839CE0F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e5d7df73fbfb3b0185ed457a2475999da444a1b7","datavalue":{"value":"W1869527659","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3523164$5CC9EF30-34B9-4687-B3F2-27644CF90EFE","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b41219a08974f1820b6a934c8c33bf903d59a40e","datavalue":{"value":{"entity-type":"item","numeric-id":3088004,"id":"Q3088004"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"927628133b2c516515853f3d4c621cf98a9b5f0e","datavalue":{"value":{"amount":"+0.821682870388031","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3523164$A848812B-0E6A-44B6-A614-0B5A4DB754F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"73732f22ae9e393a28f631d7255522eb6210bdc2","datavalue":{"value":{"entity-type":"item","numeric-id":2702599,"id":"Q2702599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"45c1fb4169907c801edc98e886aa71ff9c53d060","datavalue":{"value":{"amount":"+0.803425133228302","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3523164$66ABB003-49AF-4BEB-B637-602AC0D7A7EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b842f6c5c6f6cb13a80a9ee17335820078928091","datavalue":{"value":{"entity-type":"item","numeric-id":1346629,"id":"Q1346629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4920c45ebe218844f6e8978277661e20a88aa79e","datavalue":{"value":{"amount":"+0.8024665713310242","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3523164$62595B1A-1B41-42A7-BC62-362051C9C7CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad8945dd5ea8b23803758fedaea5e36aad46444f","datavalue":{"value":{"entity-type":"item","numeric-id":4494365,"id":"Q4494365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6cce305256a6023cf9bc430642bb18c441acf768","datavalue":{"value":{"amount":"+0.7922653555870056","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3523164$9A208DBD-76DA-445A-8993-52E7576B5ED3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3a75c513a94b6c26a0105286d556bdf47451491e","datavalue":{"value":{"entity-type":"item","numeric-id":3620615,"id":"Q3620615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6cce305256a6023cf9bc430642bb18c441acf768","datavalue":{"value":{"amount":"+0.7922653555870056","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3523164$F066B89F-3297-412D-A6E4-2048464F988E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL","badges":[]}}}}}