Top

Published in:

2018 | OriginalPaper | Chapter

Well-Founded Unions

Authors : Jeremy Dawson, Nachum Dershowitz, Rajeev Goré

Published in: Automated Reasoning

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Given two or more well-founded (terminating) binary relations, when can one be sure that their union is likewise well-founded? We suggest new conditions for an arbitrary number of relations, generalising known conditions for two relations. We also provide counterexamples to several potential weakenings. All proofs have been machine checked.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter The Higher-Order Prover Leo-III

next chapter Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories

We choose to view the forward direction as descent.

After 2005, it became too onerous to keep pace with changes in Isabelle. This does not detract from our verification in any way since Isabelle 2005 is a trusted system. Instructions on running the proofs are at http://users.cecs.anu.edu.au/~jeremy/isabelle/2005/gen/tripartite-README.

Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236, 133–178 (2000). Preliminary version. http://verify.rwth-aachen.de/giesl/papers/ibn-97-46.ps

Bachmair, L., Dershowitz, N.: Commutation, transformation, and termination. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 5–20. Springer, Heidelberg (1986). https://doi.org/10.1007/3-540-16780-3_76CrossRef

Bruynooghe, M., Codish, M., Gallagher, J.P., Genaim, S., Vanhoof, W.: Termination analysis of logic programs through combination of type-based norms. ACM Trans. Program. Lang. Syst. 29, 10 (2007)CrossRef

Dawson, J., Goré, R.: Proving results from the paper Nachum Dershowitz: tripartite unions. Technical report, Australian National University (2016). http://users.cecs.anu.edu.au/~rpg/tripartite-unions.pdf

Dershowitz, N.: Termination of linear rewriting systems. In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol. 115, pp. 448–458. Springer, Heidelberg (1981). https://doi.org/10.1007/3-540-10843-2_36CrossRef

Dershowitz, N.: Hierarchical termination. In: Dershowitz, N., Lindenstrauss, N. (eds.) CTRS 1994. LNCS, vol. 968, pp. 89–105. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60381-6_6CrossRef

Dershowitz, N.: Jumping and escaping: modular termination and the abstract path ordering. Theor. Comput. Sci. 464, 35–47 (2012). http://nachum.org/papers/Toyama.pdfMathSciNetCrossRef

Dershowitz, N.: Tripartite unions. arXiv:1606.01148 [cs.LO], informal (2016)

Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: Handbook of Theoretical Computer Science, Formal Methods and Semantics, vol. B, pp. 243–320. North-Holland, Amsterdam (1990). http://nachum.org/papers/survey-draft.pdf

10.

Dershowitz, N., Lindenstrauss, N., Sagiv, Y., Serebrenik, A.: A general framework for automatic termination analysis of logic programs. Appl. Algebra Eng. Commun. Comput. 12, 117–156 (2001). http://nachum.org/papers/aaecc.pdfMathSciNetCrossRef

11.

Doornbos, H., Backhouse, R., van der Woude, J.: A calculational approach to mathematical induction. Theor. Comput. Sci. 179, 103–135 (1997). http://www.cs.nott.ac.uk/~rcb/MPC/MadeCalculational.ps.gzMathSciNetCrossRef

12.

Doornbos, H., von Karger, B.: On the union of well-founded relations. Logic J. IGPL 6, 195–201 (1998)MathSciNetCrossRef

13.

Geser, A.: Relative termination. Ph.D. thesis, Fakultät für Mathematik und Informatik, Universität Passau, Germany (1990). http://homepage.cs.uiowa.edu/~astump/papers/geser_dissertation.pdf

14.

Giesl, J., Kapur, D.: Dependency pairs for equational rewriting. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 93–107. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45127-7_9CrossRefMATH

15.

Klop, J.W.: Combinatory Reduction Systems. CWI Math. Centre Tract. 127 (1980)

16.

Lescanne, P.: Rewriting list contributions (1989). http://www.ens-lyon.fr/LIP/REWRITING/CONTRIBUTIONS

17.

Plaisted, D.A.: Polynomial time termination and constraint satisfaction tests. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol. 690, pp. 405–420. Springer, Heidelberg (1993). https://doi.org/10.1007/978-3-662-21551-7_30CrossRef

18.

Takeuti, G.: Ordinal diagrams. II. J. Math. Soc. Jpn. 12, 385–391 (1960)MathSciNetCrossRef

Title: Well-Founded Unions
Authors: Jeremy Dawson
Nachum Dershowitz
Rajeev Goré
Publisher: Springer International Publishing
Book: Automated Reasoning
Print ISBN: 978-3-319-94204-9

Electronic ISBN: 978-3-319-94205-6

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-319-94205-6_9

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner