From: yingun@gmail.com   
      
   I just tried out the Eprover of Automated Theorem Prover, I was   
   wondering if the ATP could give the result of query just like prolog.   
   Does the purpose of ATP function just to check whether and equation   
   can be proven ? Does it does something like prolog, where it can show   
   the bounded variable ? Thanks   
      
   Prolog :   
   husband(john,marry).   
   ?- husband(X,Y).   
      
   X = john   
   Y = wife   
      
   Yes   
      
   Eprover LOP :   
   husband(john,marry) <- .   
   <- husband(X,Y).   
      
   # Proof found!   
   # SZS status Unsatisfiable   
   # Initial clauses:                     : 2   
   # Removed in preprocessing             : 0   
   ..........   
      
   [ comp.ai is moderated ... your article may take a while to appear. ]   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)