{"entities":{"Q1694474":{"pageid":1705215,"ns":120,"title":"Item:Q1694474","lastrevid":68244717,"modified":"2026-04-12T22:24:27Z","type":"item","id":"Q1694474","labels":{"en":{"language":"en","value":"Realizability in cyclic proof: extracting ordering information for infinite descent"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6833563"}},"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":"Q1694474$29C446DB-2A85-4D03-9BCD-7DB5DB0C7CD2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"98e38f5fc14f774248bf03650ca387110543a8e8","datavalue":{"value":{"text":"Realizability in cyclic proof: extracting ordering information for infinite descent","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1694474$E0DF952C-080B-4E8C-BC25-F48ACD80250C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7a028361bbb24cc54ac67fd7c5487dcd94f78cd5","datavalue":{"value":"1496.03233","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1694474$2989DE04-657C-4CBF-8ACA-D0997AD1BEF7","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a0212805e1d8cd10e982bd50170656d1a255be29","datavalue":{"value":"10.1007/978-3-319-66902-1_18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1694474$46A6B742-CA02-4F49-BE4B-D3B70CAC0333","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"604e2732b1b9634c7f23f07fef29c6e42547c2b5","datavalue":{"value":{"entity-type":"item","numeric-id":387989,"id":"Q387989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1694474$4EC5E7C4-A6FD-4A43-9C63-E74EDF14714A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b218d394a4f78b8be43b552938ed5e21a7cf904e","datavalue":{"value":{"entity-type":"item","numeric-id":1401935,"id":"Q1401935"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1694474$51FF3712-157B-478E-AD63-A4D403C2199F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3340cc79e75714646430612898cfc312969e0dd0","datavalue":{"value":{"time":"+2018-02-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1694474$D6A2B984-CE30-4B18-89A1-CA13FB7C26E6","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4c2f1c8d2d6e1b459d90f287f447a19511c787f1","datavalue":{"value":"https://kar.kent.ac.uk/62287/1/Realizability%20in%20Cyclic%20Proof.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q1694474$6C9220CD-14FA-476B-9910-C6C086D2ACC6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e2ae8b1900147d15ddea62ccb5302a15ee19b5d","datavalue":{"value":"03F07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1694474$7BADD776-3E76-4490-A5B1-25EA5672A1D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1694474$2E2D4743-10D4-48AB-89FA-720221A49C48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9b78776a56fc28cdd893baa47605a105412b838a","datavalue":{"value":"68Q45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1694474$982059D4-1CA0-4D1F-B2EF-3FFA85DABD5A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a3f1c371fb5435e5ebe34dd99e43fbffbc3c5e63","datavalue":{"value":"6833563","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1694474$35A76B91-A4B6-4CF3-8444-82BB817BA37C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a3a454778aa5c7075b65e7fb63846eb3d351cb04","datavalue":{"value":"approximation semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1694474$AB545D2D-4309-4FC8-9436-DCCA83B77391","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a81c26c178c84ff50de2a092c1964baa741ed82f","datavalue":{"value":"cyclic proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q1694474$77D220CC-1892-4149-84B0-FF5888C980E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ef005c57ec72bf1e5b47bd8f6a8adaa20239b969","datavalue":{"value":"entailment","type":"string"},"datatype":"string"},"type":"statement","id":"Q1694474$1AD9C90A-8F4D-422E-BBF7-D848B44301F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ec380ca252be3c5f710d69356f4a05c9923ebeab","datavalue":{"value":"inductive predicates","type":"string"},"datatype":"string"},"type":"statement","id":"Q1694474$553537D1-A1FA-4C06-9CF0-CF292BC320D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"60220bf05c0cc1e8e20b549069d458f7a90331c9","datavalue":{"value":"infinite descent","type":"string"},"datatype":"string"},"type":"statement","id":"Q1694474$F423FCA6-9955-42CD-B98E-BACE4E0B582D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"53d61092cbbff856a3b199e03225e42bcac6db78","datavalue":{"value":"realizability","type":"string"},"datatype":"string"},"type":"statement","id":"Q1694474$1FC2F3B8-6984-4149-AB4A-2886FCD43FD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2c7d4aa0d3cf1745112ae7d594a2a5578f4e767f","datavalue":{"value":"sequent calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1694474$39E0C7B1-01CF-4213-8BB8-F146E5CBF1AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"266cd2fb37ad2ba00390f1ff46b4c5e9361f6aa9","datavalue":{"value":"weighted automata","type":"string"},"datatype":"string"},"type":"statement","id":"Q1694474$B7C2B8EB-D2B9-4EDE-BE25-C3B48F9FE94A","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":"Q1694474$A1B80C76-AAC5-47C4-85D7-E2FD7EDFD748","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"83a59cf6682de864b66bdaf085e28429ef49b2d4","datavalue":{"value":"W2751381847","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1694474$B01FE77D-0998-4DF9-8549-03F5300B5235","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bedf41f4ad814a262dc70d8faa9745816259d7c9","datavalue":{"value":{"entity-type":"item","numeric-id":3189830,"id":"Q3189830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6bb67583ec7042fbcba70d7171570ec8fb8f112b","datavalue":{"value":{"amount":"+0.7299597859382629","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":"Q1694474$278D6E4C-AAB3-4DD3-9BFF-BC44A70ECCF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"35d80961d71c1ad11c1e28f93e1d2b7ee37629be","datavalue":{"value":{"entity-type":"item","numeric-id":1694475,"id":"Q1694475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9670c6e260df025ebd935c01cea5584dac873bd6","datavalue":{"value":{"amount":"+0.7072170376777649","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":"Q1694474$1171EA48-13EE-4CC3-B5C4-3C6EBB15E165","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a67569a8d36820a4f5d562613552274ade326408","datavalue":{"value":{"entity-type":"item","numeric-id":5479270,"id":"Q5479270"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8a7bcf2175d924e3a505f3cdf97f31d5d0a134c0","datavalue":{"value":{"amount":"+0.7043946981430054","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":"Q1694474$480F84BB-1A90-49AB-AA3C-8A37F4C39090","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8ce9665b91ecb3a2eb7e60be16e012a2320e66e4","datavalue":{"value":{"entity-type":"item","numeric-id":5200020,"id":"Q5200020"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"53d406ddfa318e6ffe254a4a4f83dc0b9280a3a6","datavalue":{"value":{"amount":"+0.6985293030738831","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":"Q1694474$2B9EE7F1-7F0D-45E3-BF8E-7C0736EB1F57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"41ec267e9cad032a4874ca7bb352e31dafbe1fb3","datavalue":{"value":{"entity-type":"item","numeric-id":3636808,"id":"Q3636808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5cfa7f6dc6275558c338f72d0c16398b0ad959b5","datavalue":{"value":{"amount":"+0.6907327175140381","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":"Q1694474$0FE2BF3F-E139-4C0F-ABF4-73B267E5CA93","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Realizability in cyclic proof: extracting ordering information for infinite descent","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Realizability_in_cyclic_proof:_extracting_ordering_information_for_infinite_descent"}}}}}