CODEWITHSUNDEEP
prologlogicboolean-logic
CodeKingPlusPlus
CodeKingPlusPlus

Reputation: 16081

prolog and translating propositional logic

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.

  1. What is the best way around my problem so that I can express p implies not(q)?
  2. 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.

Upvotes: 2

Views: 2545

Answers (2)

NotAUser
NotAUser

Reputation: 1466

You are using the wrong tool. Try Answer Set Programming.

Upvotes: -2

Will Ness
Will Ness

Reputation: 71119

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.

Upvotes: 4

Related Questions