{"entities":{"Q1102282":{"pageid":1113034,"ns":120,"title":"Item:Q1102282","lastrevid":66684024,"modified":"2026-04-12T11:55:31Z","type":"item","id":"Q1102282","labels":{"en":{"language":"en","value":"A compact representation of proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4049640"}},"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":"Q1102282$36BC050C-774B-4C35-B564-D099D36F7DBE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c57e5405b66525a855369e60ba54a8390d9eed3a","datavalue":{"value":{"text":"A compact representation of proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1102282$8F0E8A97-DD85-4AC3-9BD7-3366A5DD4EEF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"91540e700345ab8e96dfb2cf0dc69a710fab00ac","datavalue":{"value":"0644.03033","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102282$74D3DCFB-2B9B-4A93-87D7-15F78F6F1463","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"42e7dcf1c1bcdc33af945ec288497df876f49278","datavalue":{"value":"10.1007/BF00370646","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102282$35C32F1E-301D-4135-A0E7-06F57712033A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2479aee847d640d3090b268957bfaa9b03ce27ad","datavalue":{"value":{"entity-type":"item","numeric-id":1102281,"id":"Q1102281"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102282$52D36E24-A5F1-49F1-8810-AF1C201DFA3D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e34236ca73b92c6ee0bc17431d03c3537a7f0792","datavalue":{"value":{"entity-type":"item","numeric-id":195358,"id":"Q195358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102282$A69933D6-7B3F-4DEF-86B3-D613BC61F853","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":"Q1102282$9DC7BFDD-6C0D-4F70-B8E5-67B9EE56B25E","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"109dd0d9c2ff8d8273a850cddfe642b2cd69ef07","datavalue":{"value":"To save information that could be extracted from automatically generated proofs, structures called expansion trees are introduced. These trees provide a computationally useful representation of proofs in classical first-order logic and some of its extensions. Moreover, they can be easily manipulated and transformed. Explicit transformations are presented between expansion tree proofs and cut-free proofs in the sequential calculus. Similar transformations are possible also into Craig style linear proofs giving interpolants whenever they exist.    A fragment of simple type theory is used as underlying logic. A stronger form of first-order interpolation theorem is proved and a correct description of Skolem functions and the Herbrand universe is provided.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102282$76365753-39DE-436A-B2A6-3A7508F26FE8","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"5b39a071f220ede335b535a94dac9b2e05d71f72","datavalue":{"value":{"entity-type":"item","numeric-id":802552,"id":"Q802552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102282$4D5A27AC-0B8D-44E1-8093-48F98AA6EDCB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102282$2486059B-20A4-41F0-B52E-67164A7E1A94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102282$30928459-80D4-41A6-9DA2-CD9F9597115A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102282$29D84B5A-A97C-410E-BB84-C3EEB4CF75AC","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c25a103a7eaf8f2d448874e0194c1207d2e42045","datavalue":{"value":"4049640","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102282$4765415C-0B6F-45CF-8439-2EB8AD7E1D71","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"595a1e75b49a7c35cfd3caaaff3a4e298be5d31b","datavalue":{"value":"proof trees","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102282$BC814061-07F7-48F8-8DFF-0FC6A002FDAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2c7d4aa0d3cf1745112ae7d594a2a5578f4e767f","datavalue":{"value":"sequent calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102282$CCFE763E-95CA-41D8-9D4F-5D48F5EBE482","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7f26240f6f2e8ed18aba86803f35c16a9c4ed5a9","datavalue":{"value":"automatically generated proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102282$555CFA6E-E3D4-493A-8E7B-756250A3EDE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"162c8c826152c47bc21e01bdd0a121076fde9007","datavalue":{"value":"expansion trees","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102282$30EF3248-5ACA-463E-95AF-9F7929291112","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bc112c1826a1bff539c84aa7a71319d429cf3621","datavalue":{"value":"linear proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102282$725DE7D1-DB3A-48F9-8162-9DA7DB3A4E32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6187bef4252730b1da528b17e27a9e595e64d324","datavalue":{"value":"fragment of simple type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102282$2EFBBA00-5A40-4059-997F-7502D4C869F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bb58dcafe70e8b2532705652f6982b69d68d3016","datavalue":{"value":"first-order interpolation theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102282$ADD4E0F3-9023-4659-B19F-2A32481E7549","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"da9e1556c2fcea0d362972fe609ab0761a0d2f2d","datavalue":{"value":"Skolem functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102282$8711BB12-3A03-4A39-8722-B5B8220BB39D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b28556cc87db6d65020982562b393f6fbdb98277","datavalue":{"value":"Herbrand universe","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102282$A16F8DB6-CE84-4080-A232-1F62EF42F884","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":"Q1102282$646004CD-2524-44B7-A12D-510408570C49","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":"Q1102282$6312E56B-4731-482D-B4D6-152EBFA6CB28","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":"Q1102282$4AD712A7-EF14-4EA5-A110-5F1E009AE40E","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":"Q1102282$964AB90D-CFE7-433B-9A26-9C2886981858","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8971435217b64c50e375aec68a6c58475d8d0dd9","datavalue":{"value":{"entity-type":"item","numeric-id":3249759,"id":"Q3249759"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102282$D3616B42-6506-449D-87D1-8D90B0068B80","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":"Q1102282$FA8A5C57-5A41-4700-B168-0B9891D8DE2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d8c89dbd2855ba43daea8b45eab22e20a3e8e01e","datavalue":{"value":{"entity-type":"item","numeric-id":5667481,"id":"Q5667481"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102282$8A8F5D29-41A3-4F99-9462-90F5FD861D2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8d95625ec9e5b7c46cee42d87256157d982706a","datavalue":{"value":{"entity-type":"item","numeric-id":5559220,"id":"Q5559220"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102282$A6FD717F-A36A-49EA-AFC1-A82476D3CC9F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"341cf25e1331e9c3d9b625066b41f81f88fc1449","datavalue":{"value":{"entity-type":"item","numeric-id":5549033,"id":"Q5549033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102282$F4EB97CF-60D7-46E1-AE5A-05BD61DCA621","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16d8c6e78ca64cb5cd0571f9c0221eef165275e6","datavalue":{"value":{"entity-type":"item","numeric-id":5636315,"id":"Q5636315"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102282$5522E753-F364-4B52-AB34-B9D87B34D7B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"febba330446bda559f2952d624c63d67c91597ef","datavalue":{"value":{"entity-type":"item","numeric-id":5560258,"id":"Q5560258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102282$92BB0F7C-A4F1-4ACC-B644-F326BDCE539B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"24e9a7126fd3647b4929f8ad5e5b5d84f4d827a2","datavalue":{"value":{"entity-type":"item","numeric-id":2542723,"id":"Q2542723"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102282$4E551B8D-31FC-485C-BD9C-06851DE94383","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"dea4d26181e092ceca930761bfb0ba295313e63d","datavalue":{"value":"https://doi.org/10.1007/bf00370646","type":"string"},"datatype":"url"},"type":"statement","id":"Q1102282$0509957F-7990-429D-9324-4A816C948A69","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"221d86864bcc7bcd22ca562f2ab59025b2b8bc5a","datavalue":{"value":"W2084443499","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102282$C2531629-EB1D-4F1E-A735-0B4E83A29D5B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dc98fd3177bbd6c831ad4e9b86ec0d2843e074a3","datavalue":{"value":{"entity-type":"item","numeric-id":3338232,"id":"Q3338232"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bd24bf599f971c86e7e9b98e3d9663d37edc6a7f","datavalue":{"value":{"amount":"+0.8364589810371399","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":"Q1102282$A5562B57-88FE-418E-B203-25DCB8D3FF80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"87c143fa7014d6ab9009fa567823e114e3064b9a","datavalue":{"value":{"entity-type":"item","numeric-id":5236547,"id":"Q5236547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f0b2b3390528ca7a91844506ccd9e83d41ca6a84","datavalue":{"value":{"amount":"+0.8294418454170227","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":"Q1102282$F56CBA3E-8E92-4267-8D2B-7116E4CB2B43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ce1fa7696a58803451e25ea64c08937bc636481e","datavalue":{"value":{"entity-type":"item","numeric-id":670704,"id":"Q670704"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"27546e416ffe22e829c1a7010a88e720acc7a1ec","datavalue":{"value":{"amount":"+0.7777975797653198","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":"Q1102282$63725EE8-189E-4718-B758-84B50673603A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cfbf46aad459119c33004925957d08c945d98d6c","datavalue":{"value":{"entity-type":"item","numeric-id":4222817,"id":"Q4222817"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"50fb9f3c2811b462ce3194edf613641a18777a15","datavalue":{"value":{"amount":"+0.7510330080986023","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":"Q1102282$484236C7-EFA1-40F5-96A7-7D27C4F0B066","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fb5fb60d72e16ad991c6665a764621288819fa42","datavalue":{"value":{"entity-type":"item","numeric-id":843604,"id":"Q843604"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8d4656d5897f9c511555015d7ebb7f73c0cbd929","datavalue":{"value":{"amount":"+0.7397294044494629","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":"Q1102282$C77DD1A2-E32E-48D8-BD1A-346CC3BB7D37","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A compact representation of proofs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_compact_representation_of_proofs"}}}}}