On proving the termination of algorithms by machine

DOI10.1016/0004-3702(94)90063-9zbMath0938.68819OpenAlexW1987494796MaRDI QIDQ1341666

Christoph Walther

Publication date: 21 June 2000

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0004-3702(94)90063-9

Mathematics Subject Classification ID

Related Items (14)

Verifying termination and reduction properties about higher-order logic programs ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ Fermat, Euler, Wilson -- three case studies in number theory ⋮ Proving theorems by reuse ⋮ Dependency Triples for Improving Termination Analysis of Logic Programs with Cut ⋮ Patching faulty conjectures ⋮ Termination of algorithms over non-freely generated data types ⋮ INKA: The next generation ⋮ Walther recursion ⋮ AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS ⋮ Partial and nested recursive function definitions in higher-order logic ⋮ Termination Analysis by Dependency Pairs and Inductive Theorem Proving ⋮ Termination Graphs for Java Bytecode ⋮ Termination analysis for partial functions

Uses Software

• LISP
• NQTHM
• Find

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proving termination of normalization functions for conditional expressions
• The addition of bounded quantification and partial functions to a computational logic and its theorem prover
• Termination proofs for logic programs
• A closer look at termination
• A mechanical proof of the termination of Takeuchi's function
• Rotating discs of unconventional profile
• Axiomatic approach to total correctness of programs
• Proving termination with multiset orderings
• Is “sometime” sometimes better than “always”?
• Inductive methods for proving properties of programs

This page was built for publication: On proving the termination of algorithms by machine