First to the logical part: two formulas A and B are equivalent if A → B ∧ B → A holds. If you can prove this formula you are done.
Now to the prolog part:
- You are mixing up the predicate and the term level:
and(A, B) will fail with the error message that A is not sufficiently instantiated. It is much easier to create a predicate eval and define eval(and(A,B)), eval(or(A,B)), etc.
- You don't have a representation of logical variables. Say my formula is just
A. How do I find out if A may be take on true / false? I would propose to explicitly wrap a variable into a a constructor var(Truthvalue) to distinguish it from logical operators during pattern matching. Otherwise, your proof search will try to expand a variable to a more complex formula which is obviously not helpful.
- You use cuts / fail where they are not necessary: there is only one definition of
and(P,Q) such that the cut does not do anything. Similarly, fail makes a rule fail as if it were not there - so you can just delete those rules (unless you use the extralogical features of cut, that is). Remember that cut does not behave like a logical construct and should be avoided as much as possible.
- You have problems with formulating negation: you have no explicit rule for negation and your predicates for ⊤ and ⊥ are not connected to the rest of your rules (assuming you wanted to define ¬A as A → ⊥). This is due to the assymetry of Prolog rules: deriving a predicate means it is true but non-derivability is not a good means for defining logically false statements. In this case, we can make it explicit, what it means that a formula is false: e.g.
A ∧ B is false if A is false or B is false (or both). Let's split eval into two parts then: eval_tt(X) is derivable is if X is true and eval_ff(X) is derivable if X is false.
Putting all these notes together, this a minimal complete calculus for ∧ and ¬ only:
eval_tt(var(true)).
eval_tt(and(A,B)) :-
eval_tt(A),
eval_tt(B).
eval_tt(not(A)) :-
eval_ff(A).
eval_ff(var(false)).
eval_ff(and(A,_B)) :-
eval_ff(A).
eval_ff(and(_A,B)) :-
eval_ff(B).
eval_ff(not(A)) :-
eval_tt(A).
We can query the models for ¬(A ∧ ¬B) with the query:
?- eval_tt(not(and(var(A), not(var(B))))).
A = false ;
B = true.
Would we have used cut or negation as failure, we would probably nothave found both solutions.
Also A ∧ ¬A is unsatisfiable, as expected:
?- eval_tt(and(var(A), not(var(A)))).
false.
Now you just need to extend this minimal calculus by other operators you would like to have (disjunction, implication, equivalence, etc.). Btw. if you have seen sequent calculus, you might recognize some of the ideas :)
Edit: I haven't explained how to get from satisfiability to validity. The problem is the following: an answer substitution from a query to eval_tt(X) only tells us that X is satisfiable. In logic, we usually define X as valid in terms of ¬X being unsatisfiable. This can be expressed in Prolog with negation as failure by defining:
valid(X) :-
\+ eval_ff(X).
What's the problem here? We check a formula for satisfiability, e.g.
?- valid2(not(and(var(X),not(var(X))))).
true.
but we don't get an answer substitution. In particular if the query is not sufficiently instantiated, we get wrong results:
?- valid(X).
false.
But there's certainly a valid formula - we tried one above. I have not found a good solution yet that can enumerate all the valid formulas.
