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

DOI10.12775/LLP.2016.021MaRDI QIDQ4978553zbMATH OpenOpenAlexFDO

Authors Alexander Steen, Christoph Benzmüller

Publication date 11 August 2017

Published in Logic and Logical Philosophy (Search for Journal in Brave)

Full work available at URL https://doi.org/10.12775/llp.2016.021

zbMATH Keywords

automated theorem provingautomationhigher-order logicmany-valued logicmeta-logical reasoningnon-classical logicsemantic embedding

Mathematics Subject Classification ID

Many-valued logic (03B50)

Recommendations

• A cut-free system for 16-valued reasoning
• The power of Belnap: sequent systems for \(SIXTEEN_{3 }\)
• \(\mathrm{SIXTEEN}_3\) in light of routley stars
• Axiomatization of a basic logic of logical bilattices
• Some useful 16-valued logics: How a computer network should think
• On axiomatizing Shramko-Wansing's logic
• Interpolation in 16-valued trilattice logics
• Revisiting four-valued logics from \textit{Maple} using the \textit{Logics Explorer} package
• Correspondence analysis for first degree entailment
• scientific article; zbMATH DE number 475182

Cited in

(5)

• Extensional higher-order paramodulation in Leo-III
• scientific article; zbMATH DE number 7561490 (Why is no real title available?)
• Automated proof-searching for strong Kleene logic and its binary extensions via correspondence analysis
• Gödel's God in Isabelle/HOL
• Exploring Simplified Variants of Gödel’s Ontological Argument in Isabelle/HOL

Describes a project that uses

Uses Software

• Coq
• Isabelle/HOL
• Nitpick
• TPTP
• Satallax
• Leo-III

This page was built for publication: Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4978553)