I am trying to encode basic logical inferences in Prolog, and I want to define some custom operators to streamline the notation. It would be handy if I can type |- for ⊢. So I tried
:- op(1150, xfy, [ '|-' ]).
gamma |- a.
Gamma |- or(A,_) :- Gamma |- A.
Gamma |- or(_,A) :- Gamma |- A.
but when I try the query gamma |- or(a,X), I get the error message
ERROR: '<meta-call>'/1: Undefined procedure: gamma/0
instead of the true I expect.
The problem seems to be that the defined operator includes a vertical bar character. If I modify the knowledge base to
:- op(1150, xfy, [ imp ]).
gamma imp a.
Gamma imp or(A,_) :- Gamma imp A.
Gamma imp or(_,A) :- Gamma imp A.
Then Prolog has no problems answering the query gamma imp or(a,X). Is the vertical bar a reserved character that I'm not allowed to use in definitions? Or is there some way around this?
You cannot do this. Neither in ISO Prolog nor in SWI. While the vertical bar serves as an operator — provided a corresponding operator declaration is present, it cannot be used unquoted as part of an operator with a length of two or more characters. The best you can get in your situation is to declare an operator |- and use it in quoted form. In both cases below, quotes are strictly needed.
:- op(1200, xfx, '|-').
a '|-' b.
Doesn't look too attractive. Alone, as a single character, the bar serves as an infix operator.
?- ( a | b ) = '|'(a, b).
true.
?- current_op(Pri,Fix,'|').
Pri = 1105, Fix = xfy.
There is another use of | as a head-tail separator in lists. Due to the restrictions to the priority the infix bar can take, there is no ambiguity between [A|As] and above use.
Note that [a|-]. is valid Prolog text. Even gamma |- a. is valid in SWI and even valid Prolog text in ISO, provided there is an operator declaration!
?- write_canonical((gamma|-a)).
'|'(gamma,-(a))