Paramodulation with Non-Monotonic Orderings and Simplification
Tóm tắt
Ordered paramodulation and Knuth-Bendix completion are known to remain complete when using non-monotonic orderings. However, these results do not imply the compatibility of the calculus with essential redundancy elimination techniques such as demodulation, i.e., simplification by rewriting, which constitute the primary mode of computation in most successful automated theorem provers. In this paper we present a complete ordered paramodulation calculus for non-monotonic orderings which is compatible with powerful redundancy notions including demodulation, hence strictly improving the previous results and making the calculus more likely to be used in practice. As a side effect, we obtain a Knuth-Bendix completion procedure compatible with simplification techniques, which can be used for finding, whenever it exists, a convergent term rewrite system for a given set of equations and a (possibly non-totalizable) reduction ordering.
Tài liệu tham khảo
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comp. Sci. 236, 133–178 (2000)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York, NY, USA (1998)
Bachmair, L., Dershowitz, N.: Equational inference, canonical proofs, and proof orderings. J. ACM 41(2), 236–276 (1994)
Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217–247 (1994)
Bachmair, L., Ganzinger, H.: Equational reasoning in saturation-based theorem proving. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction—A Basis for Applications, vol. I, chap 11, pp. 353–397. Kluwer, Dordrecht, The Netherlands (1998)
Bachmair, L., Dershowitz, N., Hsiang, J.: Orderings for equational proofs. In: First IEEE Symposium on Logic in Computer Science (LICS), IEEE Computer Society Press, pp. 346–357. Los Alamitos, CA, USA, Cambridge, MA, USA (1986)
Bachmair, L., Dershowitz, N., Plaisted, D.: Completion without failure. In: Aït-Kaci, H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures, vol. 2: Rewriting Techniques, chap 1, pp 1–30. Academic Press, New York (1989)
Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation. Inf. Comput. 121(2), 172–192 (1995)
Bofill, M., Rubio, A.: Well-foundedness is sufficient for completeness of ordered paramodulation. In: 18th International Conference on Automated Deduction (CADE), vol. 2392, pp. 456–470. Springer, Berlin Heidelberg, Germany, Copenhagen, Denmark, LNAI (2002)
Bofill, M., Rubio, A.: Redundancy notions for paramodulation with non-monotonic orderings. In: 2nd International Joint Conference on Automated Reasoning (IJCAR), vol. 3097, pp. 107–121. Springer-Verlag, Berlin Heidelberg, Germany, Cork, Ireland, LNAI (2004)
Bofill, M., Rubio, A.: Paramodulation with well-founded orderings. J. Log. Comput. 19(2), 263–302 (2009)
Bofill, M., Godoy, G., Nieuwenhuis, R., Rubio, A.: Paramodulation with non-monotonic orderings. In: 14th IEEE Symposium on Logic in Computer Science (LICS), pp. 225–233. IEEE Computer Society Press, Los Alamitos, CA, USA, Trento, Italy (1999)
Bofill, M., Godoy, G., Nieuwenhuis, R., Rubio, A.: Paramodulation and Knuth-Bendix completion with non-total and non-monotonic orderings. J. Autom. Reason. 30(1), 99–120 (2003)
Borralleras, C., Ferreira, M., Rubio, A.: Complete monotonic semantic path orderings. In: McAllester, D. (ed.) Proceedings of the 17th International Conference on Automated Deduction (CADE-17), vol. 1831, pp. 346–364. Springer, Pittsburgh, USA, LNAI (2000)
Dershowitz, N.: Orderings for term-rewriting systems. Theor. Comp. Sci. 17(3), 279–301 (1982)
Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, chap. 6, pp. 244–320. Elsevier Science B.V, Amsterdan, The Netherlands and The MIT Press, Cambridge, MA, USA (1990)
Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Commun. ACM 22(8), 465–476 (1979)
Devie, H.: Linear completion. In: Kaplan, S., Okada, M. (eds.) Conditional and Typed Rewriting Systems, 2nd International Workshop, Springer, Montreal, Canada, LNCS 516, pp. 233–245 (1990)
Hsiang, J., Rusinowitch, M.: Proving refutational completeness of theorem proving strategies: the transfinite semantic tree method. J. Artists’ Choice Mus. 38(3), 559–587 (1991)
Kamin, S., Levy, J.J.: Two generalizations of the recursive path ordering. Unpublished note, Dept. of Computer Science, Univ. of Illinois, Urbana, IL (1980)
Kusakari, K., Nakamura, M., Toyama, Y.: Argument filtering transformation. In: Proceedings of the International Conference on Principles and Practice of Declarative Programming (PPDP’99), 1702, pp. 47–61. Springer, LNCS (1999)
Nieuwenhuis, R., Rubio, A.: Theorem proving with ordering and equality constrained clauses. J. Symb. Comput. 19(4), 321–351 (1995)
Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, J., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, chap. 7, pp. 372–444. Elsevier Science B.V, Amsterdan, The Netherlands and The MIT Press, Cambridge, MA, USA (2001)
Wechler, W.: Universal Algebra for Computer Scientists, EATCS Monographs on Theoretical Computer Science, vol. 25. Springer, New York (1992)
Wehrman, I., Stump, A., Westbrook, E.M.: Slothrop: Knuth-Bendix completion with a modern termination checker. In: Pfenning, F. (ed.) RTA, vol. 4098, pp. 287–296. Springer, Lecture Notes in Computer Science (2006)
Winkler, S., Middeldorp, A.: Termination tools in ordered completion. In: Proceedings of the 5th International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence, vol. 6173, pp. 518–532. Springer-Verlag (2010)