Logic Programming

  • Mordechai Ben-Ari

Abstract

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.

Keywords

Sorting Paral Prefix Suffix 

Preview

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