Logic Programming
An important advance in 20th-century mathematical logic was achieved in 1965 when J.A. Robinson introduced the resolution calculus as a method for mechanical theorem-proving. This calculus underlies most of the work that has gone on in automated theorem-proving since. In very brief terms, we may say that a mathematical formula is a logical consequence of a set of formulae S if an only if S {¬ } is inconsistent. The achievement of the resolution method is that it mechanizes proofs of inconsistency, i.e., makes it possible to prove when a certain set of formulae is inconsistent.
Further on, in the early 1970s R. Kowalski and A. Colmerauer discovered that it was possible to give an operational interpretation to sentences of predicate logic. For this they used the resolution method of Robinson as the underlying computational model, and logic programming was born.
Logic programming is a science that exists at three different levels. When consideration is given to programming of actual computing devices, standard programming terminology such as procedures, alternatives of procedures, calls, variables, and the like are used. When consideration is given to the logical foundations of logic programming, words from mathematical logic such as variable, function, predicate symbols, terms, atomic formulae, and the like apply. Lastly, when consideration is given to the mechanization of predicate logic in automated theorem-proving procedures, terms such as literal, unification, resolution, Horn clause, and the like apply. Which of these three ways one is speaking of logic programming is usually not made explicit, but it is clear from the context to seasoned practitioners, and causes little difficulty.
Logic programming is, like functional programming, a declarative way of composing programs. In brief, declarative programming is much more concerned about what should be computed and much less with how something should be done. But it is also much more--it is very educational to understand logic programming and its virtues even if one is never going to write a logic program.
The language of logic programming is a formalism for expressing one's ideas in the form of some chosen logic (usually the predicate logic). The execution of the program consists then of proving (or disproving) that some logical consequence follows from those expressions. There are, however, different logics, different ways of proving theorems in those logics, and different ways to implement a certain mechanized form of reasoning by traditional computer. The most well-known logic programming language Prolog is based on predicate logic (or rather a restricted case thereof), a theorem proving algorithm called SLD-resolution, and an (approximative) implementation based on simple depth-first search (DFS). Later languages have added parallellism, types, modules, more declarative and flexible control mechanisms, but Prolog continues to be the best known and most commonly used in logic programming education as well as application.
The inherently declarative nature of logic programming stems from the fact that each program has a natural meaning: the only difficulty is to make sure that the meaning of the program and the meaning of the problem are the same. If one ends up with a syntactically valid logic program that has a different semantics (i.e., meaning) than the problem one intends to solve, then the running of the program is not meaningful insofar as the desired solution to the problem is concerned. Thus, an important issue in logic programming is not only to make certain that the syntax of the code is right, but also that the semantics exactly correspond to the semantics of the problem whose solution is desired.
An interesting amalgam of two major types of programming has been achieved in the form of functional logic programming, which aims to meld these important declarative programming paradigms, namely functional programming and logic programming. The interest in the amalgamation of these two paradigms has been increased since the beginning of the 1990s. In comparison with pure functional languages, functional logic languages have more expressive power due to the availability of features like function inversion, partial data structures, existential variables, and non-deterministic search. In comparison with pure logic languages, functional logic languages have a more efficient operational behavior since functions provide for more efficient evaluation strategies (lazy evaluation, deterministic reductions) than predicates. Early research in this area has been concentrated on the definition and improvement of appropriate execution principles for functional logic languages. In recent years efficient implementations of these execution principles have been developed.
This is the complete article, containing 720 words
(approx. 2 pages at 300 words per page).
