Magnitude Monadic Logic over Words and the Use of Relative Internal Set Theory

Cost monadic logic extends monadic second-order logic with the ability to measure the cardinality of sets and comes with decision procedures for boundedness related questions. We provide new decidability results allowing the systematic investigation of questions involving "relative boundedness&...

Full description

Saved in:
Bibliographic Details
Main Author: Colcombet, Thomas
Format: Conference Proceeding
Language:English
Subjects:
Automata
Context
Games
Set theory
Software and its engineering > Software notations and tools > Formal language definitions
Syntactics
Theory of computation > Formal languages and automata theory
Theory of computation > Logic
Theory of computation > Logic > Programming logic
Theory of computation > Logic > Type theory
Theory of computation > Semantics and reasoning > Program reasoning
Upper bound
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Cost monadic logic extends monadic second-order logic with the ability to measure the cardinality of sets and comes with decision procedures for boundedness related questions. We provide new decidability results allowing the systematic investigation of questions involving "relative boundedness". We first introduce a suitable logic, magnitude monadic logic. We then establish the decidability of this logic over finite words. We finally advocate that developing the proofs in the axiomatic system of "relative internal set theory", a variant of nonstandard analysis, entails a significant simplification of the proofs.
ISSN:1043-6871
2575-5528
DOI:10.1109/LICS.2013.17