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.


Sorting Paral Prefix Suffix 


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