Abstract
We describe an abstract proof-theoretic framework based on normal-form proofs, defined using well-founded orderings on proof objects. This leads to robust notions of canonical presentation and redundancy. Fairness of deductive mechanisms – in this general framework – leads to completeness or saturation. The method has so far been applied to the equational, Horn-clause, and deduction-modulo cases.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bachmair, L., Dershowitz, N.: Equational inference, canonical proofs, and proof orderings. Journal of the ACM 41, 236–276 (1994), http://www.cs.tau.ac.il/~nachum/papers/jacm-report.pdf [viewed May 22, 2008]
Bertet, K., Nebut, M.: Efficient algorithms on the Moore family associated to an implicational system. Discrete Mathematics and Theoretical Computer Science 6, 315–338 (2004)
Bonacina, M.P., Dershowitz, N.: Abstract canonical inference. ACM Transactions on Computational Logic 8, 180–208 (2007), http://tocl.acm.org/accepted/240bonacina.pdf [viewed May 22, 2008]
Bonacina, M.P., Dershowitz, N.: Canonical ground Horn theories. Research Report 49/2007, Dipartimento di Informatica, Università degli Studi di Verona (2007), http://profs.sci.univr.it/~bonacina/papers/TR2007HornCanonicity.pdf [viewed May 22, 2008]
Bonacina, M.P., Dershowitz, N.: Canonical inference for implicational systems. In: Proc. of the Fourth International Joint Conference on Automated Reasoning (IJCAR). LNCS (LNAI), vol. 5195, pp. 380–397. Springer, Heidelberg (2008), http://www.cs.tau.ac.il/~nachum/papers/CanonicalImplicational.pdf
Bonacina, M.P., Hsiang, J.: Towards a foundation of completion procedures as semidecision procedures. Theoretical Computer Science 146, 199–242 (1995)
Buchberger, B.: Ein Algorithmus zum auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. PhD thesis, Univ. Innsbruck, Austria (1965)
Burel, G.: Systèmes canoniques abstraits: Application à la déduction naturelle et à la complétion. Master’s thesis, Université Denis Diderot – Paris 7 (2005), http://www.loria.fr/~burel/download/Burel_Master.pdf [viewed May 22, 2008]
Burel, G., Kirchner, C.: Completion is an instance of abstract canonical system inference. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol. 4060, pp. 497–520. Springer, Heidelberg (2006), http://www.loria.fr/~burel/download/bk4jag.pdf [viewed May 22, 2008]
Burel, G., Kirchner, C.: Cut elimination in deduction modulo by abstract completion. In: Artemov, S., Nerode, A. (eds.) Proc. of the Symposium on Logical Foundations of Computer Science (LFCS). LNCS, pp. 115–131. Springer, Heidelberg (2007)
Burel, G., Kirchner, C.: Regaining cut admissibility in deduction modulo using abstract completion (submitted) [viewed May 22, 2008], http://www.loria.fr/~burel/download/gencomp_ic.pdf
Butler, G., Lankford, D.S.: Experiments with computer implementations of procedures which often derive decision algorithms for the word problem in abstract algebras. Memo MTP-7, Department of Mathematics, Louisiana Tech. University, Ruston, LA (1980)
Dershowitz, N.: Canonicity. In: Proc. of the Fourth International Workshop on First-Order Theorem Proving (FTP 2003). Electronic Notes in Theoretical Computer Science, vol. 86, pp. 120–132 (2003), http://www.cs.tau.ac.il/~nachum/papers/canonicity.pdf [viewed May 22, 2008]
Dershowitz, N., Kirchner, C.: Abstract saturation-based inference. In: Proc. of the Eighteenth IEEE Symposium on Logic in Computer Science, June 2003, pp. 65–74. IEEE Press, Los Alamitos (2003), http://www.cs.tau.ac.il/~nachum/papers/lics2003-final.pdf [viewed May 22, 2008]
Dershowitz, N., Kirchner, C.: Abstract canonical presentations. Theoretical Computer Science 357, 53–69 (2006), http://www.cs.tau.ac.il/nachum/papers/AbstractCanonicalPresentations.pdf [viewed May 22, 2008]
Gallier, J., Narendran, P., Plaisted, D., Raatz, S., Snyder, W.: An algorithm for finding canonical sets of ground rewrite rules in polynomial time. J. of the Association of Computing Machinery 40, 1–16 (1993)
Huet, G.: A complete proof of correctness of the Knuth–Bendix completion algorithm. Journal of Computer and System Sciences 23, 11–21 (1981)
Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, Oxford (1970)
Lankford, D.S.: Canonical inference. Memo ATP-32, Automatic Theorem Proving Project, University of Texas, Austin, TX (1975)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dershowitz, N. (2008). Canonicity!. In: Armando, A., Baumgartner, P., Dowek, G. (eds) Automated Reasoning. IJCAR 2008. Lecture Notes in Computer Science(), vol 5195. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71070-7_29
Download citation
DOI: https://doi.org/10.1007/978-3-540-71070-7_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71069-1
Online ISBN: 978-3-540-71070-7
eBook Packages: Computer ScienceComputer Science (R0)