prolog and translating propositional logic

Question

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 implies not(q).

In Prolog this would be:

not(q) :- p

Prolog does not seem to like the not operator in the head of the rule. I get the following error:

 '$record_clause'/2: No permission to redefine built-in predicate `not/1'
        Use :- redefine_system_predicate(+Head) if redefinition is intended

I know two ways to rewrite the general formula for p implies q. First, use the fact that the contrapositive is logically equivalent.

p implies q iff not(q) implies not(p)

Second, use the fact that p implies q is logically equivalent to not(p) or q (the truth tables are the same).

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.

What is the best way around my problem so that I can express p implies not(q)?
Is it possible to write all propositional formulas in Prolog?

EDIT: Now I wish to connect my results with other propositional formulae. Suppose I have the following rule:

something :- formula(P, Q).

How does this connect? If I enter formula(false, true) (which evaluates to true) into the interpreter, this does not automatically make something true. Which is what I want.

All you have to do is choose a different name. not/1 is a built-in in your Prolog implementation. — Daniel Lyons

Will Ness Will Ness · Accepted Answer · 2013-08-19T20:18:14

p => ~q  ===  ~p \/ ~q  === ~( p /\ q )

So we can try to model this with a Prolog program,

formula(P,Q) :- P, Q, !, fail.
formula(_,_).

Or you can use the built-in \+ i.e. "not", to define it as formula(P,Q) :- \+( (P, Q) ).

This just checks the compliance of the passed values to the formula. If we combine this with domain generation first, we can "deduce" i.e. generate the compliant values:

13 ?- member(Q,[true, false]), formula(true, Q).  %// true => ~Q, what is Q?
Q = false.

14 ?- member(Q,[true, false]), formula(false, Q). %// false => ~Q, what is Q?
Q = true ;
Q = false.

prolog and translating propositional logic

2 Answers