{"entities":{"Q1338893":{"pageid":1349632,"ns":120,"title":"Item:Q1338893","lastrevid":68500572,"modified":"2026-04-13T00:07:44Z","type":"item","id":"Q1338893","labels":{"en":{"language":"en","value":"A typed logic of partial functions reconstructed classically"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 695001"}},"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":"Q1338893$D61D8139-F7E7-4D7C-A9A9-4073E86FDDEE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"da78522356c8fcfc82370b2ebf6b357332ed0100","datavalue":{"value":{"text":"A typed logic of partial functions reconstructed classically","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1338893$2AFD8E10-49A1-4897-A74B-AEB8D4216FE0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"81d8475f3bad00907bf47c299b74a21164ff1b2d","datavalue":{"value":"0804.03018","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1338893$03A461A5-CC8F-4DF7-8D18-F5D5AFCF07EA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"69e0c348dd0380072bb9a2b28083160574d3245f","datavalue":{"value":"10.1007/BF01178666","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1338893$98612792-251A-44D3-87C8-E37BF8A8942D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"24d2f620d2974ebdd1015229debd06431f4c7398","datavalue":{"value":{"entity-type":"item","numeric-id":1294575,"id":"Q1294575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1338893$C7703715-D808-4E20-8549-B38F6A8CCD13","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7d0f02e85530cd06ceb2c58a40dc9c2e0258e194","datavalue":{"value":{"entity-type":"item","numeric-id":161641,"id":"Q161641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1338893$7DBB5A7A-723A-4D15-9FC8-72A7FEEEE19B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ef98405a763dc3b6f5996340a567615bbdffa2ff","datavalue":{"value":{"time":"+1995-01-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1338893$40B0F788-173B-491C-AC0F-DF6897428A4E","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"e591fbe37f65d18a9e97941bd559bc8f53d537e6","datavalue":{"value":"This paper gives a comprehensive description of a typed version of the logic known as LPF. This logic is basic to formal specification and verified design in the software development method VDM. If appropriately extended to deal with recursively defined functions, the data types used in VDM, etc., it gives the VDM notation and its associated rules of reasoning. The paper provides an overview of the needed extensions and examines some of them in detail. It is shown how this nonclassical logic -- and the extensions -- can be reconstructed classically by embeddings into classical infinitary logic.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1338893$077B8AFB-4B30-4E0F-85BA-FEBDA4AFFA85","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1338893$9F547DF0-A28F-4575-A8A2-E5770AD723D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1338893$F9A2C1E2-94C5-4085-8F2B-A5D6CF790E5F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2ee7904fc9b8e57d16f17863c6254e0e5ed54fe6","datavalue":{"value":"695001","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1338893$1FE081F7-65FF-42F9-B4C0-F63242C81B4C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8a654d00e7a0a6ae91735c829fdcaa4b9607205a","datavalue":{"value":"logic LPF","type":"string"},"datatype":"string"},"type":"statement","id":"Q1338893$D9035740-28D7-47D1-9891-1FD06CBFBA62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"87994eb840961e5165378eb7f918102952689b42","datavalue":{"value":"formal specification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1338893$C7574324-4C08-47B8-9A79-1F8B820C8039","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bd984aa67368df334c786e1ded77e4d3f3c34c6b","datavalue":{"value":"verified design","type":"string"},"datatype":"string"},"type":"statement","id":"Q1338893$9B60E1C6-8494-4DB3-B0C8-5A6040604C26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d5909b27ab5925f09a17112c9896c1e107faf535","datavalue":{"value":"software development method VDM","type":"string"},"datatype":"string"},"type":"statement","id":"Q1338893$39C0E138-4F11-4D3C-A53E-CE6E8558ADB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6558870aa0dc5d9a99ee710093f335e5897472b0","datavalue":{"value":"embeddings into classical infinitary logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1338893$F92BCE74-2F70-48A3-A5DC-E844002160A9","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":"Q1338893$34B5A9BA-3495-4D68-ABCB-2333A1F17847","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3f474b409a8f3415f67c4fa840940f857e860d83","datavalue":{"value":{"entity-type":"item","numeric-id":790610,"id":"Q790610"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1338893$0B7C44CC-CB67-4AD8-BAED-7DDC11963802","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"842185ee810e891a84aa7366eeec94e364ed8d6f","datavalue":{"value":{"entity-type":"item","numeric-id":4296956,"id":"Q4296956"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1338893$5B0E4690-0262-44A4-BC1A-368D09CDECE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d1739c2b55475dfd43cc45c16cc81ebdb6214ea","datavalue":{"value":{"entity-type":"item","numeric-id":2547549,"id":"Q2547549"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1338893$3CABC100-E7C0-4DED-ABB5-B76282565D0D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b21834d69bd3a3794ea50a3b9c4b2646685b26aa","datavalue":{"value":"https://doi.org/10.1007/bf01178666","type":"string"},"datatype":"url"},"type":"statement","id":"Q1338893$4E3D8AD1-1C98-42D2-9F74-03B1E5D7E157","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"674c2ba1890385f8eab0ea425cbb4b6a78f3263e","datavalue":{"value":"W2030221869","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1338893$6E938049-F60F-4530-B764-F3AEACDEBA3D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"671ec0799344f16cd6c6d298783843edad6951e1","datavalue":{"value":{"entity-type":"item","numeric-id":963419,"id":"Q963419"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1eb972697ec1269465a6453f0a293a3c74d7ebf0","datavalue":{"value":{"amount":"+0.7628653049468994","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":"Q1338893$4CC2ABDE-52D7-4ECB-96AB-6D74E9F8746D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"76eb68d4640da445cf7a35c96d83a37a0bc014ba","datavalue":{"value":{"entity-type":"item","numeric-id":352946,"id":"Q352946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dfc2c35ea9b15423175fafe71e5b50662fa85429","datavalue":{"value":{"amount":"+0.7531130313873291","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":"Q1338893$1FE4232F-AA5D-4E86-97C5-4EA70202BD1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8119ec3aa981e9a9db002ac60c0b87fa899679f0","datavalue":{"value":{"entity-type":"item","numeric-id":679251,"id":"Q679251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3ccf75f071f40f1fe8fa75542c88e2246855a9ad","datavalue":{"value":{"amount":"+0.7491804361343384","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":"Q1338893$30A4BF4F-A135-4C9F-B0D4-2AE1778322A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d2c74bf2b0c7d1a63590adb2435675382a829aa9","datavalue":{"value":{"entity-type":"item","numeric-id":438568,"id":"Q438568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"43c64cb4324205fbeedd4c58903f854ad6e37c14","datavalue":{"value":{"amount":"+0.7472634315490723","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":"Q1338893$ABEE18D2-F9A9-47E9-BF86-F293ACE88E1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"272d43b608027d1551c02fdad11d1a4ad4b18f45","datavalue":{"value":{"entity-type":"item","numeric-id":2863853,"id":"Q2863853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"750bcd01fbdca4f7e4128e6a509e715c4ad0413d","datavalue":{"value":{"amount":"+0.7451635599136353","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":"Q1338893$A3A2C56D-5590-403A-90EA-330DD106029F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A typed logic of partial functions reconstructed classically","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_typed_logic_of_partial_functions_reconstructed_classically"}}}}}