{"entities":{"Q3183549":{"pageid":3194257,"ns":120,"title":"Item:Q3183549","lastrevid":80028308,"modified":"2026-05-06T15:16:35Z","type":"item","id":"Q3183549","labels":{"en":{"language":"en","value":"Liveness Reasoning with Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5618527"}},"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":"Q3183549$E17A10B0-759A-4BF1-AB13-D8F486F5B3C7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"33e6d147e8d110010120f65903a645424e2fd0ec","datavalue":{"value":{"text":"Liveness Reasoning with Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3183549$CA852A93-BE5D-4FEE-BF45-F4CAD7FC0CEA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f4eea7a5e71888b4c0986badbbf3b72da962c380","datavalue":{"value":"1252.68198","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3183549$65DD649C-8E01-4589-A099-3466709385AC","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"fa49904d5c0d28248df7a55d0431e2bfa39e834d","datavalue":{"value":"10.1007/978-3-642-03359-9_33","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3183549$7929599B-E83F-4687-B313-F200569E5AE8","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7c7dce4e2fbe3498a35a8eed98f5b00e9a678bda","datavalue":{"value":{"entity-type":"item","numeric-id":3183547,"id":"Q3183547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183549$4FEF972D-2D92-4883-927A-F76772D47347","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bbac2e5186b687bd5230ec7d5103735ddf73d9d0","datavalue":{"value":{"entity-type":"item","numeric-id":3183548,"id":"Q3183548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183549$EC29282A-77AC-4B38-A611-71401752D16F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8c1db257e626cb76e16153e74052c741125ca701","datavalue":{"value":{"entity-type":"item","numeric-id":2113967,"id":"Q2113967"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183549$F137C438-F4C6-4F00-B999-1B929EAACB2F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183549$A4D339F9-80AD-42BF-9D82-0E42CAC1CA4C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4b03fe0d32567f363cc3207214473a7371265cf3","datavalue":{"value":{"time":"+2009-10-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3183549$092804A2-2089-4142-83CB-2687D67A96BB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3183549$FD8EF70D-368E-4F5B-A766-6E5BEE959CBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3183549$BD641075-F302-4F62-8009-42CED0EB39F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"0dd26fa594336927a7a04e8147a405d69e5da239","datavalue":{"value":"68Q87","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3183549$70783399-43E9-483A-95A2-BB689807DA3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3183549$577EF7CE-038E-447C-9036-64F0E36A9233","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"14f14e71615f75db74c10f42ae436ea2f3b27837","datavalue":{"value":"5618527","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3183549$B5043184-8F30-4B3E-B00E-47F601351A26","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"95c125023026c165b99458d4ca58a279f82325ee","datavalue":{"value":"liveness proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q3183549$C8B3FC76-92D2-40C9-9ABA-0F9BD8C3962C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"56247b00b41b349feeb648843ccd1b66e4b2dcc1","datavalue":{"value":"inductive protocol verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q3183549$27CCB1A6-B31E-439C-9EFC-CB01D91AEC6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d96e0ed81d2469df094a87982571c9ec66d7dd18","datavalue":{"value":"probabilistic model","type":"string"},"datatype":"string"},"type":"statement","id":"Q3183549$442BC43C-2C3F-4403-BEB5-56E9D034DF05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dbd6d8c9e586388d37949289c67ad427d8f69de2","datavalue":{"value":"parametric fairness","type":"string"},"datatype":"string"},"type":"statement","id":"Q3183549$A1E70639-03B6-423E-A6A2-561B05A62AF7","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183549$A3C8DBC6-021A-479A-A8A4-7916D7EEC7B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183549$55BCD297-5E83-49EF-AB8A-718B2F2FD0B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b222922e2b373ab7fb2b7a049f9de07c755ee255","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183549$05C70130-7C8F-455E-8864-02C6A3BB2958","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":"Q3183549$55A5E8FF-6ED8-4FDF-9BA3-BCC9E65DDE1E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7b12ec2e20a6dcc5d553ef4f3aa01a8233bbb167","datavalue":{"value":"https://doi.org/10.1007/978-3-642-03359-9_33","type":"string"},"datatype":"url"},"type":"statement","id":"Q3183549$6DE1171A-0BB5-4536-AB8A-CE4CE5115E52","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0dae94dd6b511ec632d44fab1b67e1cde32c4ddd","datavalue":{"value":"W1485043971","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3183549$B7D7EFA7-3D88-404D-85D3-8C1EE1100EC9","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a2b1afdfd50f7f4404e431384ee3957a9cf5c28","datavalue":{"value":{"entity-type":"item","numeric-id":1176248,"id":"Q1176248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183549$7737AC38-A4BF-4E0F-A118-A9A7D964A2F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"288242718e3c927db37f8dbbb0c11f4c7a610e5e","datavalue":{"value":{"entity-type":"item","numeric-id":1803654,"id":"Q1803654"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183549$9FF9FEB2-30A8-4142-8DE1-896C943C593C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c321453b0f983f90188afe93371af650492014ce","datavalue":{"value":{"entity-type":"item","numeric-id":2583540,"id":"Q2583540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183549$EC42A966-D484-436A-B818-7780C2B37112","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e6bfe4bab7fc131fec25ca36162500a7f2cd2576","datavalue":{"value":{"entity-type":"item","numeric-id":840697,"id":"Q840697"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183549$6A29010D-6678-47B3-8E72-BA42F75C3B61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183549$A76FBC87-4DF0-4FBB-A658-89A61A61A63B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a59763b3fb25129051745803dae70f5cf79103f8","datavalue":{"value":{"entity-type":"item","numeric-id":4484343,"id":"Q4484343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183549$248DB282-016D-4FFD-BFC3-D45DC6823309","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc18b84f53cfdc559b4d296e04ba30186fce5df8","datavalue":{"value":{"entity-type":"item","numeric-id":5464655,"id":"Q5464655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183549$0411E440-26FF-4D64-97DF-EB7EF3B0E1B3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0af53033f2ed04a6f7f1b9d859620013b091db29","datavalue":{"value":{"entity-type":"item","numeric-id":2754094,"id":"Q2754094"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"211d43d931a56cac83e0bbcafa7b68b237681101","datavalue":{"value":{"amount":"+0.7302311062812805","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":"Q3183549$B55F4C8A-F2F6-4380-B42A-DDB0522AA836","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eed48a341a7df4501e55b4d17c90134cba58846c","datavalue":{"value":{"entity-type":"item","numeric-id":3613081,"id":"Q3613081"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"211d43d931a56cac83e0bbcafa7b68b237681101","datavalue":{"value":{"amount":"+0.7302311062812805","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":"Q3183549$3AD964DB-A3A3-4E88-9F77-A35A26080333","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8d21ee0f204110533d888447534135dc49ebd253","datavalue":{"value":{"entity-type":"item","numeric-id":4791836,"id":"Q4791836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4f3d06349073709ca91e1cb79be45d1c0a840393","datavalue":{"value":{"amount":"+0.7211462259292603","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":"Q3183549$10F3330B-5699-42B1-9305-296D1E275C3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"05c933e70af1e68238332006e9e0a576fbdc38ad","datavalue":{"value":{"entity-type":"item","numeric-id":5901911,"id":"Q5901911"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9f065b76b178f44c9878734e643cdc1608f52d9b","datavalue":{"value":{"amount":"+0.7204546332359314","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":"Q3183549$0B5936D9-0516-47F5-9B6D-7C2CD440D118","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d3a8cced7c0637e7503264498c6c8710b4e669e3","datavalue":{"value":{"entity-type":"item","numeric-id":4417853,"id":"Q4417853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6b6803a418febe8240150893a26639fb6126de4b","datavalue":{"value":{"amount":"+0.7168920040130615","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":"Q3183549$BC8523A6-1887-4589-B829-D5E5E5DF0C48","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Liveness Reasoning with Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Liveness_Reasoning_with_Isabelle/HOL"}}}}}