{"entities":{"Q1102941":{"pageid":1113693,"ns":120,"title":"Item:Q1102941","lastrevid":49168795,"modified":"2026-01-06T17:04:29Z","type":"item","id":"Q1102941","labels":{"en":{"language":"en","value":"A complete axiomatic characterization of first-order temporal logic of linear time"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4051575"}},"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":"Q1102941$DB5312E4-5763-4D36-9593-078707C3CACD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c5412104654c06f29b6e2a95f2e461646c1d7088","datavalue":{"value":{"text":"A complete axiomatic characterization of first-order temporal logic of linear time","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1102941$09F495CB-506C-4E06-A699-B7F808AE465B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8e770736ad2d45ac72a2c86b26eb0968d9e659c1","datavalue":{"value":"0645.03020","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102941$F7BC79A1-468E-4282-96F1-5F5197BB6D39","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"96c18b77b2cf57c737b9aed71ac9048dca65fc37","datavalue":{"value":"10.1016/0304-3975(87)90129-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102941$FC291747-2D08-4556-A7AC-CF045645903F","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":"Q1102941$8393DB77-F553-43EE-9864-1F5010726865","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5ae48c61eed19d1e1e1f33f9255d5b329362d064","datavalue":{"value":{"time":"+1987-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":"Q1102941$A08806CF-60DE-43A7-BA21-D708CCC4D5C4","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"eb3e1004ce5ef7ad9a8017a1f5e86ea9dde8f40c","datavalue":{"value":"This paper deals with the theory of first order temporal logic of linear and discrete time (FOTLL), with the ``atnext'' operator A instead of the ``until'' operator U. An infinitary, sound and complete proof system for FOTLL is given (it is known that no such finitary system could exist). The proof method is based on Q-filters (adopted from algorithmic logic). It is also proved that any syntactically consistent temporal theory has a model. An example of the use of an infinitary proof rule in proving correctness of a concurrent version of Quicksort is provided.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102941$9C7267D8-7733-4DE0-9AE7-E7074DD254CA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102941$6DAAE863-D8E4-42E5-A509-0D2063A98EF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102941$7A0A58C9-46BA-43CB-AB5C-CAA48C2FE6FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102941$BF7F621F-69DF-4A6D-A7B3-D0DB3B5B44A5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1f7ed871eea939174f862530fd718f7b21adeb64","datavalue":{"value":"4051575","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102941$994CDA4D-BC08-4829-A7FF-19FA7461233C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a850ee01f9fe6c0e93ae692ac21d7eb4a5f1f68c","datavalue":{"value":"concurrent programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102941$5EF8ED23-237E-443F-985C-21234F32E604","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f88c4dc2ac7c528d0986cf2b7d950485b332904d","datavalue":{"value":"first order temporal logic of linear and discrete time","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102941$679FC32F-A2E6-42C6-8DCF-D378696AA2B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"667ec4f4f5a99b4982a514f4c332fc78b9746a85","datavalue":{"value":"correctness of a concurrent version of Quicksort","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102941$05C6D54C-DADF-4151-A557-0AD6604DF2EF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ca60e4abfd0c45cace511a7d7434a08b65f8249c","datavalue":{"value":{"entity-type":"item","numeric-id":763332,"id":"Q763332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102941$69CDAFEC-61E1-4B25-8F6F-C41C72BB5BAF","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"6536f759dee9ce142c834adc5cc137400d919eb8","datavalue":{"value":{"entity-type":"item","numeric-id":1037240,"id":"Q1037240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102941$0A463AFE-DA49-4BB4-BFA7-8B2A3EBB2845","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":"Q1102941$54137F19-4F91-4387-8C9C-6E48223C3F00","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e128724d9789ee84a3ece93e39063fe9bc6cb08a","datavalue":{"value":"https://doi.org/10.1016/0304-3975(87)90129-0","type":"string"},"datatype":"url"},"type":"statement","id":"Q1102941$8147F01A-8DF7-400C-99D8-703858C7D5B0","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"099019e2a7a9f806cc38e7627454110e1333c5ea","datavalue":{"value":"W2074329619","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102941$F638DE9A-1DB9-42DE-A61D-6A3CCB63AFB7","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0900917f6ce2d40a95f5358f603c9df639a16762","datavalue":{"value":{"entity-type":"item","numeric-id":3952084,"id":"Q3952084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102941$5258186F-DF50-41F5-87BC-295EFBD54EF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9deaf5805369ed94d2c2b3ba23b0118b7817813","datavalue":{"value":{"entity-type":"item","numeric-id":4151145,"id":"Q4151145"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102941$E1D9EB83-582F-4C1F-BFC2-68960E45EC79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"74833c204341d9aa9ef14997fbac19d0e7da176d","datavalue":{"value":{"entity-type":"item","numeric-id":3749040,"id":"Q3749040"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102941$5E998F1C-639E-4485-B6C9-BD56D0D42E76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"45c73db8b3c2a0a30e7c3eaaca382d1ea005a940","datavalue":{"value":{"entity-type":"item","numeric-id":3677141,"id":"Q3677141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102941$3B3CAE43-49BC-4093-BFEE-2B1E203D951D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"161c81188dcd2fd1b18f956df590ef058f86413a","datavalue":{"value":{"entity-type":"item","numeric-id":800722,"id":"Q800722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102941$BF553453-082F-40BD-B47C-59826B3273B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5b4c95f53b57f2eb31607a9241c4b370cdcd831","datavalue":{"value":{"entity-type":"item","numeric-id":3939208,"id":"Q3939208"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102941$2EC975FE-D67B-44DC-86E8-64C026B676FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ddb4455e7cfda46f508237aa8760acaf2133498","datavalue":{"value":{"entity-type":"item","numeric-id":3881900,"id":"Q3881900"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102941$D01338D7-0D4B-4BDF-88A2-8173C0EA58F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6d4655612b304d9bd7e703b05e0795028a785b49","datavalue":{"value":{"entity-type":"item","numeric-id":3792662,"id":"Q3792662"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102941$327F7103-1113-4295-8E58-3A8BC31DE029","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98782dca1b1c9d3479c56bc90f4cd51924e8bc96","datavalue":{"value":{"entity-type":"item","numeric-id":5734410,"id":"Q5734410"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102941$6B0E14A3-02EC-47F8-AFD9-A44F968B30C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a2f8da7733f5df652657471b8fc372ee15cfbac5","datavalue":{"value":{"entity-type":"item","numeric-id":5585437,"id":"Q5585437"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102941$B54F9F15-2C1D-4055-BBCD-8F2D454043BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d146d246413177b312092e2e92a23dd8dd3ab624","datavalue":{"value":{"entity-type":"item","numeric-id":3957924,"id":"Q3957924"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102941$15CADAD6-3E9C-46B2-B452-BE4333121CE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1aaa7c2a801938246bc5b9c35ae533855c08aea3","datavalue":{"value":{"entity-type":"item","numeric-id":1090673,"id":"Q1090673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102941$781CF785-0A0C-43F7-8BFA-F8B9D8AE7A11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e12754be2dde76deb61f2dea60d3e4b7cd16fc70","datavalue":{"value":{"entity-type":"item","numeric-id":1101100,"id":"Q1101100"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102941$F86A576A-9533-454A-9F0E-F7C7B4ECA216","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d9456d9b3e59e143f5e55b694b92114428f6e73","datavalue":{"value":{"entity-type":"item","numeric-id":1123184,"id":"Q1123184"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102941$8FE09664-7133-4440-BE3E-CB8A5FB74D69","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"8a396ba9f3fee9878aa26e7cfa36e54f2e59a63f","datavalue":{"value":"Q127491328","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102941$223BED0B-3DC3-40F3-AEE6-E0701DFF16A8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"891ec74453572b7814cf8b5c6c0909e95aa17119","datavalue":{"value":{"entity-type":"item","numeric-id":4353629,"id":"Q4353629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2e429b713a2c53b50a176e02d4083872cd1060e7","datavalue":{"value":{"amount":"+0.842384397983551","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":"Q1102941$176EFDA2-84D9-4E17-842B-05D05DEA2D71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"081bd63286da1909b7245ea381f5077097f31ff7","datavalue":{"value":{"entity-type":"item","numeric-id":2913981,"id":"Q2913981"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5df13bdc871106dc0fa305cf794aa62c9cd57b85","datavalue":{"value":{"amount":"+0.8398885726928711","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":"Q1102941$40776E89-8725-4F40-9650-AC660F92E5B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"85ba7597552f4d235072d5a833cc94413be77496","datavalue":{"value":{"entity-type":"item","numeric-id":1101100,"id":"Q1101100"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3bb704f5820681ea1def576a80b7e995f7f7c28d","datavalue":{"value":{"amount":"+0.8367118239402771","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":"Q1102941$69B4E2FD-853C-4B44-BE1A-A989E1392661","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"341fc183e534ecaf9bb2c42b864481a6c925c178","datavalue":{"value":{"entity-type":"item","numeric-id":1118578,"id":"Q1118578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5462c4ad2f5347d3f5e1968d91627c4389fea01b","datavalue":{"value":{"amount":"+0.8218217492103577","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":"Q1102941$DA453103-04D5-48BB-B665-B057D1F0BC0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b2a268163365589a0d288d821dc138c43e323937","datavalue":{"value":{"entity-type":"item","numeric-id":2563451,"id":"Q2563451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"10a168106a3071eabed6a84ff95d7cadae10d8d6","datavalue":{"value":{"amount":"+0.8163878917694092","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":"Q1102941$6541C1DB-91F2-4CF9-A4C3-4C33D111BF0D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1102941","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1102941"}}}}}