{"entities":{"Q2758043":{"pageid":2768782,"ns":120,"title":"Item:Q2758043","lastrevid":47708971,"modified":"2026-01-02T12:09:17Z","type":"item","id":"Q2758043","labels":{"en":{"language":"en","value":"An axiomatization of full computation tree logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1679317"}},"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":"Q2758043$62740EC9-6665-44DB-931B-9EFB520969AF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"cd935539cee82161679ebb088be9618f8b12e9fc","datavalue":{"value":"1002.03015","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2758043$6F88C26A-D4F3-4B9F-852E-7E13D0490088","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e6078ba2ae3ae13e6b0ff969dbee070b7a8d5e89","datavalue":{"value":"10.2307/2695091","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2758043$D62067D9-0EDC-429E-B9A2-5A9715597883","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"8ba0e16ec554a6a916fa7a31c1f3db10e36701a3","datavalue":{"value":{"time":"+2003-01-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2758043$22A3E198-AD03-4C19-800C-D2DF213616AE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"60652406d6f4d6cf7106947ea3a4a1aca2899c5e","datavalue":{"value":"http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.666.2813","type":"string"},"datatype":"url"},"type":"statement","id":"Q2758043$B1D446DC-6847-41B2-BC95-B336F89A71AA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2758043$82ECCA79-B3A5-4FB5-8961-C2A7C2A97641","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2758043$02927249-025E-4F32-A95F-2BCC35D153E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2758043$7ACD60DE-3CB9-4DE3-83EE-79153B203B85","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b4001e9487b77e29eae655ed84ec7fa6de0fe587","datavalue":{"value":"1679317","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2758043$6973E259-8D33-48F6-89D4-98DFFADAF3F8","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a4a6f11756e1720f07cda5a080ef0476786d909b","datavalue":{"value":"temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2758043$325855A7-EC68-402A-A576-C9DC673A1784","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"565eb5fa257250dd3db6d5bd7392e096f22437ca","datavalue":{"value":"full computation tree logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2758043$1D2A02CB-9C13-4628-BDD7-09130DDC916D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c4978f2c4d263ef258ed0ffc576a325d510c4d8","datavalue":{"value":"axiomatization","type":"string"},"datatype":"string"},"type":"statement","id":"Q2758043$D42BA857-E53C-4A74-BA31-7648EBE581B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b57c832f4b21b0ae9151495d8a971f39ac6c1824","datavalue":{"value":"validity","type":"string"},"datatype":"string"},"type":"statement","id":"Q2758043$DF3277CB-A135-44A1-91C4-ACE480211C04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"252f9f9ed9fe8ca406cc19fba38a46c0414791ee","datavalue":{"value":"satisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q2758043$8CE4B68B-4853-4DE0-9821-3F76935D84B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d7bfc11de8cab95fd6af201970bd9d16d39bbd0","datavalue":{"value":"semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q2758043$5BB19AA6-E254-4329-ABF1-69C210D5EF76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"000d054838ba79f1c83227281d29722f07d85a76","datavalue":{"value":"Kripke structures","type":"string"},"datatype":"string"},"type":"statement","id":"Q2758043$58300E3B-4986-444E-9A42-8439E7DCE1AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f6816fdf79dd11ac09d9af4886c02baab03d2cf9","datavalue":{"value":"completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q2758043$2CFA96A1-17BC-4BD1-8CA1-039A7A83A243","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"22c3c5a22fb3da755e2e8fb1d94c251a072f6ebc","datavalue":{"value":{"entity-type":"item","numeric-id":790946,"id":"Q790946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2758043$1501CC37-993A-400E-8F73-5C6399F83031","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":"Q2758043$DDB55A85-E566-4AEF-88AA-289ED4593083","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"baa99071de1a92679edcc2f9a77bf662043377da","datavalue":{"value":"W2153737593","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2758043$76A481DF-7ED1-4D1C-ACF9-91DF17F460A8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f834c4739881bb3c01e4c1fdcef0e2fa69aa132","datavalue":{"value":{"entity-type":"item","numeric-id":1197983,"id":"Q1197983"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2758043$FA62A539-CFD0-4F39-8F03-4FA3C328ACC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f65004c290e3f0ea315a4c52f604a40c6749f75","datavalue":{"value":{"entity-type":"item","numeric-id":1155599,"id":"Q1155599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2758043$FFE572A0-B160-4375-96D7-F1723B7C1D3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a5aa94c8e45c27c05c3a12795740c87d5e2ef2f","datavalue":{"value":{"entity-type":"item","numeric-id":5613960,"id":"Q5613960"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2758043$F4994C9A-2899-4021-828B-8DF5C650C060","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9f21257d8b20ccfecd3db595afbc8b2e1a0a737","datavalue":{"value":{"entity-type":"item","numeric-id":3835817,"id":"Q3835817"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2758043$2EF2239D-442E-41C2-9C49-5315270E9AAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93f7e9b51624f25e880af792c7f9d74c82f45335","datavalue":{"value":{"entity-type":"item","numeric-id":3722471,"id":"Q3722471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2758043$282584A4-868E-4E80-957C-B369DD0B0D5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7dc5db43eaf35bb5b801516b08f876b5e7d02563","datavalue":{"value":{"entity-type":"item","numeric-id":4276172,"id":"Q4276172"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2758043$A2E1BB0C-5D45-42FB-81F7-317964EC98DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5c82ce0af64d5f4743d2bddb20b6a63a2841c9b","datavalue":{"value":{"entity-type":"item","numeric-id":4238504,"id":"Q4238504"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2758043$FD740188-DAB1-48C2-978A-90E0D2225DEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"23e4537b0757ba21c738936714d08bad554bee31","datavalue":{"value":{"entity-type":"item","numeric-id":4879898,"id":"Q4879898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2758043$B6FDBDA5-193B-4A06-B979-03866436D9F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4625a8b175c798b9b816252c4eb7b84249a3d851","datavalue":{"value":{"entity-type":"item","numeric-id":1066884,"id":"Q1066884"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2758043$57176C49-F645-4743-A843-8D65C991F1D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"04c087c749fac9e62b1f0f29ee6e8e1b8e2ba181","datavalue":{"value":{"entity-type":"item","numeric-id":1062045,"id":"Q1062045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2758043$E35C0FEC-80FE-41D1-83D3-0600287EFDCC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f911013841f0efd16cc2960c0d00771522a0a34c","datavalue":{"value":{"text":"An axiomatization of full computation tree logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2758043$02D9A502-AF5F-4CBA-AFCB-B042684D45FF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"cd9ebe56ec423ec5335930a0b1a45ca7ae3b5c0f","datavalue":{"value":{"entity-type":"item","numeric-id":6768298,"id":"Q6768298"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2758043$97A6C9AF-C02F-4099-B0BD-311ABD215FE9","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"f5ce04281af4a8aade1a457e280919888dece8b6","datavalue":{"value":"The paper deals with the logic CTL\\(^*\\), also called the full computation tree logic. It was introduced by Emerson and Sistla (1984) and has been mainly studied as a tool for specification and verification of complex systems in computer science and practice. The main problem regarding those applications is that of model checking (i.e., the question if a state satisfies a given formula). NEWLINENEWLINENEWLINEThe problem studied here is motivated by more classical questions of logic, it concerns validity (or satisfiability) and the relevant (Hilbert-style) axiomatization. Though the validity problem for CTL\\(^*\\) was known decidable, the existence of a simple, sound and complete axiomatization has been a long standing open problem -- and this is solved by the present paper. NEWLINENEWLINENEWLINEThe author uses the known axiomatization system for CTL\\(^*\\) with a more general semantics (i.e., the logic \\(\\forall\\)LTFC [\\textit{C. Stirling}, ``Modal and temporal logics'', in: S. Abramsky et al. (eds.), Handbook of logic in computer science. Vol. 2, 477-563 (1992; Zbl 0777.68001)]), and adds an axiom (scheme) and a rule to achieve a sound and complete system for CTL\\(^*\\) with the standard semantics (on Kripke structures with total accessibility relation). The axiom expressess (the expected) limit closure while the main novelty is the rule -- called the Auxiliary Atoms rule. The main technical part then deals with showing completeness of the system. The author also provides an informal overview of the proof and comparison with techniques used previously for related results.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2758043$363CF76D-66C6-4C8E-BEFF-D757C444E2C2","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"aa98ea30b6abca7b476f74745e2df6c0f45b70be","datavalue":{"value":{"entity-type":"item","numeric-id":672325,"id":"Q672325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2758043$0CBF2E4F-5A1E-4A24-A762-6A11CAD9F3E1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"70c047b2e7a6b97118518cc59f4a171e82b0186d","datavalue":{"value":{"entity-type":"item","numeric-id":1389439,"id":"Q1389439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cfd609c397eff74658971b096e2d1af6beaca78e","datavalue":{"value":{"amount":"+0.865644097328186","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":"Q2758043$3EA25810-1A6A-45E5-AA3B-DA245EBFB2AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c751198a8a50c07031f79a530cea0627b554c11d","datavalue":{"value":{"entity-type":"item","numeric-id":5878903,"id":"Q5878903"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"45e80c5e292872483fcdc6f5921b0617b20f9aba","datavalue":{"value":{"amount":"+0.864470362663269","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":"Q2758043$76ED7223-7963-49AA-96A8-71CC38204152","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d6c1d8ca4353a1bc152e57fb0fc519a94f58366e","datavalue":{"value":{"entity-type":"item","numeric-id":2566222,"id":"Q2566222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9c371f4229f4672517a5096a9b9781c2cf8781af","datavalue":{"value":{"amount":"+0.8412132859230042","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":"Q2758043$22787641-572B-404E-838A-5DC81D64EA7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"67266a4f620a8393150d30127a77d173cd57943c","datavalue":{"value":{"entity-type":"item","numeric-id":3768883,"id":"Q3768883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"20b01330d7f0e24019c665a60fd77f1bf8a5dbcf","datavalue":{"value":{"amount":"+0.8255694508552551","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":"Q2758043$5C9E5366-7382-4235-BC00-78052AA10775","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ea6ce8b156bb5a316bc350d0f03d67b3cbce7fe7","datavalue":{"value":{"entity-type":"item","numeric-id":2908510,"id":"Q2908510"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"93492ec8c6e8808b5798e73c1981569e98f3ce37","datavalue":{"value":{"amount":"+0.7962954044342041","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":"Q2758043$E1D5319D-E936-49B4-B325-26AB525F0E60","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2758043","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2758043"}}}}}