A tableaux calculus for default intuitionistic logic

DOI10.1007/978-3-030-29436-6_10zbMath1486.03018OpenAlexW2969896101MaRDI QIDQ2305412

Pablo F. Castro, Guillaume Hoffmann, Raul Fervari, Valentin Cassano, Carlos Areces

Publication date: 10 March 2020

Full work available at URL: https://doi.org/10.1007/978-3-030-29436-6_10

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20)

Uses Software

• ILTP
• MiniSat
• fCube
• DeReS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The ILTP problem library for intuitionistic logic
• Terminating tableau systems for hybrid logic with difference and converse
• Proof methods for modal and intuitionistic logics
• A logic for default reasoning
• Cumulative default logic: In defense of nonmonotonic inference rules
• Alternative approaches to default logic
• Semantics-based nonmonotonic inference
• Interpolation and Beth definability in default logics
• The many valued and nonmonotonic turn in logic
• A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System Description
• A Propositional Tableaux Based Proof Calculus for Reasoning with Default Rules
• SAT Modulo Intuitionistic Implications
• A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications
• Nonmonotonic consequence based on intuitionistic logic
• Stable inference as intuitionistic validity
• Applications of intuitionistic logic in Answer Set Programming
• A proof theoretical approach to default reasoning I: tableaux for default logic
• fCube: An Efficient Prover for Intuitionistic Propositional Logic
• Skeptical rational extensions
• Reasoning About Prescription and Description Using Prioritized Default Rules
• Intuitionistic Basis for Input/Output Logic
• Theory and Applications of Satisfiability Testing

This page was built for publication: A tableaux calculus for default intuitionistic logic