{"entities":{"Q935562":{"pageid":937410,"ns":120,"title":"Item:Q935562","lastrevid":65468049,"modified":"2026-04-12T02:48:02Z","type":"item","id":"Q935562","labels":{"en":{"language":"en","value":"The higher-order-logic Formath"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5309617"}},"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":"Q935562$FD1F0C48-D615-408B-9E58-7CC41A42803B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5f6e77a4b458f77d09573f86e4024246cb26ca91","datavalue":{"value":{"text":"The higher-order-logic Formath","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q935562$A15C0C86-CC87-4197-899A-A0A5B3F27BB4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"df5f8678384b9fa2f28cc842ba4c4ec938e348ac","datavalue":{"value":"1168.03007","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q935562$9D92F9FE-C225-4A56-BCE8-8525F2B598BE","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4beb27d92a054647694070bc2ab63b4f72c3706b","datavalue":{"value":{"entity-type":"item","numeric-id":935561,"id":"Q935561"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q935562$AD7ADBEB-62B4-44B8-B2B2-A8C3D92380EE","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"c4f16ddc5cdb18d4f4fb3ee6d704d6609c3404ba","datavalue":{"value":{"entity-type":"item","numeric-id":223802,"id":"Q223802"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q935562$E2CB0C52-7508-4FC7-8ADF-81BD1FA8D353","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"58daf71822dde0c530d24a3c994f8cde05db9610","datavalue":{"value":{"time":"+2008-08-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q935562$DB132CC8-895F-4B20-BACC-C7DF6AA81541","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f92b08400fca6bf93f93f6876fb83910eb670b5e","datavalue":{"value":"https://projecteuclid.org/euclid.bbms/1210254829","type":"string"},"datatype":"url"},"type":"statement","id":"Q935562$9FE3E48A-D054-4B72-81D2-2B57A1017080","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"fc3682a8de52715e656f0c37e09d17866d5cd954","datavalue":{"value":"This paper describes in detail the logic Formath, inspired by two HOL derivatives: HOL-4 and HOL-Light. Formath is designed from the point of view of a mathematician. This results in the introduction of a syntactical distinction between bound and free variables, the use of ``de Bruijn'' indices and extending the consequences to more than one consequence. The author proves the soundness of his system and ends with an interesting comparison of Formath and the classical HOL-4 and HOL-Light variants. The logical strength of Formath seems to be the same as the more established versions, but the axiomatization is rather elegant and has several novel features (for this context), e.g., multiple-conclusion sequents and a syntactic distinction between free and bound variables using an approach similar to ``de Bruijn'' indices.","type":"string"},"datatype":"string"},"type":"statement","id":"Q935562$FDDBEDE2-242D-4A2C-B385-B2F97FAAE91A","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"a70eb255db58b1b2b90f33f4fe4a154901c6aeb8","datavalue":{"value":{"entity-type":"item","numeric-id":590723,"id":"Q590723"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q935562$9D407387-FF83-41EA-B044-451241087510","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q935562$1BB9EC83-5456-4C63-AEAA-196B7D7595A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q935562$9885D87F-92F6-47ED-9C71-C9CCADF0A38A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q935562$2A940B0A-C213-43BB-992A-CA18B61CCB7F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e9d1b9c7945069bd2575aef49718df9027cee6eb","datavalue":{"value":"5309617","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q935562$7959E929-7EC7-4857-9B8C-1E941D37F962","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q935562$63C1EBE3-166F-4BB2-9EC5-CBD8A3D98865","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q935562$853A77F8-CD5B-4F3B-AC57-EE997D93D14B","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q935562$F552DB6A-5F62-4B3D-BD0E-0F8830E6002C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c652637493e8de65377ba80065ca4183c6dc627","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q935562$65124DCF-B834-4EED-BE0B-243AE69F6CF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q935562$F6BE9BDD-4F71-46BF-A23D-6E2A7F560D04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q935562$ADE9D103-2CD2-4C68-B7CC-0A92DFEAFEBD","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":"Q935562$E9D9E3C6-8A58-4597-8E61-F321CFCFBD18","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5ca6b33a9f213e3f67729583300a9e1f98b54e7d","datavalue":{"value":{"entity-type":"item","numeric-id":287361,"id":"Q287361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2cdcda202e28e38bbbf53c67e29b88c5bcde32a0","datavalue":{"value":{"amount":"+0.7851929068565369","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":"Q935562$15347016-8B4B-46C5-A20A-9EDB1F60A98B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"db22c1910555c7985f9da455f58bf2494089862c","datavalue":{"value":{"entity-type":"item","numeric-id":3183533,"id":"Q3183533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e5c0c228781eb7afead94bde904f902e5e21e450","datavalue":{"value":{"amount":"+0.7597901225090027","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":"Q935562$5AA6215D-4E25-4021-9012-77D42EDF10D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dd29c2c601a7efad8109709c45c578bb5cf69f20","datavalue":{"value":{"entity-type":"item","numeric-id":4938612,"id":"Q4938612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7a534f7d6186afb1e0deab05a9b3ab672fd54254","datavalue":{"value":{"amount":"+0.7496224641799927","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":"Q935562$37384B9E-74CC-42E4-8807-4B34CAF9ECB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7ba65f6a58ed08b60fa73248e76ff032f9c8be87","datavalue":{"value":{"entity-type":"item","numeric-id":2722041,"id":"Q2722041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d3fe3b04b1ddb6528841a7b2431e453eb9ab2cae","datavalue":{"value":{"amount":"+0.7435392737388611","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":"Q935562$67D0CB65-A007-4EBD-AA17-2C9DD468452E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4c2077f4ad9245fc0d46fa3a52024b9f53a20a69","datavalue":{"value":{"entity-type":"item","numeric-id":2713352,"id":"Q2713352"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dbba50e35a73f9e384cfc0305d7b88cdcc62a835","datavalue":{"value":{"amount":"+0.7363520264625549","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":"Q935562$7095FD0A-F886-4873-ABAC-EBDE6464B007","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The higher-order-logic Formath","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_higher-order-logic_Formath"}}}}}