Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Seventeenth Annual IEEE Symposium on

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 Symposium on Logic in Computer Science (LICS 2002)},
    year =	 {2002},
    month =	 {July}, 
    pages =      {7--16},
    location =   {Copenhagen, Denmark}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski