Modal Logic and the two-variable fragment

Carsten LutzCarsten Lutz, Ulrike SattlerUlrike Sattler, Frank WolterFrank Wolter

Datei:LutzSattlerWolter-LTCS-01-04.ps.gz

Download

Carsten Lutz, Ulrike Sattler, Frank Wolter
Modal Logic and the two-variable fragment
Technical Report, LuFG Theoretical Computer Science, RWTH Aachen, volume LTCS-01-04, 2001. LTCS-Report

Details
Bibtex

KurzfassungAbstract
We introduce a modal language L which is obtained from standard modal logic by adding the difference operator and modal operators interpreted by boolean combinations and the converse of accessibility relations. It is proved that L has the same expressive power as the two-variable fragment FO^2 of first-order logic but speaks less succinctly about relational structures: if the number of relations is bounded, then L-satisfiability is ExpTime-complete but FO^2 satisfiability is NExpTime-complete. We indicate that the relation between L and FO^2 provides a general framework for comparing modal and temporal languages with first-order languages.
Bemerkung: Note: See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@techreport{ LutzSattlerWolter-LTCS-01-04,
  address = {Germany},
  author = {C. {Lutz} and U. {Sattler} and F. {Wolter}},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {LTCS-01-04},
  title = {Modal Logic and the two-variable fragment},
  type = {LTCS-Report},
  year = {2001},
}