Papers /

Gradel-TCS 1999

Reading

Cycling

Backpacking

X-Wing

Infinity

Warhammer 40k

Boardgames

Hobby

Food

Code



Nook

sidebar

Gradel-TCS 1999

On Logics with Two Variables

Gradel and Otto

modal logic first order description complexity expressiveness decidability

@article{gradel:tcs-1999,
  author={Erich Gr\"adel and Martin Otto},
  title={On Logics with Two Variables},
  journal={Theoretical Computer Science},
  year={1999},
  volume={224},
  pages={73--113}
}

Result from Mortimer: Two-variable fragment of first order logic (FO^2) is decidable for satisfiability, via finite model property

Many propositional model logics can be embedded into this fragment

  • Description logics, computation tree logic (CTL), etc

Extending modal logic is more robust in respect to decidability than FO^2

Being two-variable requires being verifiable by successively examining pairs of objects; it does not require a larger view of the structure

Fo^2 with counting is decidable

Most interesting extensions of FO^2 are not decidable

  • Do not have finite model property, though that is not necessary
  • It is probably because they fail the tree-model property

Addition of transitive closure renders FO^2 undecidable

Recent Changes (All) | Edit SideBar Page last modified on July 17, 2009, at 11:11 AM Edit Page | Page History
Powered by PmWiki