- Referenced in 39 articles
- order equivalents and proving canonicity of modal formulae, and thus established a very general correspondence ... most important of which employs a modal version of a result by Ackermann that enables ... existentially quantified predicate variable in a formula, provided a certain negative polarity condition on that ... correctness for a large class of modal formulae containing an extension of the Sahlqvist formulae...
- Referenced in 27 articles
- counter-models and testing satisfiability of formulas in modal and description logics. This system...
- Referenced in 14 articles
- Logic Satisfiability Solver, decides satisfiability of modal formulas in a generic and compositional ... polynomial space algorithm to decide satisfiability for modal logics that are amenable to coalgebric semantics...
- Referenced in 41 articles
- case of quantified modal logics as long as the Barcan formula is not assumed...
- Referenced in 4 articles
- decides the satisfiability of modal (and, more generally, hybrid) formulas with respect ... logical framework covering a wide range of modal logics, beyond relational semantics. The core...
- Referenced in 1 article
- using either regular expressions or modal $\mu $-calculus formulas, and verified efficiently on very large...
- Referenced in 12 articles
- preorders; define propositions in a powerful modal logic and check whether a given process satisfies ... process does or does not satisfy a formula; derive automatically logical formulae which distinguish nonequivalent...
- Referenced in 6 articles
- logic with binders, the converse and global modalities, transitivity assertions and relation hierarchies ... that the negation normal form of the formulae given in input do not contain...
- Referenced in 8 articles
- modal S4 are decidable. This theorem was shown in  to be equivalent ... details of which see ). Given any formula A (in the appropriate vocabulary) the decision...
- Referenced in 1 article
- modal operators or certain modelling problems like one-to-one sentence–formula mapping. The CTRL/iCTRL...
- Referenced in 5 articles
- addressing openendedness of SOC. Indeed, SoSL provides modal operators that can be used for specifying ... have developed ways for model-checking SoSL formulae against MarCaSPiS specifications by exploiting an existing...
- Referenced in 1890 articles
- Coq is a formal proof management system. It...
- Referenced in 3189 articles
- GAP is a system for computational discrete algebra...
- Referenced in 767 articles
- Gmsh is a 3D finite element grid generator...
- Referenced in 713 articles
- Isabelle is a generic proof assistant. It allows...
- Referenced in 306 articles
- LANCELOT. A Fortran package for large-scale nonlinear...
- Referenced in 1702 articles
- LAPACK is written in Fortran 90 and provides...
- Referenced in 51 articles
- LEO-II is a standalone, resolution-based higher...
- Referenced in 394 articles
- Algorithm 583: LSQR: Sparse Linear Equations and Least...
- Referenced in 5373 articles
- The result of over 30 years of cutting...