TY - BOOK ID - 2461679 TI - Termination proofs for logic programs PY - 1990 VL - vol 446 vol *80 SN - 3540528377 0387528377 3540471634 PB - Berlin : Springer-Verlag, DB - UniCat KW - AI(Artificial intelligence) KW - Artificial intelligence KW - Artificial thinking KW - Artificiële intelligentie KW - Electronic brains KW - Intellectronics KW - Intelligence [Artificial ] KW - Intelligence artificielle KW - Intelligent machines KW - Kunstmatige intelligentie KW - Logic programming KW - Logisch programmeren KW - Logische programmering KW - Machine intelligence KW - Programmation logique KW - Programmeren [Logisch ] KW - Programming [Logic ] KW - Thinking [Artificial ] KW - 681.3*D24 KW - 681.3*F31 KW - 681.3*F41 KW - 681.3*I2 KW - Computer programming KW - AI (Artificial intelligence) KW - Intelligence, Artificial KW - Thinking, Artificial KW - Bionics KW - Cognitive science KW - Digital computer simulation KW - Electronic data processing KW - Logic machines KW - Machine theory KW - Self-organizing systems KW - Simulation methods KW - Fifth generation computers KW - Neural computers KW - Program verification: assertion checkers; correctness proofs; reliability; validation (Software engineering)--See also {681.3*F31} KW - 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} KW - 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} KW - Artificial intelligence. AI KW - 681.3*I2 Artificial intelligence. AI KW - 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} KW - 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} KW - 681.3*D24 Program verification: assertion checkers; correctness proofs; reliability; validation (Software engineering)--See also {681.3*F31} KW - Cerveaux électroniques KW - Machines intelligentes KW - Pensée artificielle KW - Artificial intelligence. KW - Logic programming. KW - Computer science. KW - Software engineering. KW - Logic design. KW - Artificial Intelligence. KW - Programming Languages, Compilers, Interpreters. KW - Software Engineering. KW - Logics and Meanings of Programs. KW - Mathematical Logic and Formal Languages. KW - Design, Logic KW - Design of logic systems KW - Digital electronics KW - Electronic circuit design KW - Logic circuits KW - Switching theory KW - Computer software engineering KW - Engineering KW - Informatics KW - Science UR - https://www.unicat.be/uniCat?func=search&query=sysid:2461679 AB - 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. ER -