Logic Programming

  • Mordechai Ben-Ari


Most axioms are expressed in the form: If premise-1 and premise-2 and …then conclusion. Formally, this is:
$$A = \forall {x_1} \cdots \forall {x_k}({B_1} \wedge \cdots \wedge {B_m} \to B),$$
where B and Bi are atoms. In the degenerate case where there are no antecedents, \( A = \forall {x_1} \cdots \forall {x_k}B.\) In clausal form, an axiom is \( \neg {B_1} \vee \cdots \vee \neg {B_m} \vee B.\) To prove that a formula \( G = {G_1} \wedge \cdots \wedge {G_1}\) is a logical consequence of a set of axioms, we append \(\neg G\) to the set of axioms and try to construct a refutation by resolution. \(\neg G\) is called the goal clause.


Logic Program Logic Programming Horn Clause Computation Rule Constraint Logic Programming 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag London 2001

Authors and Affiliations

  • Mordechai Ben-Ari
    • 1
  1. 1.Department of Science TeachingWeizmann Institute of ScienceRehovotIsrael

Personalised recommendations