{"entities":{"Q2148786":{"pageid":2159529,"ns":120,"title":"Item:Q2148786","lastrevid":55411876,"modified":"2026-02-17T15:49:58Z","type":"item","id":"Q2148786","labels":{"en":{"language":"en","value":"Verifying the conversion into CNF in dafny"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7547739"}},"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":"Q2148786$7FDB474E-8D34-49FA-A747-3564A0371854","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"80f4988e012d99939f874e8e4715e6619fecab37","datavalue":{"value":{"text":"Verifying the conversion into CNF in dafny","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2148786$788A40B4-6935-452A-971B-F197F52BFA91","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b5cff48eccca08a585b79c8ae3f41640c4b7d998","datavalue":{"value":"10.1007/978-3-030-88853-4_10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2148786$B462E09F-0D3E-4AE1-A6FF-C2D9D079BE34","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"14c40bed66ca53e4bf6d4206b39f03fc0093b090","datavalue":{"value":{"entity-type":"item","numeric-id":2148785,"id":"Q2148785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2148786$72BA8A73-0CEB-4B19-9894-174946DA8246","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"81586982d17a5065a8b3d9d0e0dbbd008e2a773f","datavalue":{"value":{"entity-type":"item","numeric-id":437032,"id":"Q437032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2148786$6A2E1D74-32EB-4E9F-AFD6-100D9F04C142","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c9bbc3a7cbbc97cf0b4e147ebc83c703a8500597","datavalue":{"value":{"time":"+2022-06-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2148786$23E80C6F-B032-4B82-ACA9-291554D11093","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2148786$FB446C2B-6DF1-4601-AD67-7E5CB36AA42A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7f096a475c61423b1f6a6f8e2d83b21627df6af6","datavalue":{"value":"7547739","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2148786$FE879581-CA27-41C9-906F-CA9DA8F52094","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2148786$C16EC8AF-255A-4C72-9883-55C668F2C0A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bb4ac1b3e6590933f07db2ef44e8e77f8844e4b4","datavalue":{"value":{"entity-type":"item","numeric-id":19271,"id":"Q19271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2148786$801BCBE7-86A8-4C3A-B8FF-8F7C020A2711","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"602b32d79a3dd12c7713e80fb0597b8ab4375f08","datavalue":{"value":{"entity-type":"item","numeric-id":16614,"id":"Q16614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2148786$1F8275CF-6930-4263-BEAC-B0A4781F58C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b6da1f42e3d4d28e24ecb68672c28ee0982a60c2","datavalue":{"value":{"entity-type":"item","numeric-id":12950,"id":"Q12950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2148786$EF70C8F9-334B-4C03-ACEA-D71266F803D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"179af68833d4e59c1e0a3c7b1bf054d82b9a6b91","datavalue":{"value":{"entity-type":"item","numeric-id":20426,"id":"Q20426"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2148786$6255D0E7-B27E-4A9B-8861-43F8823DA1E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e022583ed74f81554a39976429e547bb532293f0","datavalue":{"value":{"entity-type":"item","numeric-id":25978,"id":"Q25978"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2148786$37D11E7C-164B-4BD4-847C-BF267B3D3F9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e338912f65cbd77347bbd512933e55736ef58bd1","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2148786$2B5B3C23-C53C-4B33-98D0-9CC2F43471D5","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":"Q2148786$AB5AF885-C139-4F3D-9C5E-BE97D3309D90","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4e5516dafa2c58d3519e92bcea3d7e032c77bf0f","datavalue":{"value":"https://doi.org/10.1007/978-3-030-88853-4_10","type":"string"},"datatype":"url"},"type":"statement","id":"Q2148786$C5193736-A207-4F0E-A829-8ABFB425B198","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"93fb65cd9c3cbfd16b97147903c718dcfe18e972","datavalue":{"value":"W3202267117","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2148786$7B529DE2-5C47-4812-90AB-006F206720D3","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5fce9bfafac21694d8010d9e84d36acbe8cb15c3","datavalue":{"value":{"entity-type":"item","numeric-id":5177337,"id":"Q5177337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2148786$75EB6356-9A3C-42E9-8324-08397C2DA614","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"00c2d672d21d4d5af646f31d9599e67b8b6b153b","datavalue":{"value":{"entity-type":"item","numeric-id":1663234,"id":"Q1663234"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2148786$89B310C6-FA70-43F7-9CCC-5B2B086D417B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"18cdec34fa64c4fe94079af9a70deb0327c75541","datavalue":{"value":{"entity-type":"item","numeric-id":1201346,"id":"Q1201346"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2148786$C1E54B43-633A-4220-8636-3D6F85DA6E16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"60b4dd31c7b9c10eb7577027dd1c4dd424b1676a","datavalue":{"value":{"entity-type":"item","numeric-id":6099609,"id":"Q6099609"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2148786$295C8987-A890-42D0-B197-7EE1C4BC8F5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03cb8e50e6c3bd60a9a9a59407cf30e8e788baa4","datavalue":{"value":{"entity-type":"item","numeric-id":3618853,"id":"Q3618853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2148786$1A024CA4-A3A1-498E-8A78-E79A9B12C8D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea7fb806cb84b37335d37b3efe1590f8bc64cb5d","datavalue":{"value":{"entity-type":"item","numeric-id":839035,"id":"Q839035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2148786$73434273-5522-44AF-B9B2-4497B4898E3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c7cf3ea0d02b0dab18bf43fa3a04332137d66e09","datavalue":{"value":{"entity-type":"item","numeric-id":3224685,"id":"Q3224685"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2148786$A9D9759B-B680-4F9B-A09A-8EE30C313813","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b659b1f6009ab3df1cf8432adfeb1aaf4fe4f69d","datavalue":{"value":{"entity-type":"item","numeric-id":6060676,"id":"Q6060676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2148786$DA228BB3-8111-4245-BA88-633942DBD734","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f24266047ac8ffcefe32630c940ffdb70489bec0","datavalue":{"value":{"entity-type":"item","numeric-id":2891429,"id":"Q2891429"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2148786$C05E2376-3C0F-48FD-8C29-60CC51799844","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f769fe6ef8dd71200eafe07970c69907f40fbcb","datavalue":{"value":{"entity-type":"item","numeric-id":5179007,"id":"Q5179007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2148786$F375A77A-5AEE-4B91-B373-ECF6FAD89412","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c6b871d25a3f2bcc10ef5d12d2a6df59054c7c5","datavalue":{"value":{"entity-type":"item","numeric-id":5604434,"id":"Q5604434"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2148786$C1F178D4-8470-4F71-B6E1-5EBC2DF006E1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fe6964fbba4b601ab17eaaead2b873b279a5f70c","datavalue":{"value":{"entity-type":"item","numeric-id":3655207,"id":"Q3655207"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7e59aa74aeb28ca62e47e6116c3bc73c54129c8a","datavalue":{"value":{"amount":"+0.7396693825721741","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":"Q2148786$740D3275-BEA1-410A-883C-B3C59473E0D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5a9f910c2ba51b2ff070ba9944a4c3652961f4cc","datavalue":{"value":{"entity-type":"item","numeric-id":2307626,"id":"Q2307626"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"847c7cdb2684d0445b6e7db3f3e408dd9f932820","datavalue":{"value":{"amount":"+0.7374929189682007","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":"Q2148786$74C47294-5C36-4968-8E09-5CFF12A40B6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e8992563a0f1abc0bc8dbca2c5cc6a772bd64745","datavalue":{"value":{"entity-type":"item","numeric-id":3645586,"id":"Q3645586"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3441439e00913bbb28af3bb82988a71ca2bc5920","datavalue":{"value":{"amount":"+0.7089125514030457","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":"Q2148786$03BC8E86-1FEE-4744-A2B5-E37612653A73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"15ddb98d66127a5f5d86c935e6e2a41218e14092","datavalue":{"value":{"entity-type":"item","numeric-id":6496630,"id":"Q6496630"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"11f021394889e1ce4ca42cdf8f61d04a4c89e29b","datavalue":{"value":{"amount":"+0.7027006149291992","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":"Q2148786$73D6681B-7291-4494-BA65-5FF83491C4C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4ef8de85a063b189e894d4f314de10fb7741189a","datavalue":{"value":{"entity-type":"item","numeric-id":1367074,"id":"Q1367074"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"50e383f45c5dff1fe9d79909c6d8bf7c6d256c31","datavalue":{"value":{"amount":"+0.6974997520446777","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":"Q2148786$9D02F26F-93C2-4018-B93D-F99B1EB9657E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2148786","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2148786"}}}}}