BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/195
DTSTAMP:20230914T125914Z
SUMMARY:Counting\, Quantifiers and Algorithms
DESCRIPTION:Speaker: Kamal Lodaya\nInstitute of Mathematical Sciences\nIV C
 ross Road\nCIT Campus\nTaramani\nChennai 600 113\nht\n\nAbstract: \nLogic 
 (first order or temporal) can be easily extended to describe  counts\, par
 ity and other numerical phenomena. The satisfiability  problem of the exte
 nded logic is easily seen to be undecidable\, even  on models which are fi
 nite words. We examine situations in which the  satisfiability problem on 
 such models remains decidable (joint  work with A V Sreejith).\n\nTemporal
  logic with modulo counting is Pspace-complete (the lower  bound holds wit
 hout modulo counting\, by Sistla and Clarke).  Two-variable first order lo
 gic with modulo counting quantifiers is  Expspace-complete (the upper boun
 d is by an exponential translation to  temporal logic\, following Etessami
 \, Vardi and Wilke). If positions can  be checked for modulo congruence\, 
 but parity is kept out of the  picture\, temporal logic is complete for th
 e third level of the  polynomial hierarchy Sigma3P\, while two-variable fi
 rst order logic is  Nexptime-complete (the lower bound holds without the c
 ongruence  checking\, by Weis and Immerman). Finally\, in the special case
  of a  one-letter alphabet\, full first order logic with any number of  va
 riables\, counting quantifiers and addition built-in is decidable (by  Sch
 weikardt)  in the case of modulo counting quantifiers we give a  double ex
 ponential space upper bound. Without the modulo counting  quantifiers this
  is called Presburger arithmetic and is known to be  complete for alternat
 ing doubly exponential time with a linear number  of alternations\, shown 
 by Berman. So a small gap remains.\n\nThe talk will concentrate on the alg
 orithms rather than on details of  complexity classes.\n
URL:https://www.tcs.tifr.res.in/web/events/195
DTSTART;VALUE=DATE:20110526
LOCATION:A-212 (STCS Seminar Room)
END:VEVENT
END:VCALENDAR