{"entities":{"Q40317":{"pageid":40373,"ns":120,"title":"Item:Q40317","lastrevid":105427130,"modified":"2026-10-09T10:06:55Z","type":"item","id":"Q40317","labels":{"en":{"language":"en","value":"Presburger Automata"}},"descriptions":{"en":{"language":"en","value":"AFP entry Presburger-Automata"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"0bccfc4e3878b4277c7a473b3780499dea482749","datavalue":{"value":"28603","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40317$04F3583A-3547-43A4-A66D-E5D63FAD3739","rank":"normal"}],"P286":[{"mainsnak":{"snaktype":"value","property":"P286","hash":"805131d11d6c60d1cab1b5a3a96121273fd3de55","datavalue":{"value":{"entity-type":"item","numeric-id":3183526,"id":"Q3183526"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$DE048A8E-FF94-4FD9-9537-1C30C20EBEB7","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":"Q40317$41A53952-D129-41E4-8EC9-51A3E023F4FA","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"17de625ac31e0955e544c9c548085103d5bf4209","datavalue":{"value":"https://www.isa-afp.org/entries/Presburger-Automata.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40317$6CF97CB1-83DC-4C98-88BB-DDD66BF5BA16","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40317$203A6585-9851-4D3F-9C5A-319E0571B57D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40317$8728FC92-E1F5-4081-951F-3AF37207E795","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40317$E42E9B34-4BD0-43A6-8258-C2CF3E9691F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40317$5370DFA7-A3EF-42A1-BB90-29E7A7C5DB57","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$B594977B-2756-420E-A172-D977A3F25C68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$9CFB0D82-2845-4C93-9FCD-FB93CA623089","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2778ef58df5d105bc5fcd1f1e6190b4cffc33d19","datavalue":{"value":{"entity-type":"item","numeric-id":40261,"id":"Q40261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$36577DF0-6A06-4A72-902E-B0D08A0B0F1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$FB5C476C-45CF-4F72-ACB1-5E07A7C602C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$BC0CB0A9-610D-424F-9D17-B52E1BE414D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"03281999c3208b8f3a62eaceadadf1ce834fe219","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$8C7C8585-06CC-47C8-9A9D-19EAB120FAEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ea53781dc0a29ca150a09c3de99800e897e49297","datavalue":{"value":{"entity-type":"item","numeric-id":40507,"id":"Q40507"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$A11CE489-0BBD-4EDB-A2A1-B367DCF21711","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ab576408136da65ce68abf8488b4c4362524857b","datavalue":{"value":{"entity-type":"item","numeric-id":43941,"id":"Q43941"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$847BDCE1-A15B-4E54-A5EB-41A0369AED86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"57544187ec5ad8468535e20e3999d5193a0787a3","datavalue":{"value":{"entity-type":"item","numeric-id":40275,"id":"Q40275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$3264D449-6FF2-4D30-A37D-901A0EADC590","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"33a2c00edd213d9c703e35c0ce5b77b6ea1dd277","datavalue":{"value":{"entity-type":"item","numeric-id":18304,"id":"Q18304"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$21A6BEB1-52E2-4414-BA91-FBDB6A019C4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"81319f5b8664d8398f69fd7004689cf3156bb740","datavalue":{"value":{"entity-type":"item","numeric-id":40964,"id":"Q40964"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$81FCCBEE-6B58-4173-A141-6B3CA57F545C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"87ec2ca742c9eb10fbaa98b1820ddb7f4298bb25","datavalue":{"value":{"entity-type":"item","numeric-id":40963,"id":"Q40963"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$0D2A473D-1D70-437E-9FC1-642D4A771B85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"c1161e1e8de5a1bc9eb8260f27cf5114412c2b8a","datavalue":{"value":{"entity-type":"item","numeric-id":21343,"id":"Q21343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$871B1C5F-1386-4BBF-9C45-A4769800483E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"b49b6cd0d730920a3a4cd5d33a24263cc6515903","datavalue":{"value":{"entity-type":"item","numeric-id":43940,"id":"Q43940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$614FBD02-4A3E-444B-A92A-C684C4A86A95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"21ac0ce33ff9fe81fbefb6b70fe4d49e97e0f1f7","datavalue":{"value":{"entity-type":"item","numeric-id":18433,"id":"Q18433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$F2EABEAE-2D19-4B09-9292-D623E1F363C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"4d7f4b76492a75780585d40fb718d00d42a05322","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$8263A989-9152-4DD4-B3EF-87E0E6D019BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"b82152c1528c5be7e2040d1abd74977f4fe51817","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$DAAAE5D6-B548-4603-B023-3654EF77B504","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"32eb0c8abe1b67b4df46bc8108bb18a63a80ff38","datavalue":{"value":{"entity-type":"item","numeric-id":17120,"id":"Q17120"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$46E593DC-CCAA-4226-9A6C-28B0557D3B14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8dde418bf28e22fefe1976bd953eb7c8ec5b548d","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$0349EDAB-C3F6-4195-89E0-CC48CC5FE951","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f01c83a5a54fee889f3ec90409eea63e50d19053","datavalue":{"value":{"entity-type":"item","numeric-id":20369,"id":"Q20369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$C152B0C2-C640-4919-88E0-53B65BE1D169","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6fc7ed5d55470ad0fe2cfaad954012f59ec24c56","datavalue":{"value":"https://isa-afp.org/entries/Presburger-Automata.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40317$ECDD1360-7C83-461D-A44B-47BEFEAF5E65","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"42cc17b6ebd1e6b2e2779d5c2e7eb07525a54975","datavalue":{"value":"Stefan Berghofer","type":"string"},"datatype":"string"},"type":"statement","id":"Q40317$FFD9FAAB-9B88-4313-B5F5-8843D20F7BA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"3805736ecfc5387be03f2620dce52d9d6776ee94","datavalue":{"value":"Markus Reiter","type":"string"},"datatype":"string"},"type":"statement","id":"Q40317$C2192DA9-9F0F-4889-B9A8-EA6971417A51","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"c7a32be23b695edd672e94beb7ebd6848c0b45f0","datavalue":{"value":"This work presents a formalization of a library for automata on bit strings. It forms the basis of a reflection-based decision procedure for Presburger arithmetic, which is efficiently executable thanks to Isabelle's code generator. With this work, we therefore provide a mechanized proof of a well-known connection between logic and automata theory. The formalization is also described in a publication [TPHOLs 2009].","type":"string"},"datatype":"string"},"type":"statement","id":"Q40317$98FDF068-E22E-42A9-A667-BCC82B1C189A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"403738ebc449032b2c0b132c2ef1a436783bf929","datavalue":{"value":{"entity-type":"item","numeric-id":3183526,"id":"Q3183526"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$9E60C955-C01A-49A8-8F67-FABF42BF9C13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d51787ebb8f2f656495faac1b54743656ef36ab4","datavalue":{"value":{"entity-type":"item","numeric-id":5878899,"id":"Q5878899"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$46905FD3-1DB6-4358-8374-7DF052DB548A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"69726574968741404781ab1dd6b86acc8887068d","datavalue":{"value":{"entity-type":"item","numeric-id":4218939,"id":"Q4218939"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$CC0ED579-F670-4F1A-A88F-A4A5CD0144A3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"05684a6a76ae208e2fab322cb348b334f82a2986","datavalue":{"value":{"time":"+2009-12-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40317$3708AE4E-8AF8-44C0-91F2-954FD8A6D294","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4f2a765cf4d3cf22b6877aaa959051483ae6306a","datavalue":{"value":{"text":"Formalizing the Logic-Automaton Connection","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40317$8DC5797C-CA3F-4D80-A9BF-527A47D68ABC","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":"Q40317$F0751C0B-659C-4F32-BE91-E1F83A55451E","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"73d93a21b0749f7f2c51d7daeb11b162660cd756","datavalue":{"value":{"entity-type":"item","numeric-id":7360784,"id":"Q7360784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40317$1A9BBB25-C797-4014-BA3D-33F563747CBB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Presburger Automata","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Presburger_Automata"}}}}}