Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
Journal Title: Logic and Logical Philosophy - Year 2016, Vol 25, Issue 4
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.
Authors and Affiliations
Alexander Steen, Christoph Benzmüller
Keywords
Related Articles
- EP ID EP202232
- DOI 10.12775/LLP.2016.021
- Views 88
- Downloads 0
Set-theoretic mereology
We consider a set-theoretic version of mereology based on the inclusion relation ⊆ and analyze how well it might serve as a foundation of mathematics. After establishing the non-definability of ∈ from ⊆, we identify the...
Mereology and Infinity
This paper deals with the treatment of infinity and finiteness in mereology. After an overview of some first-order mereological theories, finiteness axioms are introduced along with a mereological definition of “x is fin...
Sequents for non-wellfounded mereology
The paper explores the proof theory of non-wellfounded mereology with binary fusions and provides a cut-free sequent calculus equivalent to the standard axiomatic system.
Partial and paraconsistent three-valued logics
On the sidelines of classical logic, many partial and paraconsistent three-valued logics have been developed. Most of them differ in the notion of logical consequence or in the definition of logical connectives. This art...
Mereology and truth-making
Many mereological propositions are true contingently, so we are entitled to ask why they are true. One frequently given type of answer to such questions evokes truth-makers, that is, entities in virtue of whose existence...