Catalogue of Artificial Intelligence Techniques

   

Jump to: Top | Entry | References | Comments

View Maths as: Images | MathML

Logic Programming

Keywords: Horn clauses

Categories: Logic Programming , Programming Languages


Author(s): Paul Brna

The core idea of logic programming is that it is possible to provide a procedural semantics for statements in certain (usually classical) logical formalisms. In theory, programming is then reduced to providing a program specification that is represented as a set of axioms. This is handed over to a sound and complete Theorem Prover. The theorem prover constructs a proof that there is a solution. If there is a solution then further useful information can usually be extracted from the proof. The main justification for such an approach is that classical logic is well understood and that, as a consequence, it is possible to provide systems which have a rigorous, theoretical foundation. In order for such systems to be useful it is necessary that the formalism is sufficiently powerful and desirable that it is also sufficiently expressive. The best-known example of an attempt to realise such a system is Prolog which is based on a Resolution theorem prover. Programs are written in the Horn clause form of first-order Predicate Logic. There is an extensive literature on the properties of Prolog (and some of its variations) vis-a-vis soundness and completeness. Note that the ideal has not been attained in practice as (i) the fixed control strategy built into most Prolog interpreters does not always find all solutions, (ii) some explicit control (procedural element) is usually required, and (iii) programs often require side effects which undermine the declarative semantics. There are also some difficulties in connection with extending the expressiveness of Prolog, in particular, the problems of Negation and equality. The term `logic programming' is often taken to be synonymous with `Prolog'. This is not correct, however, as the field of logic programming also includes the so-called committed choice languages. These languages use a Prolog-like formalism but are designed for various forms of parallel execution. Examples include PARLOG, GHC and CP. Such languages lack a clear declarative semantics. Other systems have been built which explore various extensions, alternative control regimes or methods for automating proof search other than resolution.


References:


Comments:

Add Comment

No comments.