Sweet sixteen automation via embedding into classical Higher-order logic

Abstract

An embedding of Many-valued logics based on SIXTEEN in classical Higher-order logic is presented. SIXTEEN generalizes the Four-valued set of truth degrees of Dunn/Belnap’s system to a lattice of sixteen truth degrees with multiple distinct ordering relations between them. The theoretical motivation is to demonstrate that Many-valued logics, like other Non-classical logics, can be elegantly modeled (and even combined) as fragments of classical Higher-order logic. Equally relevant are the pragmatic aspects of the presented approach: interactive and automated reasoning in Many-valued logics, which have broad applications in computer science, artificial intelligence, linguistics, philosophy and mathematics, become readily enabled with state of the art reasoning tools for classical higher-order logic.