{"entities":{"Q7361774":{"pageid":31520861,"ns":120,"title":"Item:Q7361774","lastrevid":105423845,"modified":"2026-10-08T13:45:47Z","type":"item","id":"Q7361774","labels":{"en":{"language":"en","value":"Formalizing the Logic-Automaton Connection"}},"descriptions":{"en":{"language":"en","value":"AFP entry Presburger-Automata"}},"aliases":{},"claims":{"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":"Q7361774$7B369C58-C009-451B-8C20-68E338021B86","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"42cc17b6ebd1e6b2e2779d5c2e7eb07525a54975","datavalue":{"value":"Stefan Berghofer","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361774$FDC3DD76-D4BF-447D-BF84-D7DF3C79EFE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"3805736ecfc5387be03f2620dce52d9d6776ee94","datavalue":{"value":"Markus Reiter","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361774$E302BFE2-BD41-476D-B90D-4B54B18B3413","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":"Q7361774$3EC75A9A-0962-460F-BF64-7719369F0B99","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":"Q7361774$A263F99A-A001-4D34-90B2-BA72706D05B0","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":"Q7361774$C4140780-818E-47DB-B45E-B0E3B3D50F90","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":"Q7361774$50FE8111-F595-4A7C-A121-1452817D25DA","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":"Q7361774$68DC29EB-3315-41F0-BAA4-9AC151D98F89","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":"Q7361774$2A95F622-87E0-4BF1-B34B-8FEA4888B6C1","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":"Q7361774$3A299ED7-0C94-4106-A81B-9D1360E210D2","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":"Q7361774$665E09C3-0E32-47EB-A34B-0F41E9252709","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":"Q7361774$46BE1510-7992-492E-B982-87BADA46B440","rank":"normal"}],"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"0bccfc4e3878b4277c7a473b3780499dea482749","datavalue":{"value":"28603","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361774$6AED653D-862A-4DCB-95BC-C55C53EC6393","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361774$41272C10-25C1-47D8-8842-7A23AE78F791","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361774$1EE67D2D-CC49-4B44-9A6D-D6866C4ACF69","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":"Q7361774$3E940899-FEBB-47DC-954A-D9FDEE152FFE","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":"Q7361774$0173D5E7-794C-409D-AACD-04332AD6B9C1","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":"Q7361774$A1C7DBEE-83C9-4FE5-ACED-39CCDEE41916","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":"Q7361774$1002765D-BF88-4FE1-8C28-BF5012D511AE","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":"Q7361774$7C81A9B8-CBEE-4378-A114-37665EB671F8","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":"Q7361774$A8CFC7F1-888D-4F8C-9AA6-E07A51FCCF10","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":"Q7361774$639AC8FB-AC3A-455E-8BA6-A99ABFFA9728","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":"Q7361774$40905B58-A05C-4ECB-AEC5-509E2F7210CC","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":"Q7361774$55636FA6-0DFD-4AE1-B964-C8C5789EDCBC","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":"Q7361774$2437DFCD-5CFB-45AE-B295-F21078ED7AEB","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":"Q7361774$92BC914F-88AD-4108-B925-C9D47A2FD590","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":"Q7361774$E6738B8B-8F39-4B1A-9B17-36CFCE69C4B1","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":"Q7361774$D9458D72-2315-43B7-A757-097EAA7190E2","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":"Q7361774$15AF0B44-5646-45BF-8C23-F47B61826A57","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":"Q7361774$164BF12B-BF2E-4A87-B463-623D3C260937","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":"Q7361774$040E178D-4B2F-40FE-B150-92CB3C52B27E","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":"Q7361774$B19C59FA-0DEA-4FDC-B1F2-52AFD85FED99","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":"Q7361774$CB6B4D58-949F-47EF-8511-C2F6FBC4A853","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":"Q7361774$3978ADCB-BA11-4A82-A556-010379789C71","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":"Q7361774$6E488109-D31D-4A5F-ACA9-66916C51D1E8","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":"Q7361774$F6850985-56FD-41A2-BE25-7F96FF1D7FB9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formalizing the Logic-Automaton Connection (AFP entry Presburger-Automata)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formalizing_the_Logic-Automaton_Connection_(AFP_entry_Presburger-Automata)"}}}}}