Abstract | Keywords | Export | Availability | Bookmark

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

Termination proofs constitute a crucial part of program verification. Much research about termination has been done in the context of term rewriting systems. But until now there was little hope that termination proofs for nontrivial programs could be achieved automatically. This book gives a comprehensive discussion of the termination problem in the context of logic programming. Although logic programs pose special difficulties for termination proofs it turns out that automation of this task is obtainable to a much larger degree than for programs in imperative languages. A technique for the automatic derivation of termination proofs is presented in detail. The discussion of several nontrivial examples illustrates its range of applicability. The approach is based on the concept of declarative semantics, and thus makes use of an important feature of logic programming.

AI(Artificial intelligence) --- Artificial intelligence --- Artificial thinking --- Artificiële intelligentie --- Electronic brains --- Intellectronics --- Intelligence [Artificial ] --- Intelligence artificielle --- Intelligent machines --- Kunstmatige intelligentie --- Logic programming --- Logisch programmeren --- Logische programmering --- Machine intelligence --- Programmation logique --- Programmeren [Logisch ] --- Programming [Logic ] --- Thinking [Artificial ] --- 681.3*D24 --- 681.3*F31 --- 681.3*F41 --- 681.3*I2 --- Computer programming --- AI (Artificial intelligence) --- Intelligence, Artificial --- Thinking, Artificial --- Bionics --- Cognitive science --- Digital computer simulation --- Electronic data processing --- Logic machines --- Machine theory --- Self-organizing systems --- Simulation methods --- Fifth generation computers --- Neural computers --- Program verification: assertion checkers; correctness proofs; reliability; validation (Software engineering)--See also {681.3*F31} --- Specifying anf verifying and reasoning about programs: assertions; invariants; mechanical verification; pre- and post-conditions (Logics and meanings of programs)--See also {681.3*D21}; {681.3*D24}; {681.3*D31}; {681.3*E1} --- Mathematical logic: computability theory; computational logic; lambda calculus; logic programming; mechanical theorem proving; model theory; proof theory;recursive function theory--See also {681.3*F11}; {681.3*I22}; {681.3*I23} --- Artificial intelligence. AI --- 681.3*I2 Artificial intelligence. AI --- 681.3*F41 Mathematical logic: computability theory; computational logic; lambda calculus; logic programming; mechanical theorem proving; model theory; proof theory;recursive function theory--See also {681.3*F11}; {681.3*I22}; {681.3*I23} --- 681.3*F31 Specifying anf verifying and reasoning about programs: assertions; invariants; mechanical verification; pre- and post-conditions (Logics and meanings of programs)--See also {681.3*D21}; {681.3*D24}; {681.3*D31}; {681.3*E1} --- 681.3*D24 Program verification: assertion checkers; correctness proofs; reliability; validation (Software engineering)--See also {681.3*F31} --- Cerveaux électroniques --- Machines intelligentes --- Pensée artificielle --- Artificial intelligence. --- Logic programming. --- Computer science. --- Software engineering. --- Logic design. --- Artificial Intelligence. --- Programming Languages, Compilers, Interpreters. --- Software Engineering. --- Logics and Meanings of Programs. --- Mathematical Logic and Formal Languages. --- Design, Logic --- Design of logic systems --- Digital electronics --- Electronic circuit design --- Logic circuits --- Switching theory --- Computer software engineering --- Engineering --- Informatics --- Science