{"entities":{"Q3384907":{"pageid":3395610,"ns":120,"title":"Item:Q3384907","lastrevid":55395643,"modified":"2026-02-17T15:29:21Z","type":"item","id":"Q3384907","labels":{"en":{"language":"en","value":"Formalizing constructive quantifier elimination in Agda"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7447763"}},"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":"Q3384907$1F72FE45-74E8-4288-97D7-C00F1A7B157A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"11f85c049bfa4fca27d4fd81162d20b3688a078c","datavalue":{"value":{"entity-type":"item","numeric-id":3384906,"id":"Q3384906"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3384907$A7357F19-7A71-4DA9-BD5D-364B0B4D3DAB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"34b299fdbfa6203a276028105b394bb6d77f2b95","datavalue":{"value":{"time":"+2021-12-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3384907$46C360A7-B682-4339-A650-BCEBFAAE45EA","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"033033bbdcdfe0297a31715b8acb0dbbca4ce1a8","datavalue":{"value":"https://arxiv.org/abs/1807.04083","type":"string"},"datatype":"url"},"type":"statement","id":"Q3384907$CBE1E051-51E6-430A-9B76-9920B0471E70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P205","hash":"c54d1d3e71f365f4f542ff1bc2ae67b0b18469ea","datavalue":{"value":"http://eptcs.web.cse.unsw.edu.au/paper.cgi?MSFP2018.2","type":"string"},"datatype":"url"},"type":"statement","id":"Q3384907$67FA5841-1FA0-478F-A16B-C9C50B7E6BAA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3384907$598836B4-2D12-4177-8E07-4DE9042A4910","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2dc3713aaa399096eeaee95feb03af7b77c250a5","datavalue":{"value":"7447763","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3384907$0EF9DDFA-3A4C-4D35-9E3F-6ABC34F82E35","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":"Q3384907$433B2B20-604C-433F-BB64-2812CB546A6B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"33edf6c60e987374ac2b92fef6c7f79da2b1b282","datavalue":{"value":{"entity-type":"item","numeric-id":2881068,"id":"Q2881068"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3384907$54CCCFAB-64C2-40F6-B11D-A17F8B72853E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"843e3290ea281afff49033aac2cf70e2a4d8546f","datavalue":{"value":{"entity-type":"item","numeric-id":3791109,"id":"Q3791109"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3384907$4362F15F-ED08-48B8-B57E-62238846F35B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77351dbabf5bebdfbc98823dc61ee4a06c4f1b6d","datavalue":{"value":{"entity-type":"item","numeric-id":5625113,"id":"Q5625113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3384907$4B9991F7-64C3-45BE-8880-DF85A28C7D76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4eae5b7e0558bac7e1524f821a03ac55eeef31db","datavalue":{"value":{"entity-type":"item","numeric-id":3582707,"id":"Q3582707"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3384907$FA5B1D06-0B91-4BCC-B82C-5284CA69ADFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"836a1d7b6bdb48a4904f72118ea93610f12fe959","datavalue":{"value":{"entity-type":"item","numeric-id":707743,"id":"Q707743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3384907$893BABB5-1399-4048-8F4F-0C870862A505","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"615c69ac6df9afc124401ae3b18bce04b430598c","datavalue":{"value":{"entity-type":"item","numeric-id":5839923,"id":"Q5839923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3384907$E12AAE57-38DD-48E3-B73F-0D5740C8407D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6cf70fc4006165321afe8c3a2017afd3e9646ebb","datavalue":{"value":{"entity-type":"item","numeric-id":3582707,"id":"Q3582707"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b5d5440da7faa15ad8de31e117756d3a892af92","datavalue":{"value":{"amount":"+0.79753178358078","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":"Q3384907$7CE98E74-9ECD-44FE-A983-57B216D668C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e0a2e10dfaa8dfe1b0905c1cf88300746e0e240f","datavalue":{"value":{"entity-type":"item","numeric-id":2881068,"id":"Q2881068"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"38365c318da853a6073db9a28b4f367964601b3c","datavalue":{"value":{"amount":"+0.7634523510932922","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":"Q3384907$C4B7756D-45A6-403D-A56A-0F8C86B93385","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4826a9ebcee41c22e639fb6a714a4c993eaa4703","datavalue":{"value":{"entity-type":"item","numeric-id":707743,"id":"Q707743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"22cb5d890ea15ff835e46c6347d25df1915010eb","datavalue":{"value":{"amount":"+0.7593699097633362","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":"Q3384907$1C76DCB8-B278-4635-9BDE-05536594B3FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b19f108f54644f0ec26605a1f87cb8a667d4c8a5","datavalue":{"value":{"entity-type":"item","numeric-id":3541684,"id":"Q3541684"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5034f01475da3ac79dbd8bc94e0aa5b341b3c3a8","datavalue":{"value":{"amount":"+0.734165608882904","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":"Q3384907$570ED253-A6BA-492E-9F05-1147396577D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dbd7b8bb72e0c80f6e372a8a89999c6bac81cba3","datavalue":{"value":{"entity-type":"item","numeric-id":5387851,"id":"Q5387851"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"66b273717cd02f8ff8d429fb09ea7f8328ae96a2","datavalue":{"value":{"amount":"+0.730413019657135","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":"Q3384907$31E0A5A1-4538-4DD3-A46A-5F99F1B5F7F0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3384907","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3384907"}}}}}