For an equivocation-induced premise/hypothesis pair (known as incoherent universals) only — not for all Neutral pairs.
Meta Hackathon submission. Theoretical proof only. No empirical evaluation. No evaluator.
Background: Natural Languages have quirks and ambiguity. This was designed for the fun of language and its several facets of meanings. Based on lexical ambiguities, or multiple meanings to same word, or similarly pronounced words. When I created an example as follows, it was meant to introduce something comical. The example turned out fun and funny to me. I present six resolution procedures that label Natural Language Inference by an FOL-extended method. The methods ground in developing mapping function, Domain and Interpretation using Symbolic Logic-based proofs.
Natural Language Inference (NLI) takes a premise and a hypothesis and labels the pair: Entailment if the hypothesis must follow, Contradiction if it must be false, Neutral if neither follows.
Premise: “Bat is a mammal. Bat is used in baseball. Bats have wings. Bats have a barrel. Wings are not barrels. Barrels are not wings. Bats can fly. There is a Brown bat.”
Hypothesis: “Brown bat is a mammal.”
Whatever colour is used, the phrase is commonly grounded to one of the two meanings of the homonymous keyword — mammal animal, or baseball equipment — by humans or by AI. First-order logic does not require that grounding.
This is not a new model. It is a verification method: take an NLI pair, translate it by the NLI-with-FOL scheme, and test it with first-order resolution — twice, once in each direction — and then read the label off the two results, not off a single empty clause.
Has wings. Can fly. Is a mammal.
Bat = animal
Has a barrel. Used in baseball. Is not a mammal.
Bat = equipment
One predicate, two meanings, in the same premise. That is the prop that breaks the logic — and the joke that makes it comical.
Mapping function I, by Symbolic Logic: Domain of discourse D is a non-empty set of abstract objects. If c is a constant, I(c) ∈ D. If P is a unary predicate, I(P) ⊆ D. For the collapsed example:
D = {d1, d2} · I(Brown_Bat) = d1 · I(Bat) = {d1, d2} · I(HasWings) = {d1} · I(HasBarrel) = {d2}
The catch, structurally: force Rule 2 true, and d2 must have wings — then wings and barrels collide. Force Rule 3 true, and d1 must have a barrel — then Rule 1 breaks. Force both true at once, and there is no interpretation left. The collapsed KB is unsatisfiable: d = I(Brown_Bat) would have to sit in Bat, in HasWings, and in HasBarrel, but HasWings ∩ HasBarrel = ∅.
Linear resolution is a chain, not a branching search: the most recent derived clause is the centre, the side clause is an input or ancestor clause. Starting from the KB alone, without the query:
D = {d1}, H: “Brown bat is a mammal” is TRUE.
D = {d1}, H is FALSE.
Neither world forces H, neither world is the collapsed KB. At this unresolved level only: Neutral / logically inconclusive, for equivocation-induced pairs only.
So the method verifies, in one picture: collapsed → cannot decide (both tests close vacuously, or one closes and one does not), split → Neutral / logically inconclusive (both tests do not force H, worlds disagree). That coincidence, at the unresolved level and only for equivocation-induced pairs, is the hypothesis being verified — not a claim about all Neutral pairs.
Incoherent universals: “Bats have wings” and “Bats have a barrel” assert properties universally for two different meanings of “bat” in the same premise. That is equivocation, and it renders an inconclusive inference.
Collapsed model: Domain D = {d1, d2}, I(Brown_Bat) = d1, I(Bat) = {d1, d2}, I(HasWings) = {d1}, I(HasBarrel) = {d2}. No interpretation satisfies the collapsed KB: a Brown bat would have to be in both wings and barrel, but wings and barrel do not intersect. Linear resolution, KB only, without the query: Bat → HasWings → ¬HasBarrel → ¬Bat → empty, in 4 steps.
| Resolution type | KB AND NOT QUERY | KB AND QUERY | Final Label |
|---|---|---|---|
| Traditional | Yes | Yes | cannot decide — both empty |
| Linear | Yes | Yes | cannot decide — both empty |
| Unit | Yes | Yes | cannot decide — both empty |
| Input | Yes | Yes | cannot decide — both empty |
| Set of Support | Yes | No | inconclusive inference |
| Hyper | Yes | Yes | cannot decide — both empty |
| Ordered | Yes | Yes | cannot decide — both empty |
Main design uses 2 procedures (Traditional, Linear). 7 named types are tested in total, with Ordered under 2 orders. NLI Label is Neutral in every row. Neutral as a Final Label appears only at the unresolved level: H true in the mammal world, false in the baseball world, neither follows.
Try it:
python3 -m unittest discover -s tests -v python3 run.py --results-table python3 run.py --no-model --case brown_bat
Code: legal-agent-workshop-for-incoherent-universals
Prior work: human-ai-collaborated-ai4science (32 examples from 4 hand-curated examples, partial and preliminary, not re-run here)
Runtime: Meta Model API only, Muse model muse-wonder-1.0 by default.
Put this HTML file next to a folder called supplied-input-documents/ containing the 3 documents below, and these links will work. If you put this page in a subfolder, put that folder inside the same subfolder.
Plan-and-proof-sketch-nli-inconcl.pdf
Summary: The original plan and proof sketch. NLI/FOL intersection (premise = KB, hypothesis = query, both resolution tests), incoherent universals, Brown Bat KB and query, Domain D model proof, and unrestricted and linear resolution chains. Key warning: resolution can derive an empty clause without ever touching the query clause, so an empty clause alone is not a proof about the query.
Summary: The condensed proof the implementation follows. Domain D method, the I0 interpretation (rules 1 and 4 true, rules 2 and 3 false), the general no-model proof, and the linear chain Bat → HasWings → ¬HasBarrel → ¬Bat → empty. This is the proof the verifiers check against.
Preparation-prompts-with-muse.txt
Summary: The preparation prompts used with Muse to build the Results Table, following the NLI-with-FOL proof sketch. Prerequisite: a Results Table with columns NLI Label and Final Label, row 1 KB AND NOT QUERY, row 2 KB AND QUERY. Step 1: resolution over KB AND NOT QUERY (empty = entailment, else neutral or contradiction), then KB AND QUERY (empty = contradiction, else neutral or entailed, called “inconclusive” at row level). Step 2: both rows no-empty = Neutral. Step 3: re-run step 1 over each resolution type, with a Muse call per type per test, recorded in the table. Step 4: both no-empty = Neutral; one empty, one no-empty = cannot decide / inconclusive inference — which is not the same as Neutral, and not the same as logically inconclusive. Steps 5–6: fill in the results for this example, and repeat for Unit, Input, Set of Support, Linear, Hyper and Ordered resolution (with an order defined). The rejected paper is deliberately not uploaded here.
Scope, stated openly: theoretical proof only, no evaluator, equivocation-induced pairs with the Brown Bat / Brown A structure only, not all Neutral pairs. Grounded resolution, not a full first-order prover; readings-based NLI, not a general NLI model.
These are my own work, not external references. This is my hard work, and any continuation of it should acknowledge and give credit to my initiative.
I am not interested in this project. It was created for fun. I have the copyrights for this as the original creator, please email sushma.ananda13@gmail.com as I have switched to representational Geometry and Brain-AI neuroscience sometime back. Thank you.
This is my hard work, but I have come across people who were obsessed to work on this despite court-agreed no contact, and there were others who compelled me to work with such, and I completely lost interest, and in the process I have my copyrights but I am no longer interested. I have made a decision upon consulting my wellwishers and I do not prefer to continue to work on this. However, if anyone wants to continue this work while acknowledging and giving credits to my initiative, I would love to sell this under a legal and valid legal process and appropriate Government required/assisted guidances. Please contact me at sushma.ananda13@gmail.com for any such enquiry.
At the time when I worked on this, I really thought I would be supported by brown bats, but now I find out no support whatsoever and instead use of deepfake. In an attempt to respect myself and my dignity, I have chosen to discontinue on this.