7 found
Order:
  1.  17
    Algorithmic Correspondence and Canonicity for Non-Distributive Logics.Willem Conradie & Alessandra Palmigiano - 2019 - Annals of Pure and Applied Logic 170 (9):923-974.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  2.  20
    Algorithmic Correspondence and Canonicity for Distributive Modal Logic.Willem Conradie & Alessandra Palmigiano - 2012 - Annals of Pure and Applied Logic 163 (3):338-376.
  3.  77
    Algorithmic Correspondence and Completeness in Modal Logic. V. Recursive Extensions of SQEMA.Willem Conradie, Valentin Goranko & Dimitar Vakarelov - 2010 - Journal of Applied Logic 8 (4):319-333.
    The previously introduced algorithm \sqema\ computes first-order frame equivalents for modal formulae and also proves their canonicity. Here we extend \sqema\ with an additional rule based on a recursive version of Ackermann's lemma, which enables the algorithm to compute local frame equivalents of modal formulae in the extension of first-order logic with monadic least fixed-points \mffo. This computation operates by transforming input formulae into locally frame equivalent ones in the pure fragment of the hybrid mu-calculus. In particular, we prove that (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  4.  62
    Algorithmic Correspondence and Completeness in Modal Logic. IV. Semantic Extensions of SQEMA.Willem Conradie & Valentin Goranko - 2008 - Journal of Applied Non-Classical Logics 18 (2-3):175-211.
    In a previous work we introduced the algorithm \SQEMA\ for computing first-order equivalents and proving canonicity of modal formulae, and thus established a very general correspondence and canonical completeness result. \SQEMA\ is based on transformation rules, the most important of which employs a modal version of a result by Ackermann that enables elimination of an existentially quantified predicate variable in a formula, provided a certain negative polarity condition on that variable is satisfied. In this paper we develop several extensions of (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  5.  24
    On the Strength and Scope of DLS.Willem Conradie - 2006 - Journal of Applied Non-Classical Logics 16 (3-4):279-296.
    We provide syntactic necessary and sufficient conditions on the formulae reducible by the second-order quantifier elimination algorithm DLS. It is shown that DLS is compete for all modal Sahlqvist and Inductive formulae, and that all modal formulae in a single propositional variable on which DLS succeeds are canonical.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  6. Algorithmic Correspondence for Relevance Logics I. The Algorithm PEARL\documentclass[12pt]{Minimal} \usepackage{Amsmath} \usepackage{Wasysym} \usepackage{Amsfonts} \usepackage{Amssymb} \usepackage{Amsbsy} \usepackage{Mathrsfs} \usepackage{Upgreek} \setlength{\oddsidemargin}{-69pt} \begin{Document}$$\mathsf {PEARL}$$\end{Document}. [REVIEW]Willem Conradie & Valentin Goranko - 2022 - In Ivo Düntsch & Edwin Mares (eds.), Alasdair Urquhart on Nonclassical and Algebraic Logic and Complexity of Proofs. Springer Verlag. pp. 163-211.
    We apply and extend the theory and methods of algorithmic correspondence theory for modal logics, developed over the past 20 years, to the language LR\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathcal {L}_R$$\end{document} of relevance logics with respect to their standard Routley–Meyer relational semantics. We develop the non-deterministic algorithmic procedure PEARL\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {PEARL}$$\end{document} for computing first-order equivalents of formulae of the language LR\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  7.  11
    Analogues of Bull’s Theorem for Hybrid Logic.Willem Conradie & Claudette Robinson - 2019 - Logic Journal of the IGPL 27 (3):281-313.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark