natural language semantics with THORN

[dr.mt...@gmail.com]

This is something most of you won't have seen.  A model for giving the semantics of natural language statements based on generating equivalences of the form S is true <=> P

where S is a sentence of the object language and the metalanguage is first-order logic.  Something like this was a vogue in philosophy 50 years ago, but purely theoretically.   People didn't use computers on this.  I thought I'd try THORN 19 on it.

(I need to put THORN 19 up, it is an advance on what is there now).

(define axioms
  {--> (list prop)}
  -> [[all x [[sat x "bald"] <=> [bald x]]]
      [all x [all y [all z [[[name x] & [[cop y] & [adj z]]]
                <=> [[istrue [cn x [cn y z]]] <=> [sat [den x] z]]]]]]
      [all x [all y [[sat [pair x y] "bigger"] <=> [bigger x y]]]]
      [all p [all q [[istrue [cn p [cn "and" q]]] <=> [[istrue p] & [istrue q]]]]]          
      [[den "Tom"] = tom]
      [[den "Jerry"] = jerry]
      [name "Tom"]
      [name "Jerry"]
      [adj "bald"]
      [cop "is"]])

(kb-> (axioms))

I asked it to prove the T sentence.

 [[istrue [cn [cn "Tom" [cn "is" "bald"]] [cn "and" [cn "Jerry" [cn "is" "bald"]]]]]
            <=> [[bald tom] & [bald jerry]]])

i.e. "Tom is bald and Jerry is bald" is true iff (bald Tom) & (bald Jerry).

(15+) (<-kb [[istrue [cn [cn "Tom" [cn "is" "bald"]] 

                      [cn "and" [cn "Jerry" [cn "is" "bald"]]]]]
                          <=> [[bald tom] & [bald jerry]]])

run time: 0.75 secs
1598986 inferences, equality = true
depth = 20, complexity = -1, timeout = 60 secs
true : boolean

The proof is attached.  Love this stuff but wildly inefficient as a means of representing natural languages.

Mark

[dr.mt...@gmail.com]

The methodology comes from Tarski's semantic theory of truth.

There are certain theoretical strengths of the approach.  A T sentence

BTW, is a a theorem of the form S is true <=> P.   The two strengths are:

1.  A theory of machine translation for free.

Suppose you have English and French and you give the semantics of both in

a common metalanguage.  Given  an English sentence S and a French sentence

S*, you can prove they are semantically equivalent by proving 

|- S is true iff p.

|- S* is true iff p

hence

|- S is true <=> S* is true

2.  Machine Learning for free.

You can ask question like 'Given this unknown word, to what lexical category must 

it belong for the context in which it occurs to be a sentence?'  This requires a light

reformulation of what I presented.

It's theoretically elegant but a full scale model for English would require an axiom 

base of around 250,000 axioms!  Nobody has ever tried to build a first-order theory

of that size.

M.

[dr.mt...@gmail.com]

Anyway here is machine translation in the small a la Tarski.

I give the semantics for a fragment of English and the equivalent in French.

Then I prove S translates as S* (and vice versa of course) by proving as

a theorem that S and S* are equivalent.  Namely, it is a theorem that S

is true in English iff S* is true in French.

(define axiomsEng

  {--> (list prop)}
  -> [[all x [[sat x "bald"] <=> [bald x]]]

      [all x [all y [all z [[[name x] & [[copEng y] & [adjEng z]]]
                <=> [[istrueEng [cn x [cn y z]]] <=> [sat [den x] z]]]]]]
      [all p [all q [[istrueEng [cn p [cn "and" q]]] <=> [[istrueEng p] & [istrueEng q]]]]]

      [[den "Tom"] = tom]
      [[den "Jerry"] = jerry]
      [name "Tom"]
      [name "Jerry"]

      [adjEng "bald"]order THORN to compile this theory.
      [copEng "is"]])

(define axiomsFr
  {--> (list prop)}
  -> [[all x [[sat x "chauve"] <=> [bald x]]]
      [all x [all y [all z [[[name x] & [[copFr y] & [adjFr z]]]
                <=> [[istrueFr [cn x [cn y z]]] <=> [sat [den x] z]]]]]]
      [all p [all q [[istrueFr [cn p [cn "et" q]]] <=> [[istrueFr p] & [istrueFr q]]]]]  
      [adjFr "chauve"]
      [copFr "est"]])
     
(kb-> (append (axiomsEng) (axiomsFr)))      \\ order THORN to compile

(thorn.complex 21)  \\ bound the complexity of the goals
(thorn.depth 20)

\\  |- "Tom is bald and Jerry is bald" is true in English iff  "Tom est chauve et Jerry  est chauve " is true in French

(<-kb [[istrueEng [cn [cn "Tom" [cn "is" "bald"]]

            [cn "and" [cn "Jerry" [cn "is" "bald"]]]]]

     <=> [istrueFr [cn [cn "Tom" [cn "est" "chauve"]]
              [cn "et" [cn "Jerry" [cn "est" "chauve"]]]]]]) 

run time: 7.453125 secs
13553194 inferences, equality = true
depth = 20, complexity = 21, timeout = 60 secs
true

Find proof attached.  Heroic. ;)  I'll put THORN 19 up.

M.