On proving the termination of algorithms by machine

DOI10.1016/0004-3702(94)90063-9MaRDI QIDQ1341666zbMATH OpenOpenAlexFDO

Authors 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

Cites work

• A closer look at termination
• A mechanical proof of the termination of Takeuchi's function
• Axiomatic approach to total correctness of programs
• scientific article; zbMATH DE number 4072437 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 46981 (Why is no real title available?)
• scientific article; zbMATH DE number 107881 (Why is no real title available?)
• scientific article; zbMATH DE number 3469999 (Why is no real title available?)
• scientific article; zbMATH DE number 3550181 (Why is no real title available?)
• scientific article; zbMATH DE number 1348458 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• scientific article; zbMATH DE number 3412171 (Why is no real title available?)
• Inductive methods for proving properties of programs
• Is “sometime” sometimes better than “always”?
• Proving termination of normalization functions for conditional expressions
• Proving termination with multiset orderings
• Rotating discs of unconventional profile
• Termination proofs for logic programs
• The addition of bounded quantification and partial functions to a computational logic and its theorem prover

Cited in

(16)

• Fermat, Euler, Wilson -- three case studies in number theory
• Proving theorems by reuse
• Dependency triples for improving termination analysis of logic programs with cut
• AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS
• Termination graphs for Java bytecode
• Proving termination by dependency pairs and inductive theorem proving
• Patching faulty conjectures
• Termination of algorithms over non-freely generated data types
• INKA: The next generation
• Walther recursion
• Termination analysis for partial functions
• Termination Analysis by Dependency Pairs and Inductive Theorem Proving
• Function definition in higher-order logic
• Reasoning about incompletely defined programs
• Verifying termination and reduction properties about higher-order logic programs
• Partial and nested recursive function definitions in higher-order logic

Describes a project that uses

Uses Software

• LISP
• NQTHM
• Find

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1341666)