Open arademaker opened 7 months ago
I know that LKB has a scope resolution code. See also https://aclanthology.org/P04-1032.pdf. It may not be as efficient as https://github.com/coli-saar/utool, but it can be a starting point.
LKB> (let* ((sentence "every boy loves a woman.") (user-input (lkb::split-into-words sentence))) (lkb::parse user-input nil) (when *parse-record* (let* ((edges *parse-record*) (mrs (mrs::extract-mrs (car edges)))) (setf mrs::*canonical-bindings* nil) (format t "mrs: ~a~%" mrs) (let* ((binding-sets (mrs::make-scoped-mrs mrs))) (loop for binding in binding-sets do (setf mrs::*canonical-bindings* (mrs::canonical-bindings binding)) (let* ((gq-exp (mrs::output-gq-mrs mrs)) ; (fol (mrs::convert-gq-to-fol-top gq-exp)) ) (format t "~%~%~A ~%~A ~%~A ~%~A" sentence binding-sets mrs::*canonical-bindings* gq-exp))))))) mrs: h1:e3:{ h4:"_every_q"(x6 h7 h5) h8:"_boy_n_1"(x6) h2:"_love_v_1"(e3 x6 x9) h10:"_a_q"(x9 h12 h11) h13:"_woman_n_1"(x9) }{ h1 qeq h2, h7 qeq h8, h12 qeq h13 } every boy loves a woman. (((13 12 13) (10 5 10) (2 11 2) (8 7 8) (4 1 4) (1 1 4) (11 11 2) (12 12 13) (5 5 10) (7 7 8)) ((13 12 13) (10 1 10) (2 5 2) (8 7 8) (4 11 4) (1 1 10) (11 11 4) (12 12 13) (5 5) (7 7 8))) ((4 . 4) (1 . 4) (8 . 8) (7 . 8) (2 . 2) (11 . 2) (10 . 10) (5 . 10) (13 . 13) (12 . 13)) (_EVERY_Q ?X6 (_BOY_N_1 ?X6) (_A_Q ?X9 (_WOMAN_N_1 ?X9) (_LOVE_V_1 ?E3 ?X6 ?X9))) every boy loves a woman. (((13 12 13) (10 5 10) (2 11 2) (8 7 8) (4 1 4) (1 1 4) (11 11 2) (12 12 13) (5 5 10) (7 7 8)) ((13 12 13) (10 1 10) (2 5 2) (8 7 8) (4 11 4) (1 1 10) (11 11 4) (12 12 13) (5 5) (7 7 8))) ((4 . 4) (11 . 4) (8 . 8) (7 . 8) (2 . 2) (5 . 2) (10 . 10) (1 . 10) (13 . 13) (12 . 13)) (_A_Q ?X9 (_WOMAN_N_1 ?X9) (_EVERY_Q ?X6 (_BOY_N_1 ?X6) (_LOVE_V_1 ?E3 ?X6 ?X9)))
In the Utool documentation, these bindings are the plugging-lkb format! But the docs do not describe these triples.
plugging-lkb
From @EricZinda a documentation about the task and solution with links to the code
I decided to implement the code to call Utool from Lean. For that, we need:
I know that LKB has a scope resolution code. See also https://aclanthology.org/P04-1032.pdf. It may not be as efficient as https://github.com/coli-saar/utool, but it can be a starting point.
In the Utool documentation, these bindings are the
plugging-lkb
format! But the docs do not describe these triples.