[developers] Playing with Utool for solving scope underspecification

[Alexandre Rademaker]

Hi all,

Should I use http://delphinqa.ling.washington.edu or https://github.com/delph-in/docs/issues? Anyway… 


https://www.coli.uni-saarland.de/projects/chorus/utool/docs/3.1.1/manual/0005.html#toc18

plugging-lkb: The output is a complex Lisp list that mimicks the output of the MRS solver in the LKB system. We don't describe this concrete syntax here.

I didn’t find any detailed information about this format in the mrsresolve.lisp file of LKB source code. 


Input: the old coder taught the new coder


The output in the plugging-lkb format is:

<result solvable='true' count='2' fragments='6'  chartsize='5'  time-chart='0'  time-extraction='0' >
  <solution string='((0 0 10) (10 0 10) (11 11 13) (13 11 13) (12 12 4) (4 12 4) (5 5 7) (7 5 7) (6 6 1) (1 6 1))' />
  <solution string='((0 0 4) (4 0 4) (5 5 7) (7 5 7) (6 6 10) (10 6 10) (12 12 1) (1 12 1) (11 11 13) (13 11 13))' />
</result>

The output in the plugging-oz format is:

<result solvable='true' count='2' fragments='6'  chartsize='5'  time-chart='0'  time-extraction='1’ >
  <solution string='[plug(h0 h10) plug(h11 h13) plug(h12 h4) plug(h5 h7) plug(h6 h1)]' />
  <solution string='[plug(h0 h4) plug(h5 h7) plug(h6 h10) plug(h12 h1) plug(h11 h13)]' />
</result>


So it looks like I can take lkb format as an associative list where the keys are the handlers. 

CL-USER> (assoc 0 '((0 0 10) (10 0 10) (11 11 13) (13 11 13) ...))
 (0 0 10)

If I don’t need/want to inspect the scopes by handlers, I can do the following to obtain the oz output:

CL-USER> (remove-duplicates (mapcar #'cdr '((0 0 10) (10 0 10) (11 11 13) (13 11 13) ...))
			    :test #'equal)
((0 10) (11 13) (12 4) (5 7) (6 1))


Am I right? Is that the right interpretation? My end goals is to produce FOL formulas from the resolved MRS like the one below, constructed from the output above:

_the_q(x10, _new_a_1(e15, x10) /\ _coder_n_1(x10), 
            _the_q(x7, _old_a_1(e9, x7) /\ _coder_n_1(x7), 
                       _teach_v_1(e3, x7, x10)))


LKB gives me the output below, which is interesting because for this case, it takes all generalized quantifiers from the resolved MRS and made a skolemization of the existential before adding new existential for the events.

'(exists ?e15
	 (exists ?e9
		 (exists ?e3
			 (and (and (_new_a_1 ?e15 const?x10)
				   (_coder_n_1 const?x10))
			      (and (and (_old_a_1 ?e9 const?x7)
					(_coder_n_1 const?x7))
				   (_teach_v_1 ?e3 const?x7 const?x10))))))


I tested with `the old coder taught every new coder` and for this it keeps the universal quantifier.

(exists ?e15
	(exists ?e9
		(exists ?e3
			(forall ?x10
				(or (not (and (_new_a_1 ?e15 ?x10) (_coder_n_1 ?x10)))
				    (and (and (_old_a_1 ?e9 const?x7) (_coder_n_1 const?x7))
					 (_teach_v_1 ?e3 const?x7 ?x10)))))))


Best,
Alexandre