{"entities":{"Q1193598":{"pageid":1204347,"ns":120,"title":"Item:Q1193598","lastrevid":66455676,"modified":"2026-04-12T10:11:25Z","type":"item","id":"Q1193598","labels":{"en":{"language":"en","value":"Proof systems for infinite behaviours"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 64879"}},"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":"Q1193598$25FC9CF3-AD15-4172-9F98-A4FF665EFCA1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"471779d6961c0b8e2b7fb176c639d01e2cd561c5","datavalue":{"value":{"text":"Proof systems for infinite behaviours","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1193598$44511E73-BD82-432A-855C-7D24C5D59B1B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"16eff4f4ae54b4c5eea7da96bf9485fb20415860","datavalue":{"value":"0765.03016","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1193598$5C5861E0-A412-48B4-803B-E3E5AF155EC5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"eb7f236d5507a474e467972f16afd0fc86cb55e5","datavalue":{"value":"10.1016/0890-5401(92)90029-F","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1193598$A69FEC05-EA81-4F62-90EC-49A2F25D0F6E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"271829170669ce43b1b4f10856578a74e1f3e05f","datavalue":{"value":{"entity-type":"item","numeric-id":557785,"id":"Q557785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193598$D1CD8A33-F46D-4898-9915-A3B593AF98A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a146557611ef4f94fc6e55637e62191fe9768511","datavalue":{"value":{"entity-type":"item","numeric-id":1119626,"id":"Q1119626"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193598$DD622738-C6F6-4854-9413-2CA015CB487F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"fa2d1ad91af9619c8dd37ab889fe279a84c4057e","datavalue":{"value":{"entity-type":"item","numeric-id":259032,"id":"Q259032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193598$D9AECB36-FAD6-4F5B-9E14-4F74CCF07C48","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5fd62271fe98c7ff9916cafed51cf35315eeeb31","datavalue":{"value":{"time":"+1992-09-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1193598$13D61982-0B89-4E42-A35B-44AB8453E196","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b095763d42c83f39c3601f4d671fa5f4c0cc4c67","datavalue":{"value":"The paper suggests several generalizations of testing to \\(\\omega\\)- behaviours of communicating processes, analyses the logical complexity of the testing equivalences, and establishes on that basis a connection with proof systems. Section 2 supplies infinitary tests with infinitary results for the equality of linear \\(\\omega\\)-behaviours in pure CCS. Section 3 contains an introduction to \\(\\omega\\)-logic and recalls the strong connection between \\(\\Pi^ 1_ 1\\) and the \\(\\omega\\)-rule. Section 4 establishes a mutual reduction between \\(\\Pi^ 1_ 2\\) formulas of arithmetic and formulas \\(p\\approx q\\), where \\(\\approx\\) is the equivalence over CCS programs induced by tests defined in section 2; it is concluded therefrom that complete systems of \\(\\omega\\)-proofs for \\(\\approx\\) cannot exist. Sections 5 and 6 investigate the logical complexity of two alternative equivalences based on families of finitary resp. infinitary tests with binary results, namely the equivalence of De Nicola and Hennessy resp. the equivalence of ``indiscernibility''. It is shown that indiscernibility is not \\(\\Pi^ 1_ 1\\) and has therefore no complete system of recursive \\(\\omega\\)-proofs, in contrast to De Nicola and Hennessy's equivalence. Section 7 contains an elementary introduction to Girard's work in \\(\\beta\\)-logic showing the existence of complete systems of recursive proofs for indiscernibility and for \\(\\approx\\).","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193598$740CE4C5-EB19-4EF9-B1D2-7478A1E3AE8D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1193598$E5C3E8B9-37BE-41F2-836F-A1ED713EA2D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"35bbdcbda53152c249a7f99650e19b5ef62999f2","datavalue":{"value":"68Q10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1193598$DAB2AC98-9A42-498A-A9DC-C790B669513D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2d81d16ea3fae7b6c0af15f06192f63e4215f03e","datavalue":{"value":"64879","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1193598$C6C58FF3-0794-4C7D-9445-0235B21A6C0D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6d9c2e1f00facc619242af9af43a4aae006f38ad","datavalue":{"value":"transition systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193598$E4AC88D3-3526-4D00-A1DC-40BD9F2DC7D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"161f1979f82c6f3bf19de2ed87a3ed653942d0b3","datavalue":{"value":"infinite behaviours","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193598$F3EC38F2-6C2F-4D56-9DF4-5B9C8C069305","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a813fd0e4aef1fda5e8e7d4b77b02104337d96e6","datavalue":{"value":"undecidability","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193598$D248BA42-5D00-4E05-8898-93A2B972D690","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"69ea5b69d0be7e1d5aded4795bf1838bfcba2141","datavalue":{"value":"degrees","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193598$66AAF0BD-50E8-49C9-B47A-F43B236B5705","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ff3cd15631da7cd733265945973b6ab3cbc1ce56","datavalue":{"value":"\\(\\omega\\)-behaviours of communicating processes","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193598$33F2C0AD-4E54-4CDE-97D0-E8A56F29888A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8582c9c9734eff214e5b5db65e867b5c228e500c","datavalue":{"value":"logical complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193598$310429B9-FEF1-4EDB-BA14-1E3597060C4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"112db79766d626b9071a4137b86060d0c7b63128","datavalue":{"value":"testing equivalences","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193598$60127680-579C-41CA-86CD-DAF7C15CA40D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cc028f491ca3cd6c7521dd6f6f17a35cdad54a6d","datavalue":{"value":"proof systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193598$48D94DCA-6A65-405C-9639-E89AAB62B7F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"29b99469f015af7a15f51eef633c1e2afde5c3b0","datavalue":{"value":"infinitary tests","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193598$126C531F-8066-4B7C-8C22-0299CA694094","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"44624ed27d93594c9d7e63e70f05fe788d938f52","datavalue":{"value":"\\(\\omega\\)-logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193598$FC9B1FF2-E4CC-4E13-9E96-D1C728850F4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e5b7eebc708f22c1df35973020efdb22b926daf1","datavalue":{"value":"CCS programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193598$DF57F7EB-0A29-418C-A3E6-F0B24725524A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f32defd18175082be6356fdfd3d64a8dd373b625","datavalue":{"value":"indiscernibility","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193598$2AEADFDB-2E06-4DA3-B5B8-BB92862291EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7ff7a4d147c00bc5d11e0ee62a1815bba64f0dd9","datavalue":{"value":"\\(\\beta\\)-logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193598$9C598398-D0A4-49F1-BBC9-8B47974E33BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b876b731fa4348dd311cd22fdb1c10ffda08aed3","datavalue":{"value":"recursive proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193598$0640D962-517B-434C-B60C-C947ECE4BEF8","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":"Q1193598$09A59413-F544-48A0-A890-49E4819413D0","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"dfecaf532c2be9e3f2c25c4983153b3ac961d76a","datavalue":{"value":{"entity-type":"item","numeric-id":4053647,"id":"Q4053647"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193598$897D96AD-61E5-4946-B347-060D250F71CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3d9a77f6122ef7af5ab514b68940c8a73f1674b8","datavalue":{"value":{"entity-type":"item","numeric-id":4728280,"id":"Q4728280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193598$E84CF29E-8C4F-4395-9D89-62E7D531ADFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0afad04665e6ad389173b42510f5293107d812ce","datavalue":{"value":{"entity-type":"item","numeric-id":4721642,"id":"Q4721642"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193598$45A68945-6C5C-4B0D-B1FA-9E8973FCBA9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a88e06b186a83bc1abbde69c4cd83326d414709","datavalue":{"value":{"entity-type":"item","numeric-id":1348526,"id":"Q1348526"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193598$88E87CD1-E955-4A2B-91D6-26C530EE2111","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c97a7b6faf562e1c5b09260906a1f00f35a77b0","datavalue":{"value":{"entity-type":"item","numeric-id":3773876,"id":"Q3773876"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193598$D73E4FE2-6AFE-4A10-8944-BB33E8F0946F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"51cc071a63d7e2256ef91f1a5892cb76da195303","datavalue":{"value":{"entity-type":"item","numeric-id":4128539,"id":"Q4128539"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193598$48CE2B19-62D9-45A4-816C-EA3C8C99C46B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b17989129559e41cfb06edc0b79311d4fa6022df","datavalue":{"value":{"entity-type":"item","numeric-id":3960844,"id":"Q3960844"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193598$9A721207-E561-4EAE-BB04-8F36262E6122","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0e5963ea28037dec9fe662323c70cab231400aeb","datavalue":{"value":{"entity-type":"item","numeric-id":3334070,"id":"Q3334070"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193598$B016489E-FB77-4230-BAFD-28CB51EAB40F","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":"Q1193598$A39A9A1A-DC24-46A5-8C1D-082286385EC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1f0c3549d5b8155ce7e1ff13ae07abb3b6da851","datavalue":{"value":{"entity-type":"item","numeric-id":5322161,"id":"Q5322161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193598$07727871-BEDC-49B1-8489-67FC1512D812","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":"Q1193598$53FEC62B-B269-43C0-9F5A-2D67FF1A4E87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c516c05f43b68537a5c72310725dbfca17470f25","datavalue":{"value":{"entity-type":"item","numeric-id":580961,"id":"Q580961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193598$10F2CD16-D1D9-46EC-8F7B-6D9A0C5772C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9635365b0780328d7ae22bc69b462e7144999d03","datavalue":{"value":{"entity-type":"item","numeric-id":5573961,"id":"Q5573961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193598$B513625F-2E73-48EB-B7CF-F60394B4F30F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5bdd3fae2022f43de935ebaecb39134fa6c0b8a4","datavalue":{"value":{"entity-type":"item","numeric-id":4143283,"id":"Q4143283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193598$EB0257D6-2471-4E7E-947F-1BEA541437E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"036d0859b71a1d830cc563ed0c4c5c60eed5cec5","datavalue":{"value":{"entity-type":"item","numeric-id":1119627,"id":"Q1119627"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193598$F607582E-38D0-40D7-B789-559AA60E9837","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"81ff7f27c217304396ac268c4f3f646f59170b52","datavalue":{"value":{"entity-type":"item","numeric-id":1348526,"id":"Q1348526"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"09526020182fe61fa38032eac430bf32d6fadc4f","datavalue":{"value":{"amount":"+0.7741553783416748","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":"Q1193598$C74E252A-1147-44A4-8BD8-1AC25F9DC9B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"32fb670341eec387190db86572e6609f071e0654","datavalue":{"value":{"entity-type":"item","numeric-id":1815341,"id":"Q1815341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d13487d57bbea59191b200293a0a256e360bcef4","datavalue":{"value":{"amount":"+0.7486667633056641","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":"Q1193598$DD68698C-918C-4A03-93B9-4E6B874A583D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"516bd943972c6cbd6b22be160d797dc7e9735399","datavalue":{"value":{"entity-type":"item","numeric-id":918211,"id":"Q918211"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aab2c9ba04b805df6029ede5499ed44434c9197f","datavalue":{"value":{"amount":"+0.7479431629180908","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":"Q1193598$419552DF-B4F0-4637-AD40-0C8A0960C030","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d1f06a554b506c9e5f41a5bfffab7a987a3aa511","datavalue":{"value":{"entity-type":"item","numeric-id":4219039,"id":"Q4219039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"187d6cd50b28157da6711f41dfbd5416f422a36a","datavalue":{"value":{"amount":"+0.7432695627212524","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":"Q1193598$7F6A7959-2E1E-4177-A847-901FB05EFFAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8631275ad52acd3616dd087952e119a419a7cc32","datavalue":{"value":{"entity-type":"item","numeric-id":3702497,"id":"Q3702497"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cee8c6bbef41517a7ec1f6554bf45ae3b04adbd1","datavalue":{"value":{"amount":"+0.7411918640136719","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":"Q1193598$5A0D75F7-FEFE-42D8-8990-06B0EDE2FC66","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proof systems for infinite behaviours","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Proof_systems_for_infinite_behaviours"}}}}}