{"entities":{"Q912592":{"pageid":914440,"ns":120,"title":"Item:Q912592","lastrevid":65325087,"modified":"2026-04-12T01:48:15Z","type":"item","id":"Q912592","labels":{"en":{"language":"en","value":"Proof systems for satisfiability in Hennessy-Milner logic with recursion"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4145302"}},"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":"Q912592$648937B0-EF72-412E-91EF-5DADDC66448A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"98fa9a08d5b0a894fe3636f26c549529968b8a04","datavalue":{"value":{"text":"Proof systems for satisfiability in Hennessy-Milner logic with recursion","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q912592$17589438-71DF-4205-861A-F9230BB79A1B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ab1fb1d4d3ed9231288226286f82b890c4534470","datavalue":{"value":"0698.68014","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q912592$BFF53921-2632-4C56-A28E-EEBA70A1C3F2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"eeaf53c11a32f70be337607ddb9c849c4b29c425","datavalue":{"value":"10.1016/0304-3975(90)90038-J","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q912592$7FE807DF-9423-4889-B0B8-E47F29B97E3C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7ac8acc0ee38d6ade72f0d112f1c054cc98c3505","datavalue":{"value":{"entity-type":"item","numeric-id":808272,"id":"Q808272"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$610C3394-885B-4A91-B547-35435EB66760","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$60675807-3060-4330-90B7-78D66928CB0B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"70d2fbf8bcd48a5ca1ac752985098b379d0dbb65","datavalue":{"value":{"time":"+1990-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q912592$DF614DE0-7885-4C82-9161-C26AF85D9154","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"8f20d21d3028cfc47fa42b6baf05620634e6cb1a","datavalue":{"value":"See the review in Zbl 0647.68012.","type":"string"},"datatype":"string"},"type":"statement","id":"Q912592$7BD8EB0D-1A43-4155-8500-2CF54FB88530","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q912592$9DB78012-56CA-4FAD-906C-7A45F80E71F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q912592$E846C0D5-DEA7-4B5B-956E-BC89D1BB829E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ec3769495799f08479987ac368adf64f125a2b66","datavalue":{"value":"68N25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q912592$D2731EA5-4D70-436E-9F24-2808AC3B06CC","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"894733cb87ccc7ec9c8f35f88156eec0d70199cc","datavalue":{"value":"4145302","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q912592$90243007-AC44-4232-844D-503BC36E4F11","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a5073c0a5fb9f470d8e418aa70e3fb4e6b7562d1","datavalue":{"value":"Hennessy-Milner logic with recursion","type":"string"},"datatype":"string"},"type":"statement","id":"Q912592$A4BB99E8-3755-497E-8298-F91EF73A0674","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c884a3637b5acf5b2d045b6f947eeb47f8529fed","datavalue":{"value":"minimal interpretation of formulas","type":"string"},"datatype":"string"},"type":"statement","id":"Q912592$8A6B1A3F-EDD6-4119-AFE2-668E9831E186","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0f43b5d8c0ae8848835abc81341e946063dd5eca","datavalue":{"value":"liveness","type":"string"},"datatype":"string"},"type":"statement","id":"Q912592$AE8893BC-BBDC-47D6-A78E-371F10D6F52A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"82bf66ded88b46580ccc3aa8cf0c723688355f1a","datavalue":{"value":"maximal interpretations","type":"string"},"datatype":"string"},"type":"statement","id":"Q912592$F54ED289-2A13-4EB6-843F-4F2178D70B92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d584e359576a00f85def0b98465ac7707c1c7959","datavalue":{"value":"safety","type":"string"},"datatype":"string"},"type":"statement","id":"Q912592$E1471F18-EAA6-4738-8451-4756697A5E21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cc028f491ca3cd6c7521dd6f6f17a35cdad54a6d","datavalue":{"value":"proof systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q912592$40AD852B-C0BD-4155-BBE5-1B383204180E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0892b6e9e2c60e42b1cfda9d359fd5f0302a7db0","datavalue":{"value":"prolog","type":"string"},"datatype":"string"},"type":"statement","id":"Q912592$2DFFF76C-A202-400A-8429-691ACBB72741","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eb79299daf8f29391d6c8a2b4222865ffe474551","datavalue":{"value":"decision procedure","type":"string"},"datatype":"string"},"type":"statement","id":"Q912592$E91BE569-AA0A-4297-8CB9-A69F61B03435","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7dde8a3acbf5a51e4a3d382793141716073998d1","datavalue":{"value":"verifying","type":"string"},"datatype":"string"},"type":"statement","id":"Q912592$4D27F256-BE25-47E1-A4D9-271BFC77CA0A","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":"Q912592$EA3129EC-E3D9-4FDB-A8EE-54BC61FC595B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ef4165cdc01f313b12040c9657a14ef341fa2d9","datavalue":{"value":{"entity-type":"item","numeric-id":789895,"id":"Q789895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$AC8A52E7-BCE6-4531-88F0-5B51274D5A9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8f64d7ebfc288a54139c42ec42a069a71b552c77","datavalue":{"value":{"entity-type":"item","numeric-id":802306,"id":"Q802306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$5451EBC8-156D-43A1-A8B3-B1E7A7C90E66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5d4a6a227c79868bd9b5023884039f04b712af5","datavalue":{"value":{"entity-type":"item","numeric-id":3321470,"id":"Q3321470"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$917A2A19-2BBB-4258-AE2D-9C225E95E356","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2bb9167a15a02d50f8531d7407b8aced98fa4dc9","datavalue":{"value":{"entity-type":"item","numeric-id":3336675,"id":"Q3336675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$9115CE12-C05E-4D0F-B7D3-9E9E04B6E197","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"18f169d1d0deaac447dc236e44ef2dcda7febabf","datavalue":{"value":{"entity-type":"item","numeric-id":3343432,"id":"Q3343432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$2166CF60-C883-414F-866A-D2861BBADF79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d67b4457709012c8ba92c99783e7198904e2138","datavalue":{"value":{"entity-type":"item","numeric-id":1080653,"id":"Q1080653"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$0A0EE579-DD2E-4C50-B3BE-73960EB71BCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86294c98630b181a5f8eb3c9fb0c21ddb5c467c7","datavalue":{"value":{"entity-type":"item","numeric-id":3719799,"id":"Q3719799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$527DD82F-6C10-4EEB-A064-FEAED76A1515","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf8ebc11e5152a7aaca233f3b6037de5f36fc738","datavalue":{"value":{"entity-type":"item","numeric-id":3766826,"id":"Q3766826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$BA86BEBA-2BB1-4477-8A55-6C5A6637207B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58569cfcb63db51abd33ef3dfc3dfca274845b33","datavalue":{"value":{"entity-type":"item","numeric-id":4744245,"id":"Q4744245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$BD0E1411-D2D3-4377-918F-4E03A3A41F48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03e4c3801010a4bee6d03ee81a6a1a5d94252213","datavalue":{"value":{"entity-type":"item","numeric-id":3792217,"id":"Q3792217"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$58B43194-6C57-491A-B0E7-ACCA5557C776","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a358a7e0cfe385397b6ee7256bfda7621794063","datavalue":{"value":{"entity-type":"item","numeric-id":3948585,"id":"Q3948585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$630502EE-769C-44AB-A1A5-5C5877C611CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"60da585cac100a31c125360c9cbd2d207cbfe7df","datavalue":{"value":{"entity-type":"item","numeric-id":1148667,"id":"Q1148667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$6EE00445-04B8-469F-A38F-8EB2752E11D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5512372227b73d51e646f93b09237b2a8d0d7e21","datavalue":{"value":{"entity-type":"item","numeric-id":3929062,"id":"Q3929062"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$3D9F3496-F95A-421A-A5BD-D4E2E58564C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7f190ae2fde923a1f547028868c0453492060bbe","datavalue":{"value":{"entity-type":"item","numeric-id":1050111,"id":"Q1050111"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$89CFC418-516C-451D-B371-45052E4966ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8090368e0e1c2bca919f00e317d355cf1aa8d484","datavalue":{"value":{"entity-type":"item","numeric-id":3907077,"id":"Q3907077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$B38F10DE-CBB1-409B-97BF-84678A0873CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66d102eeedc0eb3199ce5808a637283d2af0ab5d","datavalue":{"value":{"entity-type":"item","numeric-id":1878719,"id":"Q1878719"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$FEE286D2-CF93-41F5-B575-9875EB6E375F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f45f552829e448fdb1f5d0c5585c08bd5972555","datavalue":{"value":{"entity-type":"item","numeric-id":3694687,"id":"Q3694687"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$FEB38C86-FEFA-4AA6-A9F1-DB13AF0455AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c74cc36d67bfa05327429ce9b5a018fb52a35f57","datavalue":{"value":{"entity-type":"item","numeric-id":1060006,"id":"Q1060006"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$B5218786-7B0F-43D4-8AB0-E6899F268585","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8612e31926aa2a0d7d9b618cb86ed3ed06555ee3","datavalue":{"value":{"entity-type":"item","numeric-id":3677160,"id":"Q3677160"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$624045F8-A63F-4D56-92EC-3BF25E068497","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a2b3202d0a36de134fc126e958e9cdfbcf16cdd7","datavalue":{"value":{"entity-type":"item","numeric-id":3707371,"id":"Q3707371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$E0922DB9-E2E5-4676-838E-3DEB645C8F59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a50bedffce465f6dca8b90f3cc27a20109b172b","datavalue":{"value":{"entity-type":"item","numeric-id":578896,"id":"Q578896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$C18E118E-926E-496A-8866-087EE9F0FDD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e320d5ab20d9378e83c08a862b63bf2725892d4a","datavalue":{"value":{"entity-type":"item","numeric-id":2653567,"id":"Q2653567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$8C7A2ABD-AC23-409B-A670-B846F4257174","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"83b974dd0ec307a829857bb6b377f86a0c8fb368","datavalue":{"value":{"entity-type":"item","numeric-id":3683529,"id":"Q3683529"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$53C574B0-0F92-486A-8512-65F9DCEAFC1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"af7bd2820fe3f1cd359c9a558d9702d9320e1bcc","datavalue":{"value":{"entity-type":"item","numeric-id":3711741,"id":"Q3711741"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q912592$46986195-C368-4CDD-A689-BDF9639D9DA2","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"1099d1ffb98e32040f846eb9a1bbda6b8aa1d167","datavalue":{"value":"Q128111591","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q912592$50240FD9-21C5-4E99-BEBC-6ACA2F4D6113","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proof systems for satisfiability in Hennessy-Milner logic with recursion","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Proof_systems_for_satisfiability_in_Hennessy-Milner_logic_with_recursion"}}}}}