Clarification on bounds

[loc-trinh]

From the tutorial, it seems like a CONTRADICTION is when L > U: however, the results bellow happens quite often when L > U is considered APPROX TRUE.

Can someone help to clarify this?

Model before inference:

---

                            LNN Model

OPEN And: (A ∧ B) APPROX_TRUE (0.51, 0.52)

OPEN Proposition: B APPROX_TRUE (0.9, 0.99)

OPEN Proposition: A APPROX_TRUE (0.9, 0.99)

---

Model after inference:

---

                            LNN Model

OPEN And: (A ∧ B) APPROX_TRUE (0.8, 0.52)

OPEN Proposition: B APPROX_TRUE (0.9, 0.99)

OPEN Proposition: A APPROX_TRUE (0.9, 0.99)

[loc-trinh]

Specifically: OPEN And: (A ∧ B) APPROX_TRUE (0.8, 0.52)

[NaweedAghmad]

Hi there, thanks for bringing this to our attention. You are correct, there seems to be an error in the calculation of the state. The end result should be a contradiction.

[loc-trinh]

Hi again, sorry to re-ping this. I was wondering if you guys have a timeline on when this will be patched? Is the current version usable as a theorem prover?

[NaweedAghmad]

• The above patch should work, the contradiction was correctly being calculated but incorrectly overridden thereafter.

Is the current version usable as a theorem prover?

• There is a subset of FOL problems (primarily theorems without functions or equality) that the LNN should be able to solve. However certain problems with negations on bindings are known to not work here due to the complexity of grounding management having to compute set complements.