MCP Logic

Prove a logical statement using resolution.

When to use: You have premises and want to verify a conclusion follows logically. When NOT to use: You want to find counterexamples (use find-counterexample instead).

Example: premises: ["all x (man(x) -> mortal(x))", "man(socrates)"] conclusion: "mortal(socrates)" → Returns: { success: true, result: "proved" }

Common issues:

• "No proof found" often means inference limit reached, not that the theorem is false

• Try increasing inference_limit for complex proofs

Check if logical statements are well-formed with detailed syntax validation.

When to use: Before calling prove/find-model to catch syntax errors early. When NOT to use: You already know the formula syntax is correct.

Example: statements: ["all x (P(x) -> Q(x))"] → Returns: { valid: true, statements: [...] }

Common syntax issues:

• Use lowercase for predicates/functions: man(x), not Man(x)

• Quantifiers: "all x (...)" or "exists x (...)"

• Operators: -> (implies), & (and), | (or), - (not), <-> (iff)

Find a finite model satisfying the given premises.

When to use: You want to show premises are satisfiable (have at least one model). When NOT to use: You want to prove a conclusion follows (use prove instead).

Example: premises: ["exists x P(x)", "all x (P(x) -> Q(x))"] → Returns: { success: true, model: { domain: [0], predicates: {...} } }

Performance notes:

• Searches domains size 2 through max_domain_size (default: 10)

• Larger domains take exponentially longer

• Use domain_size to search a specific size only

Find a counterexample showing the conclusion doesn't follow from premises.

When to use: You suspect a conclusion doesn't logically follow and want proof. When NOT to use: You want to prove the conclusion (use prove instead).

Example: premises: ["P(a)"] conclusion: "P(b)" → Returns counterexample where P(a)=true but P(b)=false

How it works: Searches for a model satisfying premises ∧ ¬conclusion. If found, proves the conclusion doesn't logically follow.

Verify that a categorical diagram commutes by generating FOL premises and conclusion.

When to use: You have a categorical diagram and want to verify path equality. When NOT to use: For non-categorical reasoning (use prove directly).

Example: path_a: ["f", "g"], path_b: ["h"] object_start: "A", object_end: "C" → Generates premises/conclusion for proving compose(f,g) = h

Output: Returns premises and conclusion to pass to the prove tool.

Get FOL axioms for category theory concepts.

Available concepts:

• category: Composition, identity, associativity axioms

• functor: Preserves composition and identity

• natural-transformation: Naturality condition

• monoid: Binary operation with identity and associativity

• group: Monoid with inverses

Example: concept: "monoid" → Returns axioms for monoid structure

Create a new reasoning session for incremental knowledge base construction.

When to use: You want to build up premises incrementally and query multiple times. When NOT to use: Single query with all premises known upfront (use prove directly).

Example: ttl_minutes: 30 → Returns: { session_id: "uuid...", expires_at: ... }

Notes:

• Sessions auto-expire after TTL (default: 30 minutes)

• Maximum 1000 concurrent sessions

• Session ID must be passed to all session operations

Add a formula to a session's knowledge base.

When to use: Building up premises incrementally in a session.

Example: session_id: "abc-123..." formula: "all x (man(x) -> mortal(x))" → Adds the formula to the session KB

Query the accumulated knowledge base in a session.

When to use: After asserting premises, query for a conclusion.

Example: session_id: "abc-123..." goal: "mortal(socrates)" → Attempts to prove the goal from accumulated premises

Remove a specific premise from a session's knowledge base.

When to use: You need to undo an assertion or explore alternative premises.

Example: session_id: "abc-123..." formula: "man(plato)" → Removes the exact formula if found

List all premises in a session's knowledge base.

When to use: Review what has been asserted so far.

Example: session_id: "abc-123..." → Returns: { premises: ["all x (man(x) -> mortal(x))", "man(socrates)"] }

Clear all premises from a session (keeps session alive).

When to use: Start fresh within the same session.

Example: session_id: "abc-123..." → Clears all premises, session remains valid

Delete a session entirely.

When to use: Done with a session, want to free resources.

Example: session_id: "abc-123..." → Session is deleted and ID becomes invalid