Simple propositional calculus with prolog
Konrad Hoppe
im struggling with a beginner problem. I would like to add this
knowledgebase to prolog:
A <-> B
B <-> not C
C <-> (A <-> B)
but I don't get the right syntax...
the first one should be
a :- b.
b :- a.
the second one
b :- not(c).
c ; b.
and the third, is equal to this set : {{-C, -A, B} , {A,C} , {-B, C}}
hence for prolog:
a;c
c :- b.
b :- a,c.
But this doesn't work at all. Could you give me some hints concerning
my mistakes?
Thanks in Advance
Konrad Hoppe
Chip Eastham
You are trying to model the atomic propositions
A,B,C as nullary (zero-place) predicates. One
reason this is problematic for your intended
application (whatever that may be) is that not/1
in Prolog does not fully represent the semantics
of negation (with respect to the propositional
calculus). In particular Prolog cannot express
B <-> not(C)
in the manner you expect, in that not(c) cannot
be deduced from "knowing" b, but only from a
failed attempt to deduce c.
It would be helpful to know more about the
intended application, i.e. what it would mean
for it to "work at all". But you may be more
satisfied with an algebraic approach in which
the truth-values of propositional variables
A,B,C are used to evaluate Boolean expressions
involving those variables.
regards, chip
Konrad Hoppe
Hi chip,
I'm just playing arround with prolog and propositional as well as
predicate calculus in order to improve my skills in this area. In my
example above "A" means Ann says the truth, "B" means Betty says the
truth and "C" means chloe says the truth. The subformulas are derived
from an aritificial dialogue I've found in an logic book.
I've already solved the whole formula with a truth table and now I
want to solve it in a next step with prolog.
Would you think that's better to model it via predicates of the form
saysTheTruth(ann), saysTheTruth(betty),...
I think there must be a possibility to model this, but I just don't
know how.
All the best,
Konrad
YauHsienHuang
> Hi at all,
> im struggling with a beginner problem. I would like to add this
> knowledgebase to prolog:
>
> A <-> B
> B <-> not C
> C <-> (A <-> B)
>
> but I don't get the right syntax...
> the first one should be
> a :- b.
> b :- a.
Though X :- Y is a rule like "Y implies X," we do not use its function
to model the implication predicate when constructing logic statements.
Instead, a predicate is written as:
imply(a, b).
The X <-> Y equates X -> Y while Y -> X, and <-> is known as "to be
equivalent to." So I would write the knowledge base as:
equiv(a, b).
equiv(b, not(c)).
equiv(c, equiv(a, b)).
Note that not(c) is the representation of a predicate but one of built-
in predicates in SWI. A evaluator knowing the knowledge base and
trying to infer some results from it must be written.
Konrad Hoppe
I'm not sure whether I got it right. When I use
equiv(a, b).
equiv(b, not(c)).
equiv(c, equiv(a, b)).
and want to infer whether 'a' is true I have to make the query ?-equiv
(a,true) , right? but that doesn't work. The prolog interpreter
doesn't recognize that 'c' is true according to this knowledge base.
And what do you mean with:
> Note that not(c) is the representation of a predicate but one of built-
> in predicates in SWI. A evaluator knowing the knowledge base and
> trying to infer some results from it must be written.
The evaluator is swi prolog, isn't it?!
regards,
Konrad
YauHsienHuang
No. Do not give a query directly matching the representation in the
knowledge base. Instead, you ought to write some program for an
evaluator.
eval(equiv(X,Y), Z) :- ...
eval(not(X), Z) :- ...
eval(X, Z) :- ...
YauHsienHuang
wrote:
For instance, the problem #46 of P-99 problems set (https://
prof.ti.bfh.ch/hew1/informatik3/prolog/p-99/) ask you to write program
to check some statement and list a truth table. This problem is really
like yours. My solution for the problem #46 is
and(A, B) :- call(A), call(B).
or(A, _) :- call(A), !.
or(_, B) :- call(B).
%not(A) :- call(A), !, fail.
%not(_) :- true.
nand(A, B) :- not(and(A, B)).
nor(A, B) :- not(or(A, B)).
xor(A, B) :- call(A), not(call(B)).
xor(A, B) :- not(call(A)), call(B).
impl(A, B) :- call(A), !, call(B).
impl(A, _) :- not(call(A)).
equ(A, B) :- impl(A, B), impl(B, A).
table(A, B, C) :- findall(_, eval(A,B,C), _).
eval(A, B, C) :-
combination(1, [true,false], [A]), combination(1, [true,false], [B]),
(A, write(true); not(A), write(fail)), write(' '),
(B, write(true); not(B), write(fail)), write(' '),
(call(C), write(true); not(call(C)), write(fail)), nl.
combination(N, Xs, Xs) :- length(Xs, N).
combination(N, [X|Ys], [X|Zs]) :- length([X|Ys], N1), N @< N1, N2 is
N-1, combination(N2, Ys, Zs).
combination(N, [X|Ys], Zs) :- length([X|Ys], N1), N @< N1, combination
(N, Ys, Zs).
And I can give a query like this:
?- table(A,B,and(not(A),or(A,B))).
true true fail
true fail fail
fail true true
fail fail fail
true.
Konrad Hoppe
thank you for the good example, now I've an idea to deal with my
problem.
and maybe I should work on the list of 99 prolog problems before
continuing on my own...
regards,
Konrad Hoppe
Jan Burse
> Hi at all,
> im struggling with a beginner problem. I would like to add this
> knowledgebase to prolog:
>
> A <-> B
> B <-> not C
> C <-> (A <-> B)
Pure Prolog, that is Prolog without negation as failure, can
be viewed as refutation resolution theorem proving over
horn clauses, via an input strategy.
Now horn clauses are a subset of clauses. Whether we can
represent your problem in Prolog, we have first to transform
your problem into clauses, and see whether they are horn.
A clause has the general form:
A1 v .. v An v ~B1 v ... v ~Bm
Where A1, .., An are the positive literals, and B1, .., Bm are
the negative literals. A clause is horn, if n<=1, that is if there
is maximally one positive literal.
Transformation into clauses works easiest when the problem is
first transformed into conjunctive normal form (CNF). CNF
can be obtained in your case (the fragment of connectives you
are using and we need) by the following rules:
(A <-> B) --> (A -> B) & (B -> A)
(A -> B) --> ~A v B
~(A v B) --> ~A & ~B
~(A & B) --> ~A v ~B
~~A --> A
A v (B & C) --> (A v B) & (A v C)
~A v A --> t
t v A --> t
t & A --> A
Lets try this for your formulas:
A <-> B --> (A -> B) & (B -> A)
--> (~A v B) & (~B v A)
two clauses which are horn, good
B <-> ~C --> (B -> ~C) & (~C -> B)
--> (~B v ~C) & (~~C v B)
--> (~B v ~C) & (C v B)
two clauses, one is horn, the other not, bad
C <-> (A <-> B) --> (C -> (A <-> B)) & ((A <-> B) -> C)
--> (C -> ((A -> B) & (B -> A))) &
(((A -> B) & (B -> A)) -> C)
--> (~C v ((A -> B) & (B -> A))) &
(~((A -> B) & (B -> A)) v C)
--> (~C v (A -> B)) &
(~C v (B -> A)) &
(~(A -> B) v ~(B -> A) v C)
--> (~C v ~A v B) &
(~C v ~B v A) &
(~(~A v B) v ~(~B v A) v C)
--> (~C v ~A v B) &
(~C v ~B v A) &
((~~A & ~B) v (~~B & ~A) v C)
--> (~C v ~A v B) &
(~C v ~B v A) &
(~~A v ~~B v C) &
(~B v ~~B v C) &
(~~A v ~A v C) &
(~B v ~A v C)
--> (~C v ~A v B) &
(~C v ~B v A) &
(A v B v C) &
(~B v B v C) &
(A v ~A v C) &
(~B v ~A v C)
--> (~C v ~A v B) &
(~C v ~B v A) &
(A v B v C) &
(t v C) &
(t v C) &
(~B v ~A v C)
--> (~C v ~A v B) &
(~C v ~B v A) &
(A v B v C) &
t &
t &
(~B v ~A v C)
--> (~C v ~A v B) &
(~C v ~B v A) &
(A v B v C) &
(~B v ~A v C)
four clauses, three are horn, one is not horn, bad
Here is a summary of the theory as a list of clauses.
Also shown which are horn, and which not:
~A v B Horn
~B v A Horn
~B v ~C Horn
C v B Not Horn
~C v ~A v B Horn
~C v ~B v A Horn
A v B v C Not Horn
~B v ~A v C Horn
Since CNF transformation is relatively tame, we could
say the above is more or less a literal translation of
your "knowledge". And it is as such not Horn, cannot
be dealt with in Pure Prolog.
This does not answer where the above can be transformed
into something Horn (is possible sometimes). And it does
also not answer what Prolog with negation as failure is
able to do.
Best Regards
Chip Eastham
Thanks, Konrad. That's much clearer. You
can of course adapt the truth-table approach
to a Prolog implementation, wherein truth
values for A,B,C are generated and tested
using the "constraints":
A <-> B
B <-> not C
C <-> (A <-> B)
Now the truth values can be represented
as 0,1 mod 2 with the convention that 1
is truth and 0 is falsehood, then:
A <-> B becomes A is B
B <-> not C becomes B is 1-C
C <-> (A <-> B) becomes C is 1+A+B mod 2
Note that '<->' is being used both as an
assignment and a Boolean operator that
returns 1 iff both operands are equal.
Play around with these ideas. The proof
by contradiction now amounts to backtracking
on failure at inconsistent assignments, e.g.
C cannot be both 0 and 1.
regards, chip
Jan Burse
> Since CNF transformation is relatively tame, we could
> say the above is more or less a literal translation of
> your "knowledge". And it is as such not Horn, cannot
> be dealt with in Pure Prolog.
Of course a boolean constraint representation is possible.
Like given by the 99 Prolog examples post.
Or you could use Shannon trees to represent the boolean
expressions. When the Shannon tree reduces to true,
well then your boolean expressions are a tautology.
Here is Prolog code for Shannon trees:
http://www.xlog.ch/papers/integ01/Helper06a.pdf
Page 18, ff
PropOperations
/**
* This class provides inferencing on propositional trees. A
* propositional tree is either a leaf or a node. A leaf is
* either true or false. A node has a propositional variable
* and two branches.
*
* Tree = leaf(Value) | node(Variable,Tree,Tree)
*
* The interpretation of the tree are as follows. A leaf is
* interpreted by its value. A node is interpreted as a
* case switch.
*
* [leaf(Value)] = Value
* [node(Variable,T1,T2)] = (Variable and [T1]) or
* (not Variable and [T2])
And there are many more methods, which all allow an
indirect handling of propositional logic in Prolog.
Since Prolog is turing complete, and propositional
logic, i.e. SAT is NP which is less than turing
complete, this is not a surprise.
Bye