Automatic decidability
Proceedings - Symposium on Logic in Computer Science - Trang 7-16
Tóm tắt
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 /spl times/ lg(n)) clauses. For others it is polynomial. And for others it is simply exponential such as the theory of (extensional) arrays.
Từ khóa
#Equations #Polynomials #Mathematics #Computer science #Application software #Data structures #Logic #Automation #Inference algorithmsTài liệu tham khảo
10.1093/logcom/4.3.217
baader, 1998, Terra Rewriting and All That, 10.1017/CBO9781139172752
10.1109/LICS.2001.932480
10.1007/3-540-44802-0_36
10.1007/3-540-62950-5_59
10.1016/S0747-7171(87)80022-6
10.1145/363647.363681
bachmair, 2000, Abstract congruence closure and specializations, Proceedings of the 16th International Conference on Automated Deduction, 1831, 64, 10.1007/10721959_5
10.1145/322186.322198
nelson, 1981, Techniques for Program Verification