[Attempto] A comment on reasoning with RACE (a clarification)

[Norbert E. Fuchs]

On 29 Apr 2012, at 20:02 , Norbert E. Fuchs wrote:

> ... In RACE we deduce ACE theorems ACE_T from ACE axioms ACE_A where ACE_A and ACE_T are assumed to be true. (If ACE_T is a query then the query with all query words substituted is assumed to be true.) 
> 
> (4) ACE_A |- ACE_T
> 
> ACE_A and ACE_T are translated into FOL formulas in clausal form CL_A, respectively CL_T, and RACE tries the proof
> 
> (5) CL_A |- CL_T
> 
> We define that (4) succeeds if and only if (5) succeeds. Consequently, (5) should succeed since RACE should be correct and complete, and both ACE_A and ACE_T are assumed to be true. 

The last sentence could be misunderstood. Perhaps I should have better written 

The proof (5) should succeed for the clauses derived from "John is a man. |- A man is John." since we assume that the theorem "A man is John." is true whenever the axiom "John is a man." is true, and RACE is intended to be complete.

Regards.

   --- nef