Logic in Computer Science (LICS 2002)

Paper: Automatic Decidability (at LICS 2002)

Authors: Christopher Lynch Barbara Morawska

Abstract

We give a saturation procedure that takes a theory as input, and returns a decision procedure for that theory when it halts. In addition, it returns a bound on the complexity of that theory: O(n lg(n)) for some theories (such as the theory of lists), polynomial for other theories (including all equational theories that halt), and simply exponential for other theories (such as the theory of arrays).

BibTeX

  @InProceedings{LynchMorawska-AutomaticDecidabili,
    author = 	 {Christopher Lynch and Barbara Morawska},
    title = 	 {Automatic Decidability},
    booktitle =  {Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2002},
    year =	 2002,
    editor =	 {Gordon Plotkin},
    month =	 {July}, 
    location =   {Copenhagen, Denmark}, 
    publisher =	 {IEEE Computer Society Press}
  }