DocumentCode
2194820
Title
Automatic decidability
Author
Lynch, Christopher ; Morawska, Barbara
Author_Institution
Dept. of Math. & Comput. Sci., Clarkson Univ., Potsdam, NY, USA
fYear
2002
fDate
2002
Firstpage
7
Lastpage
16
Abstract
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 0(n × lg(n)) clauses. For others it is polynomial. And for others it is simply exponential such as the theory of (extensional) arrays.
Keywords
decidability; inference mechanisms; Faramodulation inference rules; constant constraints; decidability; equational clauses; first order logic; inference rules; Application software; Automation; Computer science; Data structures; Equations; Inference algorithms; Logic; Mathematics; Polynomials;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 2002. Proceedings. 17th Annual IEEE Symposium on
ISSN
1043-6871
Print_ISBN
0-7695-1483-9
Type
conf
DOI
10.1109/LICS.2002.1029813
Filename
1029813
Link To Document