{"entities":{"Q6061876":{"pageid":13196031,"ns":120,"title":"Item:Q6061876","lastrevid":94009334,"modified":"2026-06-05T05:39:38Z","type":"item","id":"Q6061876","labels":{"en":{"language":"en","value":"I/O automata in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7774801"}},"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":"Q6061876$1448A009-3FDA-406E-AEBA-271F91282DD6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"349b073527f4332f9bfb4ffd2f5ca8dac27290f3","datavalue":{"value":{"text":"I/O automata in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6061876$90B76727-1F33-49B1-80D0-3788AAF0522C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7d08f3be8ea2e4d0f62549f37522c383b88055d2","datavalue":{"value":"1530.68156","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6061876$1A1935C3-FDB2-47FA-80C8-9D9AE5739BA7","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"68fcf89c40c853358ec5307ef04afd9acac66393","datavalue":{"value":"10.1007/3-540-60579-7_6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6061876$832229C9-574C-478D-9A63-8E2C45E31AE6","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"bd39997decddd4925a8ef09cbbffc4f41d2b1f00","datavalue":{"value":{"entity-type":"item","numeric-id":670700,"id":"Q670700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6061876$41EB92D7-C60F-4504-9CB9-7AB26087EFE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1d512f15aa7dca5445b4f70135bf8aa67126d08e","datavalue":{"value":{"entity-type":"item","numeric-id":1029814,"id":"Q1029814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6061876$7FEF0DE9-58D6-46DA-BDF3-14F17490D8BC","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":"Q6061876$992D52E3-0FE0-4079-BB96-EBBE771A0176","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"80837e4f107d88dc61f75b08f8b7aa1a590aa151","datavalue":{"value":{"time":"+2023-12-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6061876$14EDA524-F097-4A61-BF49-91A32EB88177","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6061876$C423919D-646D-4251-95FA-4BC0BD74F7CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f100e7e9b912dd320a0f918ece3ef4edbbe567fd","datavalue":{"value":"68M12","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6061876$0473209D-3CDD-4468-A611-C680026B9C01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"35bbdcbda53152c249a7f99650e19b5ef62999f2","datavalue":{"value":"68Q10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6061876$D8F84542-59EA-4241-B8DA-17ACFF4582F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9b78776a56fc28cdd893baa47605a105412b838a","datavalue":{"value":"68Q45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6061876$C8B99E64-4656-4871-9EB7-4753CE8E5CD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6061876$813C439A-7C3A-4C3C-A3D8-A85CBC9997C9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d03dc6b7fd161c7a130bb792da608f2a39876744","datavalue":{"value":"7774801","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6061876$477D296F-D7C2-4C53-8C8B-779B7276F05E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8bf549142b710f01581b24fd28cbb67614316cd4","datavalue":{"value":"theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q6061876$F1B4E94E-7B73-4760-A24D-AEAC8A8DCFD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d7d55f58e4831d77db7a5c91bd18c574bc0f4b78","datavalue":{"value":"transition relation","type":"string"},"datatype":"string"},"type":"statement","id":"Q6061876$BD4240FE-1E06-40E8-AC1A-B46BF762F715","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"50d81425affb13dcf09985fe807cbb0cd8e68cb4","datavalue":{"value":"parallel composition","type":"string"},"datatype":"string"},"type":"statement","id":"Q6061876$2FFAC8C4-9D68-459B-B37F-6F55554AC937","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fc0f7ccfbc5945b2ce0be9c761848993fa261a73","datavalue":{"value":"reachable state","type":"string"},"datatype":"string"},"type":"statement","id":"Q6061876$B0A172AA-C0E1-4523-B1BC-5FD3E2727A72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4481517714437ff63c836d4b49f0e1b5127461c1","datavalue":{"value":"proof obligation","type":"string"},"datatype":"string"},"type":"statement","id":"Q6061876$5E791DA7-C925-4FC9-83CA-088B16CC378E","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":"Q6061876$F3DB4A17-C31A-457A-8A03-4988E168F01C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"df1991cf264e40dfddbdd210563d1e5af82f7f80","datavalue":{"value":"https://doi.org/10.1007/3-540-60579-7_6","type":"string"},"datatype":"url"},"type":"statement","id":"Q6061876$C376ED24-EF14-411A-AEBA-550F8DBBFA53","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"75da2373506084961f0247f0612bb7b82fe303b1","datavalue":{"value":"W1498539321","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6061876$4B7C6B4A-6EDB-4D0F-81BC-3DDF5F5965F9","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5d5978f4bdf14ef5fd8b71ce390dbec5034a1e6","datavalue":{"value":{"entity-type":"item","numeric-id":805251,"id":"Q805251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6061876$5E28C383-29D0-4EAE-AD12-B5E64B3BC615","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf4fab5a4519bb0e4a7392865538dc50ad77fca2","datavalue":{"value":{"entity-type":"item","numeric-id":1193587,"id":"Q1193587"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6061876$CED4B300-9DEB-4C40-BAD6-752CEC901A96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d38293cc06627b45c6840e21e0f7cb4f5b5bf0e","datavalue":{"value":{"entity-type":"item","numeric-id":3814780,"id":"Q3814780"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6061876$9CFB775B-5C37-4DE1-80BA-B9B401D39A90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f4533a245c21db753af232c184081d9b98ae22d","datavalue":{"value":{"entity-type":"item","numeric-id":3833630,"id":"Q3833630"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6061876$5BE3BA66-DEFA-4502-A1EB-86638E0B49C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8f52a135fa2cb9ae673692293b0336967bd5b19a","datavalue":{"value":{"entity-type":"item","numeric-id":5210768,"id":"Q5210768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6061876$251AA6B8-2D87-409E-B6BF-FE391EC4CEEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6061876$A7800CBC-13D1-43A8-86A7-BAAB6BB95CFB","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ce35a2de932330b2b03afc04f0f971a5c9229d68","datavalue":{"value":{"entity-type":"item","numeric-id":4247083,"id":"Q4247083"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fe0b04db5ce6aadf30afda46092e14a59edb83c6","datavalue":{"value":{"amount":"+0.8614306449890137","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":"Q6061876$CF3C2D30-C821-436D-B950-653A6397120A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aba11aea365327050207417956f298bd86563fab","datavalue":{"value":{"entity-type":"item","numeric-id":4239073,"id":"Q4239073"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"237d392d12df73e7e4cb94fc697b69c31e5d1ba1","datavalue":{"value":{"amount":"+0.8134417533874512","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":"Q6061876$6CD99D28-F4F1-4E7D-89CE-081082C5328A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6c8a6ef0e502a74f89c7254887f802cbabb46ede","datavalue":{"value":{"entity-type":"item","numeric-id":4945212,"id":"Q4945212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3667b0b1adacc1286de73bbc993ae8bb9bde9b3c","datavalue":{"value":{"amount":"+0.7591733336448669","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":"Q6061876$2C61E82C-8114-4D17-9384-26C3E0D155A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"23f9964fd8900314ea6c823c5eadf5f579ebe428","datavalue":{"value":{"entity-type":"item","numeric-id":4422092,"id":"Q4422092"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8253b9b191621e626131be502276a430cc507cd8","datavalue":{"value":{"amount":"+0.7580170035362244","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":"Q6061876$BCB6DED8-794A-44C6-A66B-C00FA5ACE3FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e52c6f724532c9e1142453b70c4782abf07c15fa","datavalue":{"value":{"entity-type":"item","numeric-id":1857285,"id":"Q1857285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c5e991417396854c203d746218561ee7cbf8a9c4","datavalue":{"value":{"amount":"+0.7400128245353699","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":"Q6061876$1B593BB8-1B7E-4073-984A-E140F6CE0383","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"I/O automata in Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/I/O_automata_in_Isabelle/HOL"}}}}}