[Attempto] A comment on reasoning with RACE

[Norbert E. Fuchs]

Hi

Recently this mailing list discussed RACE's interpretation of the copula "to be", specifically whether the copula should be interpreted symmetrically so that RACE would perform the deduction

(1) John is a man. |- A man is John.

I would like to add a comment to this discussion and to clarify RACE's behaviour a bit. 

Let's start with some definitions.

In first-order predicate logic you define logical consequence "|=" as follows. Given a set of first-order formulas A (axioms) and a set  of first-order formulas T (theorems) you say that T are a logical consequence of A, formally

(2) A |= T

if every model of A is a model of T. (Loosely speaking, T is true whenever A is true.)

For practical reasoning one replaces the semantic concept of logical consequence "|=" by the syntactic concept of proof "|-", formally

(3) A |- T

You say that the proof (3) succeeds if you can deduce T from A in a finite number of steps where each deduction step is an application of an inference rule that syntactically modifies A and ultimately derives T. Often the proof is done equivalently by showing that A ∪ ¬T leads to a contradiction or to inconsistency.

We say that a proof system "|-" is 

  - correct if A |- T implies A |= T   (Loosely speaking, whatever you deduce is a logical consequence.)
  - complete if A |= T implies A |- T  (Loosely speaking, you can deduce all logical consequences.)

While any proof system must be correct, completeness sometimes is sometimes considered of minor importance, for instance in Prolog.


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 problem now boils down to make sure that (5) succeeds. 

RACE is based on the model generator Satchmo, and in this context RACE's proof procedure could simply be described as follows: Develop a model MA for CL_A, develop a model MT for CL_T, and check that MT ⊆ MA.

Based on this approach RACE can prove cases like

(5) John has a red apple. |- John has an apple.

from the ACE axiom alone since obviously MT ⊆ MA.

However, RACE cannot do (1) in the same way since  MT ⊈ MA. That is, RACE is incomplete for this case. To enable the deduction (1), i.e. to achieve completeness for this case, one may hit upon the idea to add the ACE axiom "If John is a man then the man is John.". Though this certainly works, it is not a good idea since the axiom applies only to the case at hand, it is not general enough. Instead, we add to RACE the auxiliary axiom "A is B |- B is A" for any A and B using the RACE's internal representations. Given this auxiliary axiom the model MA is extended by additional elements MAA so that MT ⊆ (MA ∪ MAA), and the proof (1) succeeds. 

Thus, the completeness of RACE is achieved for this case by adding an auxiliary axiom. Similar auxiliary axioms are added to RACE for other cases, e.g. for the relation between plurals and singulars needed in "John has three apples. |- "John has one apple."


RACE's approach raises three interesting points.

First, above I stated that the ACE sentences ACE_A and ACE_T are *assumed* to be true. This is an assumption that we – i.e. the human users – make. Nothing prevents us from deciding otherwise, for instance by assuming that the ACE theorem "A man is John." of (1) is not true. To prevent the deduction (1) in this situation, we must not add the auxiliary axiom "A is B |- B is A" to RACE. Otherwise, we would violate RACE's correctness since we could derive an ACE sentence that is not (assumed to be) true.

Second, auxiliary axioms are expressed in Prolog. Prolog has the power of the Turing machine, meaning that we can deduce anything with the help of suitable auxiliary axioms. Thus, we must not only consider RACE's correctness and completeness, but also its adequateness: What do we want RACE to deduce? What should not be deduced?

Third, no set of auxiliary axioms can satisfy all users of RACE.

Best regards.

Norbert E. Fuchs
Department of Informatics & Institute of Computational Linguistics
University of Zurich