Prolog resolution prover deletes brackets

user_13500246 0
Viewed 184

I'm writing a resolution prover in prolog, which takes inputs of the form

[[(a or b) equiv neg(c and d)]]

etc., and converts them into CNF. All logical operators work fine, but when the program attempts to expand an equiv operation, brackets go missing. For example, performing one step of the algorithm on

[[(a and b) equiv c]]

gives the result

[[neg(a and b) or c], [neg c or a and b]]

In the second clause, the brackets around a and b have been deleted, while they remain in the first clause. Why is this happening?

For reference, this is my code and the command giving that output is singlestep([[(a and b) equiv c]], X). The specific code for how equiv should be dealt with is at line 93, and the function singlestep is at line 108.

prolog logic syntax
1 Answers

This is happening because the operator precedence is defined in such a way that

neg c or (a and b)

and

neg c or a and b

are equivalent. You do not include your operator declaration, but they are likely to be both xfy with equal priority.

To test the equivalence, you could try simple pattern-matching:

?- neg c or a and b = X or Y.
X = neg c,
Y = a and b?

?- neg c or a and b = X and Y.
no.

Confirming how operators are interpretated.

user_7048170
Related