{"entities":{"Q1820596":{"pageid":1831338,"ns":120,"title":"Item:Q1820596","lastrevid":49048471,"modified":"2026-01-06T12:49:21Z","type":"item","id":"Q1820596","labels":{"en":{"language":"en","value":"Writing programs that construct proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3997192"}},"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":"Q1820596$F76FF73C-2238-4CC0-927D-B7255091B3B1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c8eacf90e7efe74622f8b2bb67d74301d61806d5","datavalue":{"value":{"text":"Writing programs that construct proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1820596$85CC5897-2CA1-407C-B071-765877F8E8D0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f5750026dbbf4c6f50a56d2ed128bffc04e1cef5","datavalue":{"value":"0615.68063","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820596$F69868F6-5496-4BB1-B65D-53D40E6A9443","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4ea06b7c2c451a3f7e1dc76ab15088c2aa13bb97","datavalue":{"value":"10.1007/BF00244273","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820596$B8F28FAD-0BE0-442A-9728-E580F4A52EDF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"07c61d17a24bbf93457999d41308767000b8ac14","datavalue":{"value":{"entity-type":"item","numeric-id":1820594,"id":"Q1820594"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820596$4CEC5AFA-E3C4-43C7-82E3-9D508B87AC71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b9797322a68734871b704c448a0fe6e23f76b7cc","datavalue":{"value":{"entity-type":"item","numeric-id":1820595,"id":"Q1820595"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820596$19726D00-CE72-4D9C-8F8C-B409D3DB88BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c9f99e72dec046038a5377ceee67d8841bab629f","datavalue":{"value":{"entity-type":"item","numeric-id":1051423,"id":"Q1051423"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820596$54AC61E7-ACA2-4FB6-A507-BB9B205BFD03","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":"Q1820596$0B725980-033E-4A56-AA07-657C6B4C106F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3c94df5c9af0ede578c52141befd29044de13172","datavalue":{"value":{"time":"+1985-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":"Q1820596$D8B9BECF-EFC8-4CC5-BF16-2D94A3E19CC1","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"a326a7e48ffc250c03cb016152fc0e139319c95e","datavalue":{"value":"When we learn mathematics, we learn more than definitions and theorems. We learn techniques of proof. In this paper, we describe a particular way to express these techniques and incorporate them into formal theories and into computer systems used to build such theories. We illustrate the methods as they were applied in the \\(\\lambda\\)-PRL system, essentially using the ML programming language from Edinburgh LCF as the formalized metalanguage. We report our experience with such an approach emphasizing the ideas that go beyond the LCF work, such as transformation tactics and special purpose reasoners. We also show how the validity of tactics can be guaranteed. The introduction places the work in historical context and the conclusion briefly describes plans to carry the methods further. The majority of the paper presents the \\(\\lambda\\)-PRL approach in detail.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1820596$A817CCDF-AF99-4ADD-A0BC-F88540D7DACC","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820596$0EEAB057-6CA4-49D1-A958-0AF85D0B27B5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7bedabdd23db93d691117b233755cd5234ce2851","datavalue":{"value":"3997192","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820596$7392DB44-533A-49AF-AC26-314E0933C6B2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"79e10659ec0ab4c1636b61cba98e7ea0e00939e8","datavalue":{"value":"Automath","type":"string"},"datatype":"string"},"type":"statement","id":"Q1820596$65F8A32B-8C80-48D0-B2D9-082B3DEA7FFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ca1042868ff4f694776e4b2c62ec66638c4ef91","datavalue":{"value":"automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q1820596$E34BBCEE-827C-4CC5-BF4B-34BE9226128A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dfd2ae52b3325778b0c72742b08c947a3c4a2c65","datavalue":{"value":"decision procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q1820596$E647CBF3-68D4-479F-BE97-F717B515419A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bc238ea6cb52c715bab39832f2cd5b4837c9294f","datavalue":{"value":"formal mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1820596$2C08AD75-3A13-4FB6-AF87-22E33B502AD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2841995a1bcc2953bd7470177d889bb4a3d2f2c7","datavalue":{"value":"intelligent systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1820596$097D5B07-57A8-4B95-94ED-33929730B013","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4a614927b0caf638748bb51c0de92c1b49104311","datavalue":{"value":"proof checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q1820596$2A5D2A13-70ED-414C-865C-3E1D28292D87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ec5ef65a64ed2128194a82dc20f744211e7d7bfd","datavalue":{"value":"LCF","type":"string"},"datatype":"string"},"type":"statement","id":"Q1820596$565896CA-5C1B-48CA-BEC1-9C7971715193","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"25db55153babd7076d594d911b639e78d62b451a","datavalue":{"value":{"entity-type":"item","numeric-id":20369,"id":"Q20369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820596$3E36D8B8-0C8D-4DF2-93A6-67DE321A9C75","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":"Q1820596$81B29237-E8A0-4193-9618-2474D24E42B3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"43f4c5751039a2473f42634aa8eb47ee3015788f","datavalue":{"value":"https://doi.org/10.1007/bf00244273","type":"string"},"datatype":"url"},"type":"statement","id":"Q1820596$1D3C98CA-0E2E-42F2-9040-E84199B84BB1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"caea9ceee1920f13ae1542c8bb42fdb3e82e8699","datavalue":{"value":"W2019651724","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820596$93488D86-28C4-4A0A-9D90-580EA7AACBDB","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"59f8ddf71b2d5cd28cd251b780e95170840ac8ba","datavalue":{"value":{"entity-type":"item","numeric-id":1408657,"id":"Q1408657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c2a3bb1d19a3aba036a6943ef81fb614a9f07807","datavalue":{"value":{"amount":"+0.8041334748268127","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":"Q1820596$CEEF9286-3C21-4CB9-9387-BDDBB04CBBA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ab6ba7746db3411117fef3a34be889dfb4c4e69a","datavalue":{"value":{"entity-type":"item","numeric-id":5448310,"id":"Q5448310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2d213e5bcc538fcf5dff7fc29bb7a13952f828ea","datavalue":{"value":{"amount":"+0.7782190442085266","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":"Q1820596$43CBBD22-DF94-4593-BBF3-85A3237C535F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"787bce44c26bfa68c4bdd6a337d32f1925d9a163","datavalue":{"value":{"entity-type":"item","numeric-id":3757915,"id":"Q3757915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eb2463b77a3f8228004c74cdeb83ff0fae1c8175","datavalue":{"value":{"amount":"+0.7706506848335266","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":"Q1820596$09321AC6-9794-4CD2-BD2A-36C39D70E880","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"595f6616d7f7c7bdbfd5649089c6877995bc6cce","datavalue":{"value":{"entity-type":"item","numeric-id":2018656,"id":"Q2018656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1aa4e256bfb1f27736e1737ca0ef03cac9fe4332","datavalue":{"value":{"amount":"+0.7699978351593018","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":"Q1820596$D66A8E9D-7A9F-4386-BD2D-25D3AD8B2997","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fe7a7c4f5dac6dd56f6689fbd94d027549e0a9bd","datavalue":{"value":{"entity-type":"item","numeric-id":5756755,"id":"Q5756755"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"51225e9c60a585d3065b6fa1d4ee0a1c9320adff","datavalue":{"value":{"amount":"+0.7663069367408752","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":"Q1820596$BF553AB6-FBA1-4942-A845-0558A4AF4B8C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1820596","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1820596"}}}}}