Nominal substitution at work with the global and converse modalities

MaRDI QIDQ2904047zbMATH OpenFDO

Authors Serenella Cerrito, Marta Cialdea Mayer

Publication date 5 August 2012

zbMATH Keywords

automated deductionmodal logichybrid logictableaux calculussubstitution rule

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 2048509
• scientific article; zbMATH DE number 1867302
• On the multi-dimensional modal logic of substitutions
• scientific article; zbMATH DE number 868094
• A Modal Logic for Quantification and Substitution
• A Dynamic Semantics of Modal Subordination
• Modal translations in substructural logics
• scientific article; zbMATH DE number 823607
• Modal translation of substructural logics
• Associative substitutional semantics and quantified modal logic

Cited in

(6)

• Blocking and other enhancements for bottom-up model generation methods
• A Tableaux Based Decision Procedure for a Broad Class of Hybrid Formulae with Binders
• Nominal syntax with atom substitutions
• A tableau based decision procedure for an expressive fragment of hybrid logic with binders, converse and global modalities
• A prover dealing with nominals, binders, transitivity and relation hierarchies
• ExpTime tableaux with global caching for hybrid PDL

This page was built for publication: Nominal substitution at work with the global and converse modalities

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