{"entities":{"Q1076669":{"pageid":1087421,"ns":120,"title":"Item:Q1076669","lastrevid":66694278,"modified":"2026-04-12T12:07:19Z","type":"item","id":"Q1076669","labels":{"en":{"language":"en","value":"Tautologies with a unique Craig interpolant, uniform vs. nonuniform complexity"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3954887"}},"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":"Q1076669$78C96E73-3D3C-4BC2-84C5-EC2B453269E6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"aa5a2251b808d75865b493da8c43b7a8e54c972c","datavalue":{"value":{"text":"Tautologies with a unique Craig interpolant, uniform vs. nonuniform complexity","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1076669$E5BFD034-C32F-4B6C-B68D-96C5A9B0DE4D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5ee085567ec6c9f2097287a58a41e8f3065a05a5","datavalue":{"value":"0594.03022","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1076669$C1F98DA0-B319-423F-988C-9D7FD7EEB9A4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"188684b896e1e76250fae68a9f9861261443cd0a","datavalue":{"value":"10.1016/0168-0072(84)90029-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1076669$7B66CC5E-8D6D-4979-93B2-225D9C692277","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8059b8b5e7d67e2c7a1c512c2a2acd219f0f77d3","datavalue":{"value":{"entity-type":"item","numeric-id":186051,"id":"Q186051"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1076669$E5F3BF50-6DD3-4E86-96EE-408D002CBF0A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1076669$ECA795F5-ED91-4CC0-AD58-09C91A8126EC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2ee0f220147ae8bc749a64db56839865dbc4f127","datavalue":{"value":{"time":"+1984-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":"Q1076669$646F6A5F-34A0-4EAF-9B64-12B052AA565A","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"063921e023b90d4fe083fedfe78d0c3edcb20ffe","datavalue":{"value":"In this paper, the author continues his investigation of the relations among the complexities of computations, of circuits, of interpolation formulas, and of formal proofs. Some of the main results are as follows. (i) Consider tautologies \\(H\\to K\\) that have a unique (up to logical equivalence) interpolant J. If \\(P\\neq NP\\cap coNP\\), then no deterministic Turing machine M can produce such J in polynomial time in terms of the length of \\(H\\to K\\). (ii) Consider a finitely axiomatized, complete, first order theory \\(\\Theta\\), and let \\(\\lambda_{\\Theta}\\) be a function of the lengths of formulas that give upper bounds on the lengths of their proofs. Further, let T be a function giving an upper bound on the time to produce J in (i). Then an upper bound for a decision procedure of \\(\\Theta\\) in terms of a deterministic Turing machine is \\(T^ q\\circ \\lambda^ p_{\\Theta}\\) for some p,q\\(\\in \\omega\\). (iii) Let \\(\\delta\\) be a function of lengths of tautologies of the nature in (i) that gives the lengths of interpolants. Then any \\(S\\in NP\\cap coNP\\) can be computed by circuits \\(\\{\\alpha_ n\\}\\) whose \\(depth(\\alpha_ n)'s\\) do not exceed the bounds \\(k\\cdot \\log \\delta (n^ p)\\) where \\(k,p>0\\) depend only on S.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1076669$A8D28173-1B7F-4EB7-B03D-C4D5E02C7ED7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d7656d1c841701431b0b3d99d23720089a267cbb","datavalue":{"value":"03D15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1076669$FF23F35D-47DD-47B2-A888-D44F746A17C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c1d2d83da0d870574277144fdd1db9abaae162ec","datavalue":{"value":"03C40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1076669$833BFF31-95F6-47F4-9D62-FC689382DD46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4dd17e948ef0e266d136e969bf8283741afbd898","datavalue":{"value":"03F25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1076669$66B68101-DC9D-4CB0-A8E3-665890DCA9A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1e903e68a16880f66ed79a0863889f1b2d3c837c","datavalue":{"value":"94C10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1076669$98B93D58-F759-4B7C-AB71-97DB7C29C8B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1076669$E645779D-E582-492C-B743-C48FE68E5737","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"02f22e50cb026b0962246dd13a3793413784bad2","datavalue":{"value":"3954887","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1076669$DB6D420C-3EEF-44EE-B4AC-1690AB5B3F83","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7edadeef8bb2338ff3a07e14bdbe112375679df2","datavalue":{"value":"proof length","type":"string"},"datatype":"string"},"type":"statement","id":"Q1076669$8ACA6611-689A-4BEC-9A54-4A81CCFE65DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"214c3f3e09276ae5f2bcb6823802ced29340e205","datavalue":{"value":"circuit depth","type":"string"},"datatype":"string"},"type":"statement","id":"Q1076669$A005DF75-EFD5-4530-965B-3D3B539DB9C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4dc23b90c1be4baaecf0ba99f92c30aca4062487","datavalue":{"value":"deterministic Turing machine","type":"string"},"datatype":"string"},"type":"statement","id":"Q1076669$6C1E2DDA-0E88-4770-81F8-3EAC479FC7E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eb79299daf8f29391d6c8a2b4222865ffe474551","datavalue":{"value":"decision procedure","type":"string"},"datatype":"string"},"type":"statement","id":"Q1076669$BA4E6403-C470-43F3-86A7-9F7ED4AB6508","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"63aa3593d01449c2e90186926372d4acfefae5d8","datavalue":{"value":"lengths of interpolants","type":"string"},"datatype":"string"},"type":"statement","id":"Q1076669$34B2F97B-DE7D-47BC-82FD-BAF2DAEAC911","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":"Q1076669$3A8407C1-EE32-45A6-8ABA-A3E3D2F3779C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c097ddeb302cb669c9f9cf68647264f7b2756320","datavalue":{"value":"https://doi.org/10.1016/0168-0072(84)90029-0","type":"string"},"datatype":"url"},"type":"statement","id":"Q1076669$BEBF5949-A591-42D4-A535-3F134B2EBB3D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ba2ecb67167e38a0689e5992ab0b26b64aeee703","datavalue":{"value":"W2026916148","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1076669$759D899A-4357-4A77-A040-81C051EBA69C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0c859dc9bc5c44c673f4132f2e7bef4d53162ec9","datavalue":{"value":{"entity-type":"item","numeric-id":1188602,"id":"Q1188602"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1076669$0BAAC99F-55A8-4FD8-B137-6FF5A2802CC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"472fa3c2a3aac4e284c61a994efad95a655ca659","datavalue":{"value":{"entity-type":"item","numeric-id":4068717,"id":"Q4068717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1076669$DCAB0874-78C7-458C-94F0-F42DC400B0C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df9b440a7e27b4753042460b886584e943bebd26","datavalue":{"value":{"entity-type":"item","numeric-id":3957950,"id":"Q3957950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1076669$2487A7AF-C2DC-4AFC-96AC-17FAFFB555B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"21c346fcf8c23cf4fedee6adca5eb2e9b1b265a3","datavalue":{"value":{"entity-type":"item","numeric-id":3887444,"id":"Q3887444"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1076669$AFDA6870-16E8-4B10-BBA5-C6A8789D85D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3589abe08309ee0c80b87d4a4fa6a10bf824c734","datavalue":{"value":{"entity-type":"item","numeric-id":1235011,"id":"Q1235011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1076669$18732FBA-A5D9-492E-8049-A6180401DB63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4756f7b3e413b96dc6a797669c55c442b5b6f6f1","datavalue":{"value":{"entity-type":"item","numeric-id":4749821,"id":"Q4749821"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1076669$4AAB1E76-D08A-479D-AE50-191AB031ADD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2dd10b809cdfd26674cd25cafbf01bbf0dce8e4f","datavalue":{"value":{"entity-type":"item","numeric-id":3724312,"id":"Q3724312"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1076669$B963EC0A-1614-4E7F-BBA7-E0349C498BEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b3ef38ef005c69e7bd0fea842b7da511c1842a8","datavalue":{"value":{"entity-type":"item","numeric-id":4077450,"id":"Q4077450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1076669$8B7B3812-CA2C-447F-B0B4-B1E9E01E70BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9920c3ac00d626f59f95283223bd4fb6ae680345","datavalue":{"value":{"entity-type":"item","numeric-id":1152951,"id":"Q1152951"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1076669$8BEA6932-AAC5-43A7-BB6F-8B0EEA0161BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c43b242e8d2a6febe28b4e1a41898561ecb7a1a8","datavalue":{"value":{"entity-type":"item","numeric-id":4138141,"id":"Q4138141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1076669$C158206C-7A4E-4094-A4DF-AF0A210331B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22a3fc682c768d150fc7590f349de88990574d26","datavalue":{"value":{"entity-type":"item","numeric-id":3967050,"id":"Q3967050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1076669$AEDF9A7D-4B6C-4B36-885A-06371937117D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a480ff6f8af5ea30ef6a1afcb4c00518709484e6","datavalue":{"value":{"entity-type":"item","numeric-id":3936198,"id":"Q3936198"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1076669$88B98B4F-88F7-4BAD-81DB-EF8878538BBC","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"e75445a69c6d3e8593c76da682d6cbf841c54f13","datavalue":{"value":"Q127957473","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1076669$62716679-E7F4-48E4-9C15-6EDCC18CA653","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9cc6dc927d7171552954decb2348910c6af0a2d3","datavalue":{"value":{"entity-type":"item","numeric-id":3724312,"id":"Q3724312"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"819d273bf38477d72e0c778c43e626db0aa16313","datavalue":{"value":{"amount":"+0.8821683526039124","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":"Q1076669$53FB7CB6-09C5-48E7-9D6A-F490B75DA2BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2da167317dd79e81ce517fedf9670335ecd7e89a","datavalue":{"value":{"entity-type":"item","numeric-id":3684112,"id":"Q3684112"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2dc74a6282c5941526b975b6fd7f25e05d84ac70","datavalue":{"value":{"amount":"+0.8757519721984863","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":"Q1076669$5C8FF3CA-CC7B-4AC2-8243-03E53598DE10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"49ae2a0b77923a129f57ce18f68b6556632938c3","datavalue":{"value":{"entity-type":"item","numeric-id":1118581,"id":"Q1118581"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9af61dbd0c377b8ceee18823451ab9e6217eb4dd","datavalue":{"value":{"amount":"+0.8014459013938904","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":"Q1076669$A1E61E00-C0C1-4F78-B350-E69EF9525862","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"02e55b61410f38e6a1b24aaa79cfee91f308ed35","datavalue":{"value":{"entity-type":"item","numeric-id":4934563,"id":"Q4934563"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e58b7a5d86784d61acc6cc3de449f0766cca312a","datavalue":{"value":{"amount":"+0.7778308987617493","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":"Q1076669$EBA06FA2-4AD3-42FA-9E55-9FD49451F63E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6ee13f3a2d31cceffa18aee668ba7a8337f1c448","datavalue":{"value":{"entity-type":"item","numeric-id":4340536,"id":"Q4340536"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e58b7a5d86784d61acc6cc3de449f0766cca312a","datavalue":{"value":{"amount":"+0.7778308987617493","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":"Q1076669$F66F493C-C692-4F3A-B6B2-45BF564FCBF1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Tautologies with a unique Craig interpolant, uniform vs. nonuniform complexity","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Tautologies_with_a_unique_Craig_interpolant,_uniform_vs._nonuniform_complexity"}}}}}