[Attempto] RACE answers queries "how many" and "how much"

[Norbert E. Fuchs]

On 13 Apr 2012, at 17:09 , David Whitten wrote:

> Thank you again Norbert for helping understand what RACE was attempting to communicate.
> 
> With your indulgence I would ask If you could clarify a little more. 
> I asked the query expecting that there would be no solution
> to the query.  I think that from the statement "every woman is a human", 
> then this statement should be equivalent to the statement 
> that "there does not exist a woman who is not a human".
> 
> How does RACE communicate that the set of facts satisfying the theorem
> is empty ? 
> 
> It doesn't seem to me that this is the same as saying that the 
> theorem doesn't follow from the axioms.  
> 
> If I said "the theorem doesn't follow from the axioms", 
> I think I would mean that with a better set of axioms, 
> the ambiguity in the theorem would be removed and it would be 
> possible to prove the theorem from the axioms. Another way
> to interpret it would be to say that the theorem is not in the
> deductive closure of the axioms.
> 
> I know that I haven't spent as much time in the field as some of the
> other people on this list, so please enlighten me if I am not thinking clearly.
> 
> Best Wishes,
> David Whitten
> 713-870-3834

David

Let's assume that we want to do the proof 

ACE_Axioms |- ACE_Theorems

RACE proceeds as follows

  - translate ACE_Axioms (via DRS) into first-order clauses Axiom_Clauses
  - translate ACE_Theorems (via DRS) into first-order clauses Theorem_Clauses
  - check whether Axiom_Clauses ∪ ¬Theorem_Clauses is (in-) consistent
  - if Axiom_Clauses ∪ ¬Theorem_Clauses is inconsistent 
    then identify all minimal subsets of the clauses, and ultimately all minimal subsets Inconsistencies of ACE_Axioms, that lead to inconsistency  
  - if Axiom_Clauses ∪ ¬Theorem_Clauses is consistent 
    then generate all minimal models Models of Axiom_Clauses ∪ ¬Theorem_Clauses  

The result of the proof is either

  - Axiom_Clauses ∪ ¬Theorem_Clauses is consistent
    Inconsistencies = [], Models can be empty or not empty
    meaning ACE_Axioms |\- ACE_Theorems
    RACE reports "ACE_Theorems do not follow from ACE_Axioms"

or

  - Axiom_Clauses ∪ ¬Theorem_Clauses is inconsistent
    Inconsistencies ≠ [], Models = []
    meaning (subsets of) ACE_Axioms |- ACE_Theorems
    RACE reports "The following minimal subsets of the axioms entail the theorems: ..." 

RACE does not externally report Models.

Regards.

   --- nef