Automatic Decidability

Christopher Lynch and Barbara Morawska

To appear at Symposium on Logic in Computer Science (LICS'2002), Copenhagen, Denmark, July 22nd - 25th, 2002


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).

Server START Conference Manager
Update Time 15 Mar 2002 at 15:30:31
Start Conference Manager
Conference Systems