{"entities":{"Q5387920":{"pageid":7417494,"ns":120,"title":"Item:Q5387920","lastrevid":50366540,"modified":"2026-01-13T21:58:38Z","type":"item","id":"Q5387920","labels":{"en":{"language":"en","value":"To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in $\\mathit{SMT}(\\mathcal{EUF} \\cup \\mathcal{T})$"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5279599"}},"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":"Q5387920$C312E8A4-0440-4845-9B6A-50F1202A6C79","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"765d0592d7976c9392b1a2f4d74359e91c2bd39a","datavalue":{"value":{"text":"To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in $\\mathit{SMT}(\\mathcal{EUF} \\cup \\mathcal{T})$","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5387920$621AF003-F1A8-4D49-BBA8-B451D7C11D3C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4110acfd0dd263fe181160b48366e7eb74dd6bf8","datavalue":{"value":"1165.68482","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387920$73B6571C-5FA5-4D8A-A67A-A9721A225079","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ed0ab36f5227356837f65cec389c99ea69128e75","datavalue":{"value":"10.1007/11916277_38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387920$BC299760-149F-4941-9993-0581EDFCB1E0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7b1bce7f658807241618c24b1a425d03bccc6443","datavalue":{"value":{"entity-type":"item","numeric-id":479813,"id":"Q479813"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5387920$FB2EA19D-C143-443A-9977-6F2C4A8AF7E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"387e6ac60ed3a0144bb303179c23c53493d401d0","datavalue":{"value":{"entity-type":"item","numeric-id":329418,"id":"Q329418"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5387920$E0B31249-BA15-4D05-BEEA-58DFE9E54F18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4cd48eb61e203d5044e95bf99a9a9627aeaf2505","datavalue":{"value":{"entity-type":"item","numeric-id":1037398,"id":"Q1037398"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5387920$216BC505-37E8-4857-B2E8-738FB98EEC07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e97e7d65eece04188cb1a1dff66ddc09c38fbea4","datavalue":{"value":{"entity-type":"item","numeric-id":479835,"id":"Q479835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5387920$7B91E847-9C78-4ED5-97D5-D9674905F14E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dd3de1d09a612b5191ae1f6940eb136e3c3558b9","datavalue":{"value":{"entity-type":"item","numeric-id":5387919,"id":"Q5387919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5387920$1E838799-41A1-42D7-8CE5-9D50A4805A8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4fd5a076641129df5baba24779caed9dec893447","datavalue":{"value":{"entity-type":"item","numeric-id":511776,"id":"Q511776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5387920$AAE96B3B-EE50-42AB-AB3F-7F90412EC4D8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"23864e2be568bb8a6a4b0526f5a5216348320070","datavalue":{"value":{"entity-type":"item","numeric-id":2870110,"id":"Q2870110"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5387920$6BF82C91-37A2-4A91-82BE-10EF6D83BD4F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6183386ae8366a240584c653ce5ca2494433aedb","datavalue":{"value":{"time":"+2008-05-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5387920$EF788527-A775-439A-A5AF-FD382D26EF36","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387920$6C571FD5-4270-4706-BEC2-B641F08326DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387920$30B55A0E-CF0D-400A-B282-A84D513E9253","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387920$F279582E-53C2-440A-B57A-FE8EAF670987","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f2dfe9c55f8516ccec9bb0488ea94cf8b581c0e5","datavalue":{"value":"5279599","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387920$20B1704B-067C-4960-A0B6-1FF880440B30","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"974d686bb7a8166ba9e2c27ca746a951eae6eb2a","datavalue":{"value":"Q62041367","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387920$F1126F2F-CCB2-4438-940C-8A68C74F3750","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":"Q5387920$70FCF4CB-0FCD-41BF-A868-9B09EF6AFBFD","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"cfd7e3200de97c4d74705556c2df8ab54e7f047d","datavalue":{"value":"https://doi.org/10.1007/11916277_38","type":"string"},"datatype":"url"},"type":"statement","id":"Q5387920$9678E3E0-D5F0-4A06-8A98-1F0B0D0E27F5","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b40d6d46eb27b3330fb1dcfde1f577fcffeb71ea","datavalue":{"value":"W1831282309","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387920$4BF374AD-0CAA-4E4A-A1BC-67FC0786117F","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"f5a79cf0e1855bbbc34d5cf368078022fe533773","datavalue":{"value":"conf/lpar/BruttomessoCFGSS06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387920$313CFC84-A133-4EEF-90F8-4EAFE41F79CF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"47a27d644bc37c8513cc96e390f432ba6042278a","datavalue":{"value":{"entity-type":"item","numeric-id":2432765,"id":"Q2432765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d51f7d23337ada3df8fcd218eb68f319acf6b3e1","datavalue":{"value":{"amount":"+0.7482864856719971","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":"Q5387920$E37A3795-AA7A-4C2B-8811-B830973ABF11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fd383dfcfaa29dfecf25405e7e7fb128b0b5ca3e","datavalue":{"value":{"entity-type":"item","numeric-id":2848689,"id":"Q2848689"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aa9c83b96477e488ba3dbbc9cc6cf30b82252aa0","datavalue":{"value":{"amount":"+0.742795467376709","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":"Q5387920$D74885F2-C552-4A1F-9D42-05839DE5CFBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c346a30c2b2aed7868880120d4d7c225af677033","datavalue":{"value":{"entity-type":"item","numeric-id":6039408,"id":"Q6039408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"36dd0d96f9a63f0322020911cb84d1b23fd34db2","datavalue":{"value":{"amount":"+0.731924831867218","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":"Q5387920$99B0460F-E171-431E-864E-EE18FEC082B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7f43ea42045a25afcb7c0a99962bfe0a3b2188c5","datavalue":{"value":{"entity-type":"item","numeric-id":3172881,"id":"Q3172881"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8fe6785b7e6f673ba7982091faf1883878dda66d","datavalue":{"value":{"amount":"+0.7277838587760925","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":"Q5387920$BA269366-3128-4335-9268-456D13A46DFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"18ba98873d052f5816175646d512a17079b79c03","datavalue":{"value":{"entity-type":"item","numeric-id":3176369,"id":"Q3176369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6f614ce464a905aef19faad2e5c72865113be609","datavalue":{"value":{"amount":"+0.7196142077445984","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":"Q5387920$82710405-5E4A-468B-BA3F-4A517D5D0BA2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5387920","badges":[]}}}}}