Deduction in Prolog

Question

This is an elementary Prolog question. I'm trying to implement reasoning that may be informally expressed like this:

The (necessary but not sufficient) conditions for x(X) to be true are that a(X) and b(X) must hold. We know that x(mary). Those conditions must have held for x(mary) to be the case. It is the case. Therefore a(mary) and b(mary) are both true.

The following code clearly doesn't do what I have in mind:

a(jim).
b(jack).
x(X) :- a(X), b(X).
x(mary).

If I now ask a(mary), Prolog answers with a No.

I'm pretty sure I understand why it answers this way. I just don't know how to correctly implement what I want.

UPDATE:

The above example is simplified. In the actual problem I'm working on, a and b are intertwined. Instead of x(X) :- a(X), b(X)., I actually have r(A,B,C) :- p(A,D), p(C,E), a(D,n), a(E,c), s(B,E,F,2), s(C,E,D,1), s(C,E,F,1).. That is, for r(A,B,C) to hold, it is necessary that all the interlinked conditions on the right hold together. Now it doesn't seem right to replace this with a series of rules p(A,D) :- r(A,B,C). a(D,n) :- r(A,B,C). and so on, because, as I understand it, the D in the p(A,D) is no longer the same as the D in the a(D,n), these being now totally independent rules. I could easily implement the reasoning I want in a (deductive) automated theorem prover for first order logic, which I am more familiar with than with Prolog.

Another example. Consider this Prolog code:

breathable(X) :- part(X,Y), atom(Y,o).
part(air,oxygen).
breathable(air).

Air is breathable. Air contains oxygen. I want to infer that atom(oxygen,o). But Prolog will answer No.

Answer 1

In your breathable example, you'd need an added rule:

atom(X, Y) :- breathable(Y), part(Y, X).

Without this rule, it's logic would not be implicitly and consistently true with your existing rule base and fact schema. It is, in part, a converse of your existing rule. From a purely logical perspective, the converse of an implication doesn't necessarily hold true just because the original implication is true. The truth of atom(oxygen, o) in the simple example given is established by the converse of the existing rule plus currently available, specific facts. This is basically a form of abductive logic, not deduction as your question title suggests. Without the new atom/2 rule, if new part facts are added later without even changing your fact schema, that abductive process may cause the example query to fail or be non-provable, different than the current result. So it's not reliable without an explicit rule.

Answer 2

"Those conditions must have held for x(mary) to be the case. It is the case. Therefore a(mary) and b(mary) are both true."

Let's express that in code, shall we?

a(X) :- x(X).
b(X) :- x(X).

That should produce the expected result.

Answer 3

You probably think of it the wrong way. Currently you have written: "x(X) holds given a(X) and b(X) hold, or X is mary.".

Not the opposite way. If you want to write: "a(A) holds given A is jim or X(A).", you should write:

a(jim).
a(A) :-
    x(A).

So you probably want to write:

a(jim).
a(A) :-
    x(A).

b(jack).
b(B) :-
    x(B).

x(mary).