Completion is an Instance of Abstract Canonical System Inference

Conference object English OPEN
Burel , Guillaume; Kirchner , Claude;
(2006)
  • Publisher: Springer Verlag
  • Related identifiers: doi: 10.1007/11780274_26
  • Subject: completion | [ INFO.INFO-LO ] Computer Science [cs]/Logic in Computer Science [cs.LO] | proof ordering | proof representation | Logic in computer science;rewriting and deduction | equational logic | rewriting and deduction
    acm: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES

http://www.springerlink.com/content/u222753gl333221p/; Abstract canonical systems and inference (ACSI) were introduced to formalize the intuitive notions of good proof and good inference appearing typically in first-order logic or in Knuth-Bendix like completion procedu... View more
  • References (43)
    43 references, page 1 of 5

    [1] M. Aiguier and D. Bahrami. Structures for abstract rewriting. Journal of Automated Reasoning, 2006. To appear.

    [2] F. Baader and T. Nipkow. Term Rewriting and all That. Cambridge University Press, 1998.

    [3] L. Bachmair. Proof methods for equational theories. PhD thesis, University of Illinois, Urbana-Champaign, (Ill., USA), 1987. Revised version, August 1988.

    [4] L. Bachmair and N. Dershowitz. Equational inference, canonical proofs, and proof orderings. Journal of Association for Computing Machinery, 41(2):236-276, 1994.

    [5] L. Bachmair and H. Ganzinger. Resolution theorem proving. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 2, pages 19-99. Elsevier Science, 2001.

    [6] M. P. Bonacina and N. Dershowitz. Abstract Canonical Inference. ACM Transactions on Computational Logic, 2006. To appear.

    [7] M. P. Bonacina and J. Hsiang. On rewrite programs: semantics and relationship with Prolog. Journal of Logic Programming, 14(1 & 2):155-180, October 1992.

    [8] P. Borovansky, C. Kirchner, H. Kirchner, and P.-E. Moreau. ELAN from a rewriting logic point of view. Theoretical Computer Science, 2(285):155-185, July 2002.

    [9] B. Buchberger. An algorithm for finding a basis for the residue class ring of a zero-dimensional polynomial ideal. PhD thesis, University of Inssbruck (Austria), 1965. (in German).

    [10] B. Buchberger. A critical-pair/completion algorithm for finitely generated ideals in rings. In E. B¨orger, G. Hasenjaeger, and D. R¨odding, editors, Proceedings of Logic and Machines: Decision problems and Complexity, volume 171 of Lecture Notes in Computer Science, pages 137-161. Springer-Verlag, 1983.

  • Metrics
    No metrics available
Share - Bookmark