Logic Programming is a programming paradigm based on formal logic. A logic program is represented by formulas (axioms) – a set of sentences in logical form, expressing facts and deductions about a domain of discourse.
The idea of Logic Programming is to declare what is true (or a conclusion iteratively deducible in n finite steps from true sentences), not to to imperatively write how and when to construct this and that object in memory (control flow). Therefore Logic Programming belongs to the Declarative Languages allowing a style.
A common and most practical form of formula used in Logic Programming are Clauses.
A clause is a (logical) expression like
C1 & … & Cm <== P1 & P2 & … & Pn
Meaning that the Conclusions C1,…,Cm hold (are deducible) if each of the premises P1,…,Pn also holds.
In a very common Logic Programming language – Prolog – a simplified but most practical form of clauses is used: Horn clauses :
A Horn Clause is a simplified expression like
C1 <== P1 & P2 & … & Pn
Meaning that the conclusion C1 holds (is deducible) if each of the premises P1,…,Pn also holds.
Cx <==
Means, that Cx is true „per se“ (an axiom) and does not need to be derived (deducted).
A set of Horn Clauses builds a logical program (also called a Knowledge Base which is the same as an ontology in other formal systems, see below), which can be executed in a suitable logical execution environment (e.g. a Prolog interpreter) in such a way that the user (or another program) ask to proof a goal (a hypothetical formula) inside and against that knowledge base. Proving a goal means to find some variable values (terms) for which an iterated structured derivation out of the Axioms can be constructed. This can be seen as a special case of Theorem Proving.
One challenge in Logic Programming is to declaratively write a program (a knowledge base) in a way that the a-posteriori-work of the interpreting system be as efficient as possible. This is known as inference control. Inference is the way a Theorem Prover applies clauses (or more in the general: formulas) in order to perform deductions in order to prove some goals (asked logical sententes).
Controlling the efficiency of a Theorem Prover involves meta-inference techniques. The latter are heuristic methods, which inferences and which deduction to chose in order to proof goals.
Other Logical Programming Formalisms
RDFS and OWL are de-facto logical programming paradigms involving RDF as a basis to formulate formal sentences (formulas) using Linked-Data. In RDFS and OWL formulas are made of RDF statements (Subject Predicate Object). A set of RDF statements build therefore an RDFS ontology or an OWL ontology depending on the involved predicates. OWL is a super set of RDFS, OWL has negation and class equivalence as added value to RDFS.
From an abstract point of view, an ontology is a document (formally) describing objects and (logical) relationships among them. So also a declarative program like a Prolog program (a knowledge base) is an ontology inside the Prolog space. [The use of the word „ontology“ is though not so popular in the Logical Programming communities. They speak rather of „knowledge bases“.]
The following is an
:Person rdfs:subClassOf :HumanBeing .
:john a :Person .
:paul :tastes :pizzaMargherita .
:john :eats :pizzaNapoli .
:tastes rdfs:subPropertyOf :eats.
:eats rdfs:subPropertyOf :nourischesHimselfWith .
:eats :domain :Person .
:tastes rdfs:range :Pizza .
:nourischesHimselfWith rdfs:domain :HumanBeing .
:Pizza rdfs:subClassOf :Food.
An ontology is understood inside the „own“ formal execution (interpreting) system. In case of RDFS the interpreting system is any inference enabled RDF-store (also called graph store) like GraphDB or Stardog. As soon as the the RDFS ontology is loaded (or changed) inside a repository of the graph store, the latter starts a reasoning method with forward chaining inferring all possible (but not expressed) true RDF statements. These automatically inferred (materialized) RDF statements build the Entailment of the ontology, i.e. all possible true statements.
Note that e.g. the sentence :paul a :HumanBeing is not in the ontology but is also „true“ because it is in the entailment of the ontology.
Wrapping up
There are dozens of formal systems I do not explain here for the sake of simplicity. In this page an introduction on one backward-chaining inference system (Prolog on Horn Clauses) and one using forward-chaining inference system (RDFS) were sketched. A knowledge base (or an ontology) describes a (part of a) domain and possibly essential relationships among the component. A so called interpreting system (some time also called reasoner) work with this ontology and answers queries or proofs goals.
The advantage of using a declarative formalism like the ones presented above lies in the high self explaining nature of the used sentences, express the domain and its processes more clearly than procedural programs.
Mixed systems – cf. cliopatria or Trill allow to fuse the world of Horn Clauses with the world of RDF.