title: prolog and translating propositional logic
body: <p>My ultimate goal is to load a set of propositional formulas in to Prolog from a file in order to deduce some facts. Suppose I have the propositional formula:</p>
  
  <pre><code>p implies not(q).
  </code></pre>
  
  <p>In Prolog this would be:</p>
  
  <pre><code>not(q) :- p
  </code></pre>
  
  <p>Prolog does not seem to like the <code>not</code> operator in the head of the rule. I get the following error: </p>
  
  <pre><code> '$record_clause'/2: No permission to redefine built-in predicate `not/1'
          Use :- redefine_system_predicate(+Head) if redefinition is intended
  </code></pre>
  
  <p>I know two ways to rewrite the general formula for <code>p implies q</code>. First, use the fact that the contrapositive is logically equivalent.</p>
  
  <p><code>p implies q</code> iff <code>not(q) implies not(p)</code></p>
  
  <p>Second, use the fact that <code>p implies q</code> is logically equivalent to <code>not(p) or q</code> (the truth tables are the same). </p>
  
  <p>The first method leads me to my current problem. The second method is then just a conjunction or disjunction. You cannot write only conjunctions and disjunctions in Prolog as they are not facts or rules.</p>
  
  <ol>
  <li>What is the best way around my problem so that I can express <code>p implies not(q)</code>?</li>
  <li>Is it possible to write all propositional formulas in Prolog?</li>
  </ol>
  
  <p><strong>EDIT:</strong> Now I wish to connect my results with other propositional formulae. Suppose I have the following rule:</p>
  
  <p><code>something :- formula(P, Q).</code></p>
  
  <p>How does this connect? If I enter <code>formula(false, true)</code> (which evaluates to true) into the interpreter, this does not automatically make <code>something</code> true. Which is what I want.</p>