{"entities":{"Q1058285":{"pageid":1060133,"ns":120,"title":"Item:Q1058285","lastrevid":67016385,"modified":"2026-04-12T14:21:19Z","type":"item","id":"Q1058285","labels":{"en":{"language":"en","value":"Proving properties of Pascal programs in MIZAR 2"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3900133"}},"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":"Q1058285$84C729FD-B87E-48D4-820C-8CBFFB2CD42C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b7c6666b971b0ab798c7a52c59bb0c62f6f76281","datavalue":{"value":{"text":"Proving properties of Pascal programs in MIZAR 2","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1058285$E003616E-E7E8-406F-AF49-B1CFA22135FD","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c1c548a880fa3c705088dfa08c2724bec3e9a47b","datavalue":{"value":"0564.68010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1058285$6085AE87-EDB3-4B1B-B7F4-12C2BB70A784","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4c6407da1aef8968d0ff8fb45c8e49e0fe96f4a6","datavalue":{"value":"10.1007/BF00265684","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1058285$F0F0F70E-86B7-4CC7-AE73-670476E1B392","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9d72ee9ffde9510a13b5bea91934f187bdc57c7e","datavalue":{"value":{"entity-type":"item","numeric-id":467775,"id":"Q467775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1058285$AFAF1B57-40FF-4C20-BAA6-5C0C7B0D1F92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"aca37643c25c4f7a18b2bf47f8e6a1980c00131e","datavalue":{"value":{"entity-type":"item","numeric-id":511026,"id":"Q511026"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1058285$224E2D1C-62EE-4013-BCFA-A40D0CDDD508","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":"Q1058285$88464478-AB9C-4CF5-9110-C5F05803F251","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":"Q1058285$717E7E51-966B-477A-B508-14CC7503E527","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"22c7da5b24067d37d2f7b3b910ba36e8d72fd553","datavalue":{"value":"In this paper we present the so called natural semantics for a subset of Pascal programming language. A set of sentences of first order predicate calculus defines the meaning of the Pascal language constructs. The meaning of a specific program is defined separately by another set of sentences which can be generated automatically. Both these sets together constitute axiomatics of a theory, called the theory of a specific program. The axiomatics is built in such a way that its logical consequences describe all the computational processes defined by the program. Proofs of properties for two small programs are discussed in detail. These properties and their proofs are recorded in the MIZAR 2 language - a computer formalization of predicate calculus. MIZAR 2 proof checker was used to verify the proofs.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1058285$FC7AAFA1-EF33-45DF-8633-BA40D2C026B1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1058285$9D9DB8D1-5CFB-422E-9884-986769F36DBA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"048532e7082a5722bd8fce0d0cd173c60bebe55b","datavalue":{"value":"3900133","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1058285$3999156C-4963-4B3F-A531-9E0FBCE934F4","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d7bfc11de8cab95fd6af201970bd9d16d39bbd0","datavalue":{"value":"semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1058285$A9170BC1-CA29-483E-9BEB-D3E255B43EB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7227247e26a7a4e3cf718a9747f1fd0491872cd1","datavalue":{"value":"predicate calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1058285$D80E886D-97F0-4ED9-BC74-5567046B9361","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1b4aec64d6f8f9b51dd6f9005c1e4cd40043c556","datavalue":{"value":"Pascal language constructs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1058285$A090C86C-E1C6-4293-9B45-3FAC76FF08E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e184a28d18586b79620daaac315907b7ccd8679c","datavalue":{"value":"MIZAR 2","type":"string"},"datatype":"string"},"type":"statement","id":"Q1058285$BFBCFBFA-4409-4C87-8944-82A6529E9F64","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1058285$4AD3E172-25D0-4D63-82CC-7B5637351AC2","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":"Q1058285$799D198F-EF3D-4108-A2B6-3A5AE5C7BAED","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d1fd206acf881022e2cabc3cf043a1ab6fef5fda","datavalue":{"value":"https://doi.org/10.1007/bf00265684","type":"string"},"datatype":"url"},"type":"statement","id":"Q1058285$0938C1F3-499D-4BF9-8435-EA2BE30D3F7B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"069f6d38b17c8e0b0e604055809104dfffd636bf","datavalue":{"value":"W2094822356","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1058285$66BA5C39-1335-4938-AF04-78C0175DEB6F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3a39a2cb9e8db094cb4da26da228b833592e4016","datavalue":{"value":{"entity-type":"item","numeric-id":796289,"id":"Q796289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8d0a9dd4de7e057abae0b65e4706c60ab85dcddf","datavalue":{"value":{"amount":"+0.7648893594741821","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":"Q1058285$E7ECBAAD-83F5-470D-9281-E085157CADCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"678c0c38f6268df2cba63533bb44a641d219e574","datavalue":{"value":{"entity-type":"item","numeric-id":3197301,"id":"Q3197301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e0f690a32d4f4d66590b85f0390de3dd33448e7d","datavalue":{"value":{"amount":"+0.7516035437583923","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":"Q1058285$220D4D78-89A1-4836-978A-0FD907753E12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5add08a5d004f50146f4311c1ba27d67f8ad1f8e","datavalue":{"value":{"entity-type":"item","numeric-id":3477935,"id":"Q3477935"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9c78e1f66ec96514bba9c16f5bd34dcc7b092000","datavalue":{"value":{"amount":"+0.7356245517730713","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":"Q1058285$88AF18B8-1F7E-454B-ABF5-DBB294FD3962","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":"35ab0a684d8d92c26af2fc638c71f51c9d2611a3","datavalue":{"value":{"amount":"+0.7351419925689697","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":"Q1058285$88309F86-759F-488D-A489-C781EF3B10CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1c52a4a8a8811963fe180a97c565b57c9351d2fd","datavalue":{"value":{"entity-type":"item","numeric-id":3326831,"id":"Q3326831"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c8982d7f1478440ecd737e4cefb42e980ab11e58","datavalue":{"value":{"amount":"+0.7343822121620178","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":"Q1058285$64955FDD-13A8-4185-AA18-E0E2DC72A177","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proving properties of Pascal programs in MIZAR 2","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Proving_properties_of_Pascal_programs_in_MIZAR_2"}}}}}