Abstract
The logic MSOL+B is defined, by extending monadic second-order logic on the infinite binary tree with a new bounding quantifier B In this logic, a formula BX.φ(X) states that there is a finite bound on the size of sets satisfying φ(X). Satisfiability is proved decidable for two fragments of MSOL+B: formulas of the form ¬BX.φ(X), with φ a B-free formula; and formulas built from B-free formulas by nesting B, V and Λ. © Springer-Verlag 2004.
Cite
CITATION STYLE
Bojańczyk, M. (2004). A bounding quantifier. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3210, 41–55. https://doi.org/10.1007/978-3-540-30124-0_7
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
