[Bug]: Logic engine 'is'/'is not' patterns silently drop RHS operand — returns verified=True for rewritten premises

[rahuldass19]

QWED-MCP Audit Finding: MED-05

Severity: 🟡 MEDIUM
Component: logic_engine.py — parse_statement (" is " / " is not " patterns)
Audit ID: MED-05
Re-audit of v0.2.1: Finding is NEW — distinct from #16 (status conflation). This is semantic corruption producing wrong verified=True.

---

Description

The natural-language is patterns silently discard the right-hand operand and misbind negation. Empirically confirmed on v0.2.1:

# logic_engine.py L75-80
if " is " in stmt:
    parts = stmt.split(" is ", 1)
    if parts[1].startswith("not "):
        return Not(get_var(parts[0]))   # "A is not B" -> NOT A  (B dropped!)
    return get_var(parts[0])            # "A is B"     -> A      (B dropped!)

Live probe results:

verify_logic_statement(premises=["A is B"],     conclusion="A")
# -> verified=True   (premise was silently rewritten to just "A")

verify_logic_statement(premises=["A is not B"], conclusion="not A")
# -> verified=True   ("A is not B" was rewritten to NOT A; "B" vanished)

The engine returns verified=True for arguments whose premises it silently rewrote. This is worse than a parse failure: the user receives an affirmative verification of a different argument than the one submitted.

Semantic expectations that are violated:

Input	Parsed as	Any reasonable reading
A is B	A	A ↔ B or A → B — never bare A
A is not B	¬A	A → ¬B — never bare ¬A

---

Why This Violates QWED Philosophy

• Principle 6 — No Silent Degradation: The parser quietly substitutes a weaker (and different) proposition for the submitted one, then verifies the substitute. Failures must remain visible; here the failure is invisible and crowned with verified=True.
• Principle 2 — Fail Closed: If is/is not semantics cannot be deterministically modeled, the pattern must be rejected as UNVERIFIABLE, not approximated.

---

Expected Behavior

• A is B must either map to an explicit deterministic semantics (e.g., biconditional A ↔ B, or implication with documented direction) or be rejected as unsupported.
• A is not B must never drop B.
• Any statement pattern the parser cannot model must produce verified=False with verification_mode: "UNVERIFIABLE" (aligns with the status taxonomy in [Bug]: Logic engine conflates parse errors with logical refutations — cannot distinguish DISPROVEN from UNVERIFIABLE #16), never a rewritten premise.

---

Suggested Fix Direction

if " is " in stmt:
    parts = stmt.split(" is ", 1)
    lhs, rhs = get_var(parts[0]), parse_statement(parts[1])
    return And(Implies(lhs, rhs), Implies(rhs, lhs))   # biconditional, or
    # raise UnsupportedStatementError(...)             # fail closed

Whichever semantics is chosen, add regression tests proving the RHS operand participates in the Z3 model (e.g., premises=["A is B"], conclusion="B" must verify; premises=["A is not B"], conclusion="not B" behavior must match the documented semantics).

---

Environment

Field	Value
QWED-MCP Version	0.2.1
Component	Logic Verification Engine
File	src/qwed_mcp/engines/logic_engine.py (L75–80)