SAT vs. SMV for automatic validation of tabular property of superintuitionistic logics

zbMATH Open1249.03005MaRDI QIDQ2880609FDOQ2880609

Authors: P. A. Shrajner, Nikolay V. Shilov, S. O. Grebeneva 

Publication date: 13 April 2012

Published in: Joint Bulletin of the Novosibirsk Computing Center (NCC) and A. P. Ershov Institute of Informatics Systems (IIS). Series: Computer Science (Search for Journal in Brave)

Recommendations

• SAT vs. Translation Based decision procedures for modal logics: a comparative evaluation
• scientific article; zbMATH DE number 1538057
• Automatic recognition of the interpolation property in some superintuitionistic propositional logics
• Publication:4863689
• A tableau-based decision procedure for CTL\(^*\)

zbMATH Keywords

Kripke semanticsBoolean satisfiabilitysuperintuitionistic logicsymbolic model checkingKripke frametabularity propertypropositional variable

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Intermediate logics (03B55) Logic in computer science (03B70)

This page was built for publication: SAT vs. SMV for automatic validation of tabular property of superintuitionistic logics

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