This thread started in 2020 and I am still playing with text entailment in the SICK dataset using logic reasoning. Actually, the main motivation is that proofs can be eventually constructed with neuro-symbolic provers like ([2006.13155] Logical Neural Networks) and huge knowledge bases. Given that goal, I started working with MRS to FOL before going to more expressive approaches (e.g. A Type-Theoretical system for the FraCaS test suite: Grammatical Framework meets Coq - ACL Anthology).

For a simplified sentence from the SICK dataset:

```
'A boy is playing piano'
[ TOP: h0
INDEX: e2
RELS: < [ _a_q<0:1> LBL: h4 ARG0: x3 RSTR: h5 BODY: h6 ]
[ _boy_n_1<2:5> LBL: h7 ARG0: x3 ]
[ _play_v_1<9:16> LBL: h1 ARG0: e2 ARG1: x3 ARG2: x8 ]
[ udef_q<17:22> LBL: h9 ARG0: x8 RSTR: h10 BODY: h11 ]
[ _piano_n_1<17:22> LBL: h12 ARG0: x8 ] >
HCONS: < h0 qeq h1 h5 qeq h7 h10 qeq h12 > ]
'No boy is playing piano'
[ TOP: h0
INDEX: e2
RELS: < [ _no_q<0:2> LBL: h4 ARG0: x3 RSTR: h5 BODY: h6 ]
[ _boy_n_1<3:6> LBL: h7 ARG0: x3 ]
[ _play_v_1<10:17> LBL: h1 ARG0: e2 ARG1: x3 ARG2: x8 ]
[ udef_q<18:23> LBL: h9 ARG0: x8 RSTR: h10 BODY: h11 ]
[ _piano_n_1<18:23> LBL: h12 ARG0: x8 ] >
HCONS: < h0 qeq h1 h5 qeq h7 h10 qeq h12 > ]
```

My translator from MRS to FOL gives me F1 for the first MRS above and F2 for the second:

```
[F1] ā e2, ā x8, _piano_n_1 x8 ā§ (ā x3, _boy_n_1 x3 ā§ _play_v_1 e2 x3 x8)
[F2] ā e2, ā x8, _piano_n_1 x8 ā§ (ā x3, _boy_n_1 x3 ā Ā¬_play_v_1 e2 x3 x8)
```

Does it make sense so far? My transformation is based on http://svn.delph-in.net/lkb/branches/fos/src/tproving/gq-to-fol.lisp. But I consider more quantifiers and I allow high-order predicates (with formulas as arguments).

For these two sentences, I would expect to be able to find a proof of the contradiction using a FOL prover, that is, a proof that `not(and(F1, F2))`

is a tautology, or that `and(F1, F2)`

is unsatisfiable.

but, of course, the problem is that the existential variables are different so there is no logical contradiction and I will need to eventually unify some existential variables first, I imagine that I would need to make some variables unification in the two MRS before the FOL transformation. But I suspect people already investigated approaches to that, right? Any obvious direction?

```
Ā¬((ā e2, ā x8, _piano_n_1 x8 ā§ (ā x3, _boy_n_1 x3 ā§ _play_v_1 e2 x3 x8)) ā§
(ā e2, ā x8, _piano_n_1 x8 ā§ (ā x3, _boy_n_1 x3 ā Ā¬_play_v_1 e2 x3 x8)))
```