{"entities":{"Q2471743":{"pageid":2482486,"ns":120,"title":"Item:Q2471743","lastrevid":72731454,"modified":"2026-04-14T07:11:37Z","type":"item","id":"Q2471743","labels":{"en":{"language":"en","value":"On the mechanization of the proof of Hessenberg's theorem in coherent logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5236603"}},"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":"Q2471743$CD1E505D-6A98-4C72-8098-7151B0509F13","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"822fec761be6496730176eef2a079ba922a459ef","datavalue":{"value":{"text":"On the mechanization of the proof of Hessenberg's theorem in coherent logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2471743$CFF30D21-E47B-41B7-9529-25337310C11F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b42d3cfcb53ca8e5ea2da4a0509793de52e6597d","datavalue":{"value":"1140.03004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2471743$21D67801-3F0F-4072-A7B0-8D72B5266D42","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"86dd1292a8b5a1afaa94642cc6a7d0169c59a759","datavalue":{"value":{"entity-type":"item","numeric-id":409313,"id":"Q409313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$BDE98617-6B7A-41D0-8FA9-875D5F284822","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3ca9aba1d27cc0a527c5e55e40b675c206cdc1e1","datavalue":{"value":{"entity-type":"item","numeric-id":549187,"id":"Q549187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$1C757B44-5E4D-4410-ADD0-2AEB86FE5285","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":"Q2471743$A4DC7DE8-4ED6-4192-BC07-62A7C80CA9D2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"118eb39459fbba91acbfa1c46ee7e29cd76ebdf5","datavalue":{"value":{"time":"+2008-02-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2471743$DF9DEB80-AA48-42ED-89AC-0CC646C06F45","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7165d315bbf4fc6999ccd8ce96fdd4c9c2ae49a9","datavalue":{"value":"https://research.vu.nl/en/publications/23049501-068c-48b6-be93-fec9c22ca4d6","type":"string"},"datatype":"url"},"type":"statement","id":"Q2471743$9C021B7F-C8AE-462A-A651-CCC013C94808","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"fe27f96bd70097231bb5d6f28806b7373763f6d2","datavalue":{"value":"General-purpose automated theorem provers are not yet able to prove difficult theorems. The formal verification of difficult theorems requires human ingenuity.   The authors propose to combine interactive proof construction with proof automation for a fragment of first-order logic called coherent logic (CL). CL allows to make Skolemization unnecessary and has a natural proof system based on forward reasoning. This approach was tested by formally proving Hessenberg's theorem in elementary projective plane geometry.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2471743$AE312973-0D59-4A2E-B4CD-F4FA9317D457","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2471743$D00E7A6B-1C5D-4788-B512-F664FF9B1E17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c06e0874e30722381d620ef69fb36c407a01cb04","datavalue":{"value":"03B10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2471743$A939BDA0-C5D9-487B-A5FB-368391C00F2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2471743$684E4D9A-0A8F-40E4-8277-60F63D50BE6C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f1958106a796532662682dd1e58aacbc4b33f8f7","datavalue":{"value":"5236603","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2471743$E2463B5B-A271-4F18-A1B7-899B8F6B6EE1","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"223556ef87b8f25f218d19756cbdf5e24d0a2719","datavalue":{"value":"coherent logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2471743$AB1579AA-06F3-4300-89F2-0E8E7DE70C52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2471743$17031AE6-AEE7-46DC-AA9D-96BA2E818415","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e0885033cf4b16d0fe54f08ae6472e825daee282","datavalue":{"value":"proof objects","type":"string"},"datatype":"string"},"type":"statement","id":"Q2471743$01053E7E-45E5-4963-BE07-BB2905F741B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3bc15aad2cb03f62c8f0e19bb19148bc00e8c059","datavalue":{"value":"Hessenberg's theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q2471743$028BDF81-54FA-4775-80F5-4C5D59B3134A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e412acfc7e10f891239cff44b5ad91c2634be70b","datavalue":{"value":"projective plane geometry","type":"string"},"datatype":"string"},"type":"statement","id":"Q2471743$464739F7-31D3-465D-B1FF-162B70B38285","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"05f3dff3edc7d97b14af7ecb326f488fb3fee31b","datavalue":{"value":{"entity-type":"item","numeric-id":583186,"id":"Q583186"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$908C85A1-CDE6-4DE1-B545-392C4E802204","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$6EEEE0FC-AEFC-4F45-B8C1-BAA3686A2B83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$DAAC52A9-3896-4644-BCD9-2BCC96B4E4FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e3fa1be4925f6565903e34254fe3ce3cb99beabc","datavalue":{"value":{"entity-type":"item","numeric-id":18828,"id":"Q18828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$002B8C99-08FF-4AA2-B841-B644EFB4A2D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$7F1092D1-EFAA-4E27-A688-32C77EE5958F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9301974fbdbf3896f705a4c8ed840f169a9b63f","datavalue":{"value":{"entity-type":"item","numeric-id":19182,"id":"Q19182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$C7CBA6EA-255A-4FBC-9A93-04BE4A372C77","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":"Q2471743$E776842E-DF75-4CC8-A63A-0B4B04E6D122","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7e8cebc4c897da5c4038b28a0b04ca1f03c6fdc5","datavalue":{"value":"W2142703483","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2471743$E68B4238-461B-4BA1-A932-8E7EC94D66E0","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b9f30a506579d570709211d696ed5ba11d9cc6f","datavalue":{"value":{"entity-type":"item","numeric-id":4665735,"id":"Q4665735"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$7B5E13E8-E93C-48C1-8C41-C545507E958A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"30492f77eb016746469a740ef03c349aed405ecd","datavalue":{"value":{"entity-type":"item","numeric-id":5387843,"id":"Q5387843"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$F3963A43-418A-43CC-8E3F-38DC9039E129","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4678e4c2f003554895218494da0c1f6e87bb3ea","datavalue":{"value":{"entity-type":"item","numeric-id":1868508,"id":"Q1868508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$8D08DA35-2904-4421-BE43-2D46A9DD9A98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4370175d8030918ba7fe1c9ab8112224b76824d","datavalue":{"value":{"entity-type":"item","numeric-id":3498463,"id":"Q3498463"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$E0AF872A-5B15-48EE-A5A2-234D7738EB94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fbe7c29edfc603f81cbf3471ffc407d4a954e5e0","datavalue":{"value":{"entity-type":"item","numeric-id":5850099,"id":"Q5850099"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$062A4E1A-5CD2-4796-808F-D5FF15F1B3BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"37cbf3dde76acfad2bb612f8636a09ea1ff087e4","datavalue":{"value":{"entity-type":"item","numeric-id":5821577,"id":"Q5821577"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$E0795D16-975D-452F-8034-7A7646CE4CE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"04c0523630e1e6c8f44c947a834580b7eb080727","datavalue":{"value":{"entity-type":"item","numeric-id":2486578,"id":"Q2486578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$D2C36689-FFA2-42DE-B302-A29C2306044E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4bf54fd52b3ae148a01d4229df0c1b5a1e68af7f","datavalue":{"value":{"entity-type":"item","numeric-id":3613415,"id":"Q3613415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$F4125820-DE6D-43E8-8FEE-4C3726EC2A2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"021e6e2184fd3d7f831680d56b426b95217eac7a","datavalue":{"value":{"entity-type":"item","numeric-id":4033837,"id":"Q4033837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$0A6D9ED2-DA4E-4DCB-BF3A-8A6DD8B72D58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"41bd2cc0badda1bd2b407ae76037505554d94b2a","datavalue":{"value":{"entity-type":"item","numeric-id":4828514,"id":"Q4828514"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$36F981A8-FDEA-4967-B176-2DBE229DDFEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03cbc69cab2b7d5069acc953a5626227ed8c07a0","datavalue":{"value":{"entity-type":"item","numeric-id":1340050,"id":"Q1340050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$BAC450F6-6047-4B05-B8A7-F7B6AA05735B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$590CDE11-CBBD-4239-982D-40147FD1A745","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42ba0d7a787c3ddf27f1ee78a59c4dec37184a75","datavalue":{"value":{"entity-type":"item","numeric-id":4520767,"id":"Q4520767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$C974EAA7-5D4E-47EC-9DF8-6514E6EC181D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"309a715ecfe3fe3e4ec0e698ae13dce021cfc93e","datavalue":{"value":{"entity-type":"item","numeric-id":2724150,"id":"Q2724150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$53D796D6-A514-427B-98F1-A001D0233298","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c5b09e879fc9e6d166a18cb26ec583e2bf401aa","datavalue":{"value":{"entity-type":"item","numeric-id":1272614,"id":"Q1272614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$9873F5E4-FD34-4553-B026-4B68538CFC7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66ed1fd88663850940208777b453a5e31171f5d4","datavalue":{"value":{"entity-type":"item","numeric-id":5486135,"id":"Q5486135"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2471743$49AA3683-97EE-4F2C-A9DE-F9E42F701F2C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a1672b247bf00803a30717aeaa037a1e952a1dcf","datavalue":{"value":"10.1007/S10817-007-9086-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2471743$1795AFFE-8320-4B1E-8EC8-49C10B928C6A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"37ed56f054f2c4d95c0e23622653d6f12097a0ba","datavalue":{"value":{"entity-type":"item","numeric-id":5387843,"id":"Q5387843"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fe9bd48a9d75758cfeff2ac1806c136d461feda4","datavalue":{"value":{"amount":"+0.8759040236473083","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":"Q2471743$7DF16AD8-4C61-4480-B66C-642C46D0DB44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c69d2638618b1398e223482eea704c8301b9fd6b","datavalue":{"value":{"entity-type":"item","numeric-id":3102745,"id":"Q3102745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a345174bf98aa6bcca69604a96f9584653dc9d42","datavalue":{"value":{"amount":"+0.7888258099555969","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":"Q2471743$6D44FC10-D5ED-4867-841D-D6F66BA8D5FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a760c74583d2c9fd3acc648ecc03c499f5e936ea","datavalue":{"value":{"entity-type":"item","numeric-id":5495937,"id":"Q5495937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f629d88e110fd1a1a112e11161b7d6267a658a73","datavalue":{"value":{"amount":"+0.7515387535095215","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":"Q2471743$60AF724D-6DED-4400-B3F6-D61EAE2D8DFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c4043424a019ad7473006eca39e1b8daadbac8cf","datavalue":{"value":{"entity-type":"item","numeric-id":2102932,"id":"Q2102932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"69da3b05bbfcd1e8257b1af7dfdb74d5fe16383e","datavalue":{"value":{"amount":"+0.7512621879577637","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":"Q2471743$55F39398-957C-45B0-B6ED-949FA8B18040","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ff044de1c8ab53ceae087038db232905f546e4ff","datavalue":{"value":{"entity-type":"item","numeric-id":2907328,"id":"Q2907328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1f8f28b5e7899e9ddfecd43b6c2d4bb173fbb5b7","datavalue":{"value":{"amount":"+0.7468981146812439","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":"Q2471743$8F3A50C6-0BE0-43BE-916F-6124413BCA85","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On the mechanization of the proof of Hessenberg's theorem in coherent logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/On_the_mechanization_of_the_proof_of_Hessenberg%27s_theorem_in_coherent_logic"}}}}}