Quantifiers and n-ary binders: an OpenMath standard enhancement proposal
2013 (English)In: Proceedings of the MathUI, OpenMath, PLMMS and ThEdu Workshops and Work in Progress at CICMco-located with Conferences on Intelligent Computer Mathematics (CICM 2013), Aachen: Redaktion Sun SITE, Informatik V, RWTH Aachen , 2013Conference paper (Refereed)
It is proposed that the restriction in the OpenMath standard that an OMBIND element must have exactly three children should be lifted, to support more general binder symbols. The case of logics with generalised quantifiers is described in some detail, since these turn out to not have a natural encoding within OpenMath 2.0, because of precisely this restriction. That restricting quantifiers to a single body should have such consequences is not trivial, but follows from a theorem in the Logic branch of Philosophy.
Place, publisher, year, edition, pages
Aachen: Redaktion Sun SITE, Informatik V, RWTH Aachen , 2013.
, CEUR Workshop Proceedings, ISSN 1613-0073 ; 1010
OpenMath, binder, XML encoding, binary encoding, Lindström quantifier, second-order logic, general logics, condition clause
Algebra and Logic Software Engineering
Research subject Mathematics/Applied Mathematics
IdentifiersURN: urn:nbn:se:mdh:diva-21081OAI: oai:DiVA.org:mdh-21081DiVA: diva2:642953
MathUI, OpenMath, PLMMS and ThEdu Workshops and Work in Progress at CICMco-located with Conferences on Intelligent Computer Mathematics (CICM 2013), Bath, UK, July 9 - 10