Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic

C. Benzmüller, A. Steen— 2016

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.

TitelSweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
VerfasserC. Benzmüller, A. Steen
Themamany-valued logic; non-classical logic; higher-order logic; automated theorem proving; semantic embedding; automation; meta-logical reasoning
KennungDOI: http://dx.doi.org/10.12775/LLP.2016.021
Erschienen inJournal of Logic and Logical Philosophy; Vol 25, No 2 (2016): June 2016