Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Beyond polynomials and Peano arithmetic-automation of elementary and ordinal interpretations
Zankl H., Winkler S., Middeldorp A. Journal of Symbolic Computation69 (C):129-158,2015.Type:Article
Date Reviewed: Sep 1 2015

Goodstein sequences and theorems are very popular because of their unboundedness with respect to multiple recursive functions and derivational complexity.

Showing the termination of Goodstein sequences and showing this termination automatically are both research topics that call for algebraic expertise. The authors encode Goodstein’s result as a termination problem of a finite rewrite system.

The authors use ordinal interpretations in implementing algebras to automatically show the termination of a system. They present 13 definitions, seven theorems, seven lemmas, and 20 examples in support of their method. The authors claim that their method is the first of its kind to automatically show the termination of a “system whose derivational complexity is not multiple recursive.”

For the implementation of their method, the authors combine ordinal algebras with matrix interpretations for the automatic termination proof. They further find that it manages Goodstein sequences within nine seconds, where a problem has approximately 120,000 variables and 300,000 clauses. The authors experiment on 1,463 termination tools for rewriting systems in the standard category of the termination problems database (TPDB). In the future, they propose the use of termination tools for rewrite systems with high derivational complexity.

The authors’ ideas of automating elementary interpretations for termination analysis make this paper an interesting read. They further claim that their method can automatically prove termination of two specific systems, namely, the battle of Hercules and Hydra, and the Worm battle.

Reviewer:  Lalit Saxena Review #: CR143738 (1511-0967)
Bookmark and Share
 
Grammars And Other Rewriting Systems (F.4.2 )
 
 
Deduction And Theorem Proving (I.2.3 )
 
 
Discrete Mathematics (G.2 )
 
Would you recommend this review?
yes
no
Other reviews under "Grammars And Other Rewriting Systems": Date
Automating the Knuth Bendix ordering
Dick J., Kalmus J., Martin U. Acta Informatica 28(2): 95-119, 1990. Type: Article
Apr 1 1992
Sufficient-completeness, ground-reducibility and their complexity
Kapur D. (ed), Narendran P., Rosenkrantz D., Zhang H. Acta Informatica 28(4): 311-350, 1991. Type: Article
Jun 1 1992
An introduction to Knuth-Bendix completion
Dick A. The Computer Journal 34(1): 2-15, 1991. Type: Article
Apr 1 1992
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy