Towards Fully Automated Axiom Extraction for Finite-Valued Logics

Abstract. We implement an algorithm for extracting appropriate collections of classic-like sound and complete tableaux rules for a large class of finite-valued logics. Its output consists of Isabelle theories.1 Key words: Many-valued logics, tableaux, automated theorem proving.

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Dalmo Mendonca, João Marcos
• Keywords: Appropriate Collections, Automated Reasoning, CADE 2008, Classic-like Sound, Complete Tableaux Rules