{"entities":{"Q908896":{"pageid":910744,"ns":120,"title":"Item:Q908896","lastrevid":65326176,"modified":"2026-04-12T01:49:41Z","type":"item","id":"Q908896","labels":{"en":{"language":"en","value":"On connections and higher-order logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4135911"}},"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":"Q908896$7FA2258D-B626-46C4-9B8E-7DB5201BC424","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"78e88f64010e6884158f1dd4b43eb69c14adfea1","datavalue":{"value":{"text":"On connections and higher-order logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q908896$9C322637-9BD6-426F-9D7E-54F6F75E2F33","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2421cf2942551e354325827d02a85066308388c2","datavalue":{"value":"0694.03011","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q908896$011987FD-A548-4FF8-950D-63840F028F62","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"669a0c943571e23498b44f8184ed275323dd1014","datavalue":{"value":"10.1007/BF00248320","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q908896$A939D4C7-BAD7-43AD-906B-8BF4C6F8C8F2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"025155ad88f33216a4124a2c377d3f6c78a58a7c","datavalue":{"value":{"entity-type":"item","numeric-id":804556,"id":"Q804556"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$14B21A90-7FD9-4A31-9838-7793938D45AC","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$B197C958-6418-44D2-9CBB-26DD62D7A7DE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7211ad5ca16eb0d22cd0051fff3d0f3af254ceb6","datavalue":{"value":{"time":"+1989-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":"Q908896$85196EC1-A015-4A0F-8D70-0E1B54880238","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b16a751c8e1e0d09c0a32ad8cb13ad1355577e62","datavalue":{"value":"The paper gives a detailed introduction to proving theorems in Church's typed lambda-calculus. The presented method was developed by D. A. Miller and uses expansion trees: an expansion tree is built from the tree-form negation normal form of the formula by adding subtrees with substitution instances to the nodes. Proofs consist of finding a contradictory tree by establishing right connections between parts of the expansion tree. Detailed examples are given.","type":"string"},"datatype":"string"},"type":"statement","id":"Q908896$2B68DF4B-2101-4DA4-965B-0ACDB0A92CB1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q908896$68079D39-151F-4B24-8B3E-8169B7C57D2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q908896$B3A9D45B-6B99-4ECF-8AE4-499D31E2350D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q908896$7CF9D362-0ABA-4FBF-AF77-C67B426040E2","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"fb7d5eb56624d9f1b115cf4c2b4357d84fc7f4ab","datavalue":{"value":"4135911","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q908896$D8F4B537-0D91-45A6-A015-621DE9885B00","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9766ea21e04bbb663ab057ef2e9635b0fd3090d5","datavalue":{"value":"connection method","type":"string"},"datatype":"string"},"type":"statement","id":"Q908896$A231FBEB-DF36-45A8-93F0-085D3FE0A9B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e61f6e458efbc8d9423292372f8fe500146462dc","datavalue":{"value":"proving theorems in Church's typed lambda-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q908896$1095C38D-D6AE-48AE-8D8C-EA192547E3DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"162c8c826152c47bc21e01bdd0a121076fde9007","datavalue":{"value":"expansion trees","type":"string"},"datatype":"string"},"type":"statement","id":"Q908896$1206EBF2-84A8-49FE-B1E1-A997438E4E10","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1aec27d540e360c78ddad230e6e300ced62bdec3","datavalue":{"value":{"entity-type":"item","numeric-id":18433,"id":"Q18433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$960E231B-32E3-4D05-8AE8-5EBE4B88AB2B","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":"Q908896$210CDFCC-1417-4DF0-BA82-6A3C59F3EE21","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0021eb1ef45a5b93ce1d9b7eb620338bc69ad123","datavalue":{"value":{"entity-type":"item","numeric-id":5638281,"id":"Q5638281"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$60CD55B9-5EC3-4DD2-A876-AD5DF295DA68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"818f2044ada61f8186028673bf007a526a9aea73","datavalue":{"value":{"entity-type":"item","numeric-id":4096457,"id":"Q4096457"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$AFAE3ED0-AAF8-446D-8684-B1616F692702","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a74c52dce2b41371b695c2dd9e16f460a2c3a87e","datavalue":{"value":{"entity-type":"item","numeric-id":3880316,"id":"Q3880316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$0B55C3CB-817F-4066-9B3E-EFA5AD7B95F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ed4e2b73edd0e2661ebb75822eda29ecb9eb63a","datavalue":{"value":{"entity-type":"item","numeric-id":3906484,"id":"Q3906484"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$A043F716-168E-43D4-B4E7-0AA522F44967","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c9f2843640e7eabb53dcf6b38d2e418915c6350","datavalue":{"value":{"entity-type":"item","numeric-id":3343471,"id":"Q3343471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$2623AA25-179E-4383-B05D-3422A6F1AB3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"85b58e334bbf84629d414ca7d6688164e5524fe2","datavalue":{"value":{"entity-type":"item","numeric-id":4726218,"id":"Q4726218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$3C08E6AA-2877-41FE-99F1-8D6E77B33DC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2a0224c2184a70caa4b65bc17bb3bf09017286a7","datavalue":{"value":{"entity-type":"item","numeric-id":1132862,"id":"Q1132862"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$DA97C107-BBBA-4968-A018-B26D817E6114","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"82285947ecd1d65d80e17696025cdf5ddb799be6","datavalue":{"value":{"entity-type":"item","numeric-id":3922205,"id":"Q3922205"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$8AAA3A68-D23A-4DE0-BE76-7480A8F6A7DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d703f425e2cd9d5990923afa9390325a818d3a22","datavalue":{"value":{"entity-type":"item","numeric-id":1836483,"id":"Q1836483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$848D020A-FC36-4659-900B-1A77AD32E46F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"850ca39a94aac87362042c94528de0b33c665341","datavalue":{"value":{"entity-type":"item","numeric-id":3668887,"id":"Q3668887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$EA0540BF-2C7F-47D4-AE81-126FC17E72F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ca7e027091589776f78a6d7ad8457e805c17b28","datavalue":{"value":{"entity-type":"item","numeric-id":5777498,"id":"Q5777498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$98AF7134-C08B-4540-A9FC-D1EA69AC7A69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d9d6412374cd99d26f25760aacca4ecd0fb813a7","datavalue":{"value":{"entity-type":"item","numeric-id":5339307,"id":"Q5339307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$6E658A8C-1FB9-4A94-BCAB-6AF0E2D9BDEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b258ca187c81b9bb7848210f28bc59e01d56d47e","datavalue":{"value":{"entity-type":"item","numeric-id":5331469,"id":"Q5331469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$516A42BC-EFC9-4C8B-8065-2F982E11175C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f6c3f3ba22c16111e5ca10533d8e5ad50f4bb3a2","datavalue":{"value":{"entity-type":"item","numeric-id":5625123,"id":"Q5625123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$511E1471-40CD-4A5D-BF25-49FA011FF86E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4fecc7ce8fe53bf0ab0f560a96ff760721b70f9b","datavalue":{"value":{"entity-type":"item","numeric-id":1230505,"id":"Q1230505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$FA53EC10-6F0C-45BC-A4DF-6A5C8449B09A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"18ce06304bf3709cc235c3276b4f500aec1ac468","datavalue":{"value":{"entity-type":"item","numeric-id":1239309,"id":"Q1239309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$C405713F-F9F9-4DDD-8F1A-5D4DAB3AEA26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"55a782dae04bccdcae6268f44742e68ac18ada1a","datavalue":{"value":{"entity-type":"item","numeric-id":3338232,"id":"Q3338232"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$F9B3D63A-B130-4269-B66B-8698BA32E764","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1675ec5894a8c57acbe2bcc56434f5813617d031","datavalue":{"value":{"entity-type":"item","numeric-id":1102282,"id":"Q1102282"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$2F6C9727-778B-468C-9554-6CDE3B57BDBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58cb14dabb49ce81b914063d4d765de30bcb45f7","datavalue":{"value":{"entity-type":"item","numeric-id":3338233,"id":"Q3338233"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$C1D78404-0660-4B37-A604-A381C597F511","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cceee8a5fb32e6eb7443356542ae558c36b13a21","datavalue":{"value":{"entity-type":"item","numeric-id":5672214,"id":"Q5672214"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$C5451A58-0E41-45BC-952A-48F29722FFEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c5bd4f24e8eb1a084ca4ac4963d45f487b7e5bb4","datavalue":{"value":{"entity-type":"item","numeric-id":1226867,"id":"Q1226867"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908896$05249A88-9616-4EA4-9673-2C8693B92748","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"54ec3f98bb8e5e1de471f72f74cbbaf4a55644e0","datavalue":{"value":"https://doi.org/10.1007/bf00248320","type":"string"},"datatype":"url"},"type":"statement","id":"Q908896$B4AFDB60-C449-4729-B0AE-56F6034F5EF5","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6d2ca28d8df3d73e88074e5595c044301d71f1eb","datavalue":{"value":"W2040723389","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q908896$EBCA9B38-F88F-43C9-A4B9-AEDC45E113D9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"050391e3f27b8bfab5af09f69bc4e968903fe067","datavalue":{"value":{"entity-type":"item","numeric-id":4871733,"id":"Q4871733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7b2ffe5c20e49eb5dc84fab95c4c4c23e05e3cbe","datavalue":{"value":{"amount":"+0.7656359672546387","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":"Q908896$F711507B-E7A1-4717-B139-280D527973D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad894f0e4fcd4cc03c848bf583b58ab56e3b8f5c","datavalue":{"value":{"entity-type":"item","numeric-id":2753786,"id":"Q2753786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"13497f5c67fe629fd9294dac88bcd45d9d9e2a94","datavalue":{"value":{"amount":"+0.7564458250999451","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":"Q908896$9BDDD9ED-C53F-4DCC-983E-DBD8DABBD31C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4a77f92b0a8bdda0dc21719f1ec259c8b9ed6960","datavalue":{"value":{"entity-type":"item","numeric-id":2754030,"id":"Q2754030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"59a409e4dd099b349d93342f59f7e32f091bf549","datavalue":{"value":{"amount":"+0.7541065812110901","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":"Q908896$0A08B8E1-6F22-402D-BF3A-A38F3978BCEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"68f5e6c2ffa5a2ba95848085e6708f2b0de4f8c7","datavalue":{"value":{"entity-type":"item","numeric-id":3997125,"id":"Q3997125"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6c763df41560e1de51161180899b266ee8d0b89f","datavalue":{"value":{"amount":"+0.7490314245223999","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":"Q908896$B3A12AC9-5CE7-4F44-BA0E-6CF28094EF2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d0af841dbaac1c030960b977a72d80d9d1f04996","datavalue":{"value":{"entity-type":"item","numeric-id":2708310,"id":"Q2708310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"95011195743176f8b5f53c284c902d86a2b54473","datavalue":{"value":{"amount":"+0.7479065656661987","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":"Q908896$4D7DE90F-6FF4-4B95-943D-6C2D7D5DD4AA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On connections and higher-order logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/On_connections_and_higher-order_logic"}}}}}