Automated Synthesis of Tableau Calculi

DOI10.2168/LMCS-7(2:6)2011zbMath1218.03012OpenAlexW2569781727MaRDI QIDQ5892517

Renate A. Schmidt, Dmitry Tishkovsky

Publication date: 26 May 2011

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2168/lmcs-7(2:6)2011

zbMATH Keywords

modal logiccompletenessfirst-order logicautomated reasoningdecidabilityintuitionistic propositional logicdescription logicsoundnesstableau calculidecision procedurecalculus synthesis

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

A bi-intuitionistic modal logic: foundations and automation ⋮ Modal Tableau Systems with Blocking and Congruence Closure ⋮ Intuitionistic Decision Procedures Since Gentzen ⋮ Using tableau to decide description logics with full role negation and identity ⋮ Blocking and other enhancements for bottom-up model generation methods ⋮ Tableau-based decision procedure for non-Fregean logic of sentential identity ⋮ SAT-based proof search in intermediate propositional logics

Uses Software

• LoTREC
• KL-ONE