We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Sahlqvist-Type Completeness Theory for Hybrid Logic with Binder

Authors: Zhiguang Zhao
Abstract: In the present paper, we continue the research in \cite{Zh21c} to develop the Sahlqvist-type completeness theory for hybrid logic with satisfaction operators and downarrow binders $\mathcal{L}(@, \downarrow)$. We define the class of skeletal Sahlqvist formulas for $\mathcal{L}(@, \downarrow)$ following the ideas in \cite{ConRob}, but we follow a different proof strategy which is purely proof-theoretic, namely showing that for every skeletal Sahlqvist formula $\phi$ and its hybrid pure correspondence $\pi$, $\mathbf{K}_{\mathcal{H}(@, \downarrow)}+\phi$ proves $\pi$, therefore $\mathbf{K}_{\mathcal{H}(@, \downarrow)}+\phi$ is complete with respect to the class of frames defined by $\pi$, using a restricted version of the algorithm $\mathsf{ALBA}^{\downarrow}$ defined in \cite{Zh21c}.
Comments: arXiv admin note: text overlap with arXiv:2102.13291
Subjects: Logic in Computer Science (cs.LO); Logic (math.LO)
Cite as: arXiv:2207.01288 [cs.LO]
  (or arXiv:2207.01288v1 [cs.LO] for this version)

Submission history

From: Zhiguang Zhao [view email]
[v1] Mon, 4 Jul 2022 09:36:52 GMT (23kb)

Link back to: arXiv, form interface, contact.