|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
17th Annual IEEE Symposium on Logic in Computer Science (LICS'02)
Automatic Decidability
Copenhagen, Denmark
July 22-July 25
ISBN: 0-7695-1483-9
| ASCII Text | x | ||
| Christopher Lynch, Barbara Morawska, "Automatic Decidability," Logic in Computer Science, Symposium on, pp. 7, 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), 2002. | |||
| BibTex | x | ||
| @article{ 10.1109/LICS.2002.1029813, author = {Christopher Lynch and Barbara Morawska}, title = {Automatic Decidability}, journal ={Logic in Computer Science, Symposium on}, volume = {0}, year = {2002}, issn = {1043-6871}, pages = {7}, doi = {http://doi.ieeecomputersociety.org/10.1109/LICS.2002.1029813}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - Logic in Computer Science, Symposium on TI - Automatic Decidability SN - 1043-6871 SP EP A1 - Christopher Lynch, A1 - Barbara Morawska, PY - 2002 KW - null VL - 0 JA - Logic in Computer Science, Symposium on ER - | |||
We give a set of inference rules with constant constraints. Then we show how to extend a set of equational clauses, so that if the application of these inference rules halts on these clauses, then the theory is decidable by applying a standard set of Paramodulation inference rules. In addition, we can determine the number of clauses generated in this decision procedure. For some theories, such as the theory of lists, there are O(n × lg(n)) clauses. For others it is polynomial. And for others it is simply exponential such as the theory of (extensional) arrays.
Citation:
Christopher Lynch, Barbara Morawska, "Automatic Decidability," lics, pp.7, 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), 2002
Usage of this product signifies your acceptance of the Terms of Use.